arxiv-2409.13082-autoverus

Extract — AutoVerus (multi-agent Verus proof synthesis)

• URL: https://arxiv.org/abs/2409.13082 (read via https://arxiv.org/html/2409.13082; PACMPL OOPSLA’25 DOI 10.1145/3763174)
• Fetched: 2026-09-27 ~19:33 CST · defuddle parse —md
• Authors: Yang et al. (UIUC / Columbia / UCI / Toronto / MSR / MSRA / UChicago)
• Code (related): https://github.com/microsoft/verus-proof-synthesis

Core claims

• AutoVerus generates Verus proof annotations (loop invariants, asserts, lemma/proof fns) for given Rust code + specs — not the executable code. Specs assumed provided.
• Three-phase orchestration mimicking Verus experts: (1) preliminary loop-invariant generation (high-temp multi-output); (2) generic refinement agents for common invariant mistakes/omissions; (3) error-driven debugging (~10 agents keyed to Verus error types: postcond, pre-loop invariant, assert failure, …) up to ~10 iterations.
• Discipline over creativity: Lynette (AST tool on Verus parser) filters “cheating” (modified code/specs, assume(...)), ranks by Verus feedback, merges complementary partial proofs; Houdini subset minimization.
• Design principles: no fine-tune / RAG on scarce Verus data (<10 GitHub projects at writing); encode human expertise in agent instructions; high-temp diversity + formal filtering.

Numbers (Verus-Bench, 150 tasks from Diffy/MBPP/CloverBench → Rust/Verus)

• AutoVerus: 137/150 (~91%+) proved.
• Baseline direct GPT-4o: 67/150 (45%) despite longer time/call budget + 4 answer examples in prompt.
• Efficiency: >half of tasks solved in <30s or ≤3 LLM calls; baseline <40 under same tight budget.
• Subsets: Diffy+CloverBench 100%; MBPP 87% (harder — needs beyond-invariants).
• Models: GPT-4o / GPT-4-turbo / DeepSeek-R1 comparable; R1 slightly fewer; 4-turbo slower.

DIY-relevant patterns

• Error-type → specialized repair agent routing is the high-value DIY pattern for Verus (and portable to Dafny etc.).
• Merge partial candidates (linear best-so-far merge, not exponential) + Houdini prune.
• Static safety gate (Lynette) before spending Verus cycles — reject code/spec edits and assumes.
• Progress scoring via Verus error counts / verified fragment score V (imperfect vs ITP goal-diff, but workable).
• Verus quirks that burn LLM tokens: int/nat casts, @ view (Vec→Seq), ghost vs exec API misuse, axioms needing explicit asserts for Seq/Set ops, overflow invariants like count <= i.
• Adopt: 3-phase propose→refine→debug; multi-candidate + merge; cheat filter. Skip: one-shot prompting; trusting LLM not to rewrite implementation.
• Schwarz later shows AutoVerus 69.3% on KVerus-File vs Schwarz 95.5% — AutoVerus is strong on Verus-Bench-scale but solver-local repair helps at project scale.

Gaps / confidence

• Specs are inputs — not a full propose-spec→prove loop. Verus-Bench tasks are small single-fn translations, not repo-scale systems (authors failed to extract from large Verus projects due to deps). Confidence high on agent-orchestration patterns; medium on extrapolating 90% to Herdr fleet code.