VeruSAGE: A Study of Agent-Based Verification for Rust Systems

This paper introduces VeruSAGE-Bench, a new benchmark of 849 proof tasks from eight open-source Verus-verified Rust systems, and demonstrates that tailored LLM-agent combinations can successfully solve over 80% of these tasks and more than 90% of unfinished system proofs, highlighting the significant potential of AI-assisted verification for system software.

The Gist

Imagine you are building a massive, high-speed train system (like a computer's operating system). You want to be 100% sure that the brakes will always work and the train will never derail.

In the old days, you'd hire a team of super-smart, paranoid engineers to write a mathematical "proof" for every single bolt and gear. This is called Formal Verification. It's incredibly safe, but it's slow, expensive, and requires a PhD in math just to read the instructions.

Then, Artificial Intelligence (LLMs) arrived. These AIs are like incredibly fast, creative interns. They can write code in seconds. But there's a catch: they are confident but often wrong. They might build a train that looks great but has no brakes.

The Big Question: Can we combine the speed of the AI intern with the safety of the paranoid engineer? Can an AI write the "mathematical proof" that guarantees the code is safe?

This paper, VeruSAGE, says: "Yes, but it depends on how you manage the AI."

Here is the breakdown of their discovery, using some everyday analogies:

1. The Problem: Small Puzzles vs. Giant Mazes

Previous studies asked AI to solve tiny math puzzles (like "find the middle number in a list"). The AI was great at these.
But real-world systems (like operating systems) are like giant, tangled mazes. They have thousands of moving parts, complex rules, and no simple "middle number."

• The Finding: When the researchers tested AI on these giant mazes, the old methods failed miserably. The AI got lost immediately.

2. The Solution: Two Different Management Styles

The researchers tested four different "super-intelligent" AI models (like the latest versions of GPT and Claude). They discovered that one size does not fit all. You have to manage different AIs differently.

Style A: The "Hands-Off" Boss (For the Smartest AIs)

For the most advanced models (like Sonnet 4.5), the researchers acted like a hands-off boss.

• The Setup: They gave the AI a file, a set of rules (the "Verus" tool), and a "cheat detector" (to make sure the AI doesn't just fake the proof).
• The Result: The AI was so smart it figured out the whole maze on its own. It didn't need step-by-step instructions.
• Analogy: Imagine giving a genius chess player the board and saying, "Checkmate me." They don't need you to tell them which piece to move; they just see the whole game and win.
• Success Rate: These models solved 81% of the complex tasks!

Style B: The "Hands-On" Coach (For the Smarter-but-Struggling AIs)

For slightly less powerful models (like o4-mini), the "hands-off" approach failed. They got confused and made syntax errors (typos in the math language).

• The Setup: The researchers built a coach system called VeruSAGE. This system breaks the giant maze into tiny steps.
  1. The Planner: The AI looks at the error and says, "Okay, I need to use a specific strategy here."
  2. The Specialist: The system calls a specific "agent" (like a math expert or a logic expert) to fix just that one error.
  3. The Reviewer: The system checks if the fix actually helped before moving to the next step.
• The Result: This coaching doubled the success rate for these models.
• Analogy: This is like teaching a student to solve a complex equation. You don't just say "solve it." You say, "First, isolate X. Good. Now, divide by 2. Good. Now, check your work."

3. The Surprise: AI Can Fix Human Mistakes

The researchers gave the AI a project that humans were still working on (Atmosphere, an operating system).

• The Magic: The AI didn't just finish the proofs; it found bugs in the human's own rules.
• The Story: The humans wrote a rule that said, "If you skip the first item in a list, the rest won't contain that item." The AI looked at it, thought, "Wait, that's wrong if the list has duplicates!" and suggested a fix. The human experts agreed and fixed it.
• Takeaway: The AI isn't just a worker; it's a critical thinking partner.

4. The Catch: Time and Money

• Speed: The "Hands-Off" genius models were fast (about 7 minutes per task).
• Cost: The "Hands-On" coaching was slower and cost more because it took many small steps to get there.
• The Trade-off: If you have a budget, use the "Hands-Off" genius. If you need to save money and have a slightly less smart model, use the "Hands-On" coach, but be prepared to wait.

The Bottom Line

This paper proves that AI is ready to help write the safety proofs for our most critical software (like self-driving cars or banking systems).

• For the smartest AIs: Just give them the tools and let them run.
• For the others: You need a smart system to break the problem down and guide them step-by-step.

We aren't replacing the human engineers yet (the humans still have to design the system and the rules), but we are finally getting a tool that can do the boring, difficult math work that keeps the system safe. It's like finally getting a robot that can not only build the house but also pass the building inspector's test.

Technical Summary

1. Problem Statement

While Large Language Models (LLMs) have demonstrated impressive capabilities in generating code, their ability to rigorously reason about and prove the correctness of system-level software remains unproven. Previous research (e.g., AutoVerus, RagVerus) focused on small programming tasks or specific benchmarks (like VerusBench), which often lack the complexity of real-world systems. These studies showed poor performance (often <20% success) when applied to large-scale, verified Rust systems.

The core challenges identified are:

• Complexity Gap: Real-world system proofs involve massive specifications, complex dependencies, and helper lemmas, unlike small benchmark tasks dominated by loop invariants.
• Agent Architecture Limitations: Existing agent systems (like AutoVerus) were designed for small tasks and lack the strategic depth to handle system-level verification errors.
• Model Limitations: It is unclear whether current state-of-the-art LLMs (e.g., GPT-5, Claude Sonnet 4.5) can handle system verification without specialized agent designs, or if they require different approaches (hands-on vs. hands-off) based on their specific strengths.

2. Methodology

A. Benchmark Construction: VeruSAGE-Bench

The authors created a comprehensive benchmark suite to evaluate LLMs on real system verification tasks.

• Source: Extracted from 8 open-source, Verus-verified Rust systems (including operating systems like Atmosphere, storage systems, memory allocators, and distributed systems).
• Scale: Contains 849 proof tasks.
• Extraction Process:
  • Each task is a standalone Rust file containing the target function, all necessary dependencies (signatures only, bodies replaced with unimplemented!() to prevent copying), and pre/post-conditions.
  • Crucial Step: All original proof bodies and annotations are removed, forcing the LLM to generate proofs from scratch.
• Characteristics: Compared to previous benchmarks, VeruSAGE-Bench tasks are significantly larger (avg. ~947 LoC vs. 32 LoC), contain far more specifications (avg. ~496 LoC), rely heavily on helper lemmas (2.4 per task vs. 0.07), and have very few loop invariants (a common feature in smaller benchmarks).

B. Agent System Designs

The study evaluates two distinct agent approaches across four LLMs: o4-mini, GPT-5, Sonnet 4, and Sonnet 4.5.

1. Hands-Off Approach (CLI Agents):

   • Mechanism: Uses generic coding agents (GitHub Copilot CLI, OpenAI Codex) with a simple prompt.
   • Tools: Grants the LLM access to the Verus compiler, a "cheat checker" (to detect assume/admit misuse), and the Verus standard library (vstd).
   • Strategy: The LLM drives the process, iterating on code and running Verus autonomously.
   • Target: Best suited for strong, general-purpose coding models (e.g., Sonnet 4/4.5).

2. Hands-On Approach (VeruSAGE):

   • Mechanism: A specialized, multi-agent system designed to "teach" the LLM verification strategies.
   • Architecture:
     • Planning Agent: Analyzes errors and context to select the best strategy (e.g., induction, case analysis) before acting.
     • Action Agents: Specialized agents for specific tasks (e.g., bit-vector solver, non-linear arithmetic, quantifier instantiation, lemma usage).
     • Candidate Selector: Sophisticated logic to accept intermediate proof candidates that may temporarily increase error counts but represent strategic progress (e.g., divide-and-conquer).
     • Context Management: Tracks history and provides concise code diffs to avoid token overflow.
   • Target: Designed to boost "smaller" or reasoning-focused models (e.g., o4-mini, GPT-5) that struggle with raw syntax and strategy without guidance.

3. Key Contributions

1. VeruSAGE-Bench: The first large-scale, diverse benchmark for system-level verification in Rust, revealing that system proofs are structurally distinct from small-program proofs (high spec/lemma density, low loop density).
2. Dual-Agent Strategy: Demonstrated that different LLMs require fundamentally different agent architectures.
   • Strong Coding Models (Sonnet 4/4.5): Perform best with a Hands-Off approach, leveraging their ability to self-correct and search large contexts efficiently.
   • Reasoning/Smaller Models (o4-mini, GPT-5): Require a Hands-On approach (VeruSAGE) to overcome syntax errors and lack of high-level strategy.
3. Human-LLM Collaboration: Showed that LLMs can not only complete unfinished human proofs but also identify and correct errors in human specifications (e.g., spotting missing preconditions in the Atmosphere OS project).

4. Experimental Results

• Success Rates:
  • The best combination (Sonnet 4.5 + Hands-Off) achieved an 81% success rate on the entire VeruSAGE-Bench (849 tasks).
  • It achieved 100% success on three projects (Anvil Library, Node Replication, Vest).
  • On the Atmosphere OS project (a new, unreleased system), it achieved 83% success, including proving tasks that human experts had not yet finished.
• Performance of VeruSAGE (Hands-On):
  • Doubled the success rate of o4-mini (from ~17% with AutoVerus/Codex to 41%).
  • Improved GPT-5 from ~20% to 55%.
• Efficiency:
  • Sonnet 4.5 (Hands-Off) is the fastest, completing 60% of tasks in under 6 minutes.
  • Cost: The Hands-Off approach is generally more cost-effective for Sonnet models due to fewer "chatty" interactions, though Hands-On is cheaper for o4-mini due to strict token control.
• Failure Analysis:
  • Sonnet 4.5 struggles with inductive invariants (finding stronger invariants for state machines) and procedural macro expansion (understanding code generated by macros).
  • o4-mini frequently fails due to syntax errors and hallucinations about existing lemmas, highlighting the need for the Hands-On "tutorial" and syntax-repair agents.
• Proof Quality:
  • LLM proofs are often longer (more "chatty") than human proofs because LLMs over-annotate what theorem provers could solve automatically.
  • However, LLMs are excellent at finding and utilizing helper lemmas from the standard library (vstd).

5. Significance and Conclusion

• Feasibility of Automated Verification: The study proves that LLMs, when paired with the right agent architecture, can synthesize formal proofs for complex, real-world system software with high success rates (>80%).
• Paradigm Shift: It challenges the notion that LLMs are only for "quick and dirty" code. Instead, they can serve as powerful assistants for high-assurance systems, provided the verification environment is structured correctly.
• Future Directions:
  • Inductive Invariants: A major remaining bottleneck is the automatic generation of inductive invariants for state machines.
  • Specification Generation: Current LLMs are good at proving given specs but not yet capable of breaking down high-level system goals into the correct low-level specifications and lemmas.
  • Collaboration: The paper suggests a future workflow where LLMs act as "oracles" for AI-generated code, significantly accelerating the development of verified systems while humans focus on high-level design and invariant discovery.

In summary, VeruSAGE demonstrates that the gap between AI coding and formal verification is closing, but it requires a nuanced understanding of model capabilities and the deployment of specialized, context-aware agent systems.