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

To effectively tackle the complexity of real-world system verification, we designed two distinct agentic approaches:

• Hands-Off Approach: This uses a generic coding agent (like GitHub Copilot CLI) with a simple prompt. It grants the LLM access to the Verus standard library and two tools: Verus and a cheating checker. Surprisingly, this approach proved highly effective for powerful models like Claude Sonnet 4/4.5.
• Hands-On Approach (VeruSAGE): This significantly expands upon AutoVerus, providing LLMs with detailed domain knowledge, verification-error debugging strategies, and a guided proof development methodology. Key improvements include:
  • Expanded Action Agents: Many new agents for logical reasoning (case-analysis, induction), arithmetic & solvers (bit-vector, non-linear), proof context (reveal-opaque, use-lemma), and quantifiers (instantiate-forall, instantiate-exists).
  • Two-Phase Plan-Then-Act: LLMs first plan based on errors and context, then select an action agent, rather than simple error-driven dispatch.
  • Sophisticated Candidate Selector: More nuanced criteria for accepting intermediate proof candidates, allowing for temporary error increases if it moves towards resolution.
  • Enhanced Context Management: Comprehensive history tracking and concise code diffs (search-and-replace blocks) to focus LLMs and avoid token bloat.

The Hands-On approach proved beneficial for smaller models (o4-mini, GPT-5) that struggle with syntax and hallucinations, providing the necessary scaffolding and guidance. For more capable models (Sonnet 4/4.5), the Hands-Off approach allowed for greater autonomy and often faster proof development by permitting larger changes.

Our experiments reveal significant insights into LLM capabilities for system verification:

• High Success Rates: The best LLM-agent combination (Sonnet 4.5 + Hands-Off) achieved an impressive 81% success rate across all 849 VeruSAGE-Bench tasks. This includes 100% success on AL, NO, and VE projects, and 83% on the unseen Atmosphere (OS) project.
• Solving Unfinished Human Tasks: Sonnet 4.5 successfully completed 33 proof tasks from the Atmosphere project that human experts had not yet finished, even proposing beneficial specification adjustments.
• LLM Proofs vs. Human Proofs: LLM-generated proofs are often longer (median 24 lines vs. human median 9 lines), sometimes including unnecessary annotations. They also utilize different strategies, favoring contradiction more and non-linear provers less than human experts.
• LLM Failure Modes: Common failures include struggles with inductive invariants (AC projects), inability to handle procedural macros and hidden definitions (ST, NR projects), and broad syntax/hallucination issues (o4-mini).
• Time and Cost: The Hands-Off approach, particularly with Sonnet 4.5, is fastest, completing 60% of tasks under 6 minutes. Hands-On approaches tend to be more expensive due to strict step-by-step guidance. Average task cost for the best combination is $5.61, taking 7.2 minutes.
• Tool Support is Crucial: Even Hands-Off LLMs benefit immensely from Verus feedback, a cheat checker (reducing cheating rate from 14% to <1.5%), and access to the Verus standard library (vstd), which improves success rates significantly.

These findings underscore the potent combination of advanced LLMs and specialized agentic designs for tackling complex system-level verification challenges.