AutoVerus
LLM agents write the proof annotations Verus needs to prove Rust code correct, and Verus's error messages drive the repair rounds.
The loop
- Proposes
Proof annotations (loop invariants, assertions) for Rust code with Verus specifications, from GPT-4o agents
- Judged by
The Verus verifier, which either proves the specification or returns errors
- Steers
Three phases: initial proof, refinement with generic tips, then agents that fix the specific errors Verus reports
Headline result
Proves 137 of 150 tasks (91.3%) on Verus-Bench, with at most 3 tries per task and GPT-4o; 122 were proved on the first attempt. A baseline that repeatedly calls GPT-4o for up to 10 minutes proved 67 of 150. More than half were done in under 30 seconds or 3 LLM calls.
What this does not prove
Verus-Bench is a 150-task suite the authors built from existing code and verification benchmarks, and the task gives the code and the specification. The tool proves what the spec says; a wrong spec would still pass.
How it generalizes the harness
Verus decides validity, not an LLM or a test, and the verified annotations stay in the code with no model needed to re-check them.
Classification
| What it proposes | Proof |
|---|---|
| Generative model | GPT-4o (frozen), orchestrated as a network of specialized agents |
| Algorithmic authority | Verus verifier (SMT-based) |
| Feedback | Verifier errors |
| What gets updated | Prompt context |
| When it runs | At inference time |
| Validity | Formal (machine-checked) |
| Evidence | Experiments reported |
| Lineage | Original system |