The hardest part of formal verification has never been the verifier. It is writing the proof.
Give a senior Rust engineer Verus, the SMT-based verifier from Microsoft Research, and they can annotate a function with preconditions and postconditions in an afternoon. The verifier will then tell them, with mechanical certainty, whether the function satisfies those contracts for every possible input. That part is satisfying.
Then they hit a loop. The verifier complains that it cannot establish the postcondition. The engineer needs an invariant, a logical statement that is true before and after every iteration. Finding that invariant used to require a PhD, or at least forty hours of trial and error. AutoVerus, published at OOPSLA 2025, automates more than 90% of that work using a network of LLM agents. The median proof task resolves in under 30 seconds or three LLM calls.
Here is how it actually works, what it costs you, and where it still breaks.
The Real Bottleneck Is Invariant Search, Not the SMT Solver
Verus extends Rust with ghost code, preconditions, and postconditions. You write something like this:
use vstd::prelude::*;
verus! {
fn sum(arr: &[i32]) -> (result: i32)
requires
arr.len() <= 0x40000000,
ensures
result == spec_sum(arr@),
{
let mut total = 0;
let mut i = 0;
while i < arr.len()
invariant
0 <= i <= arr.len(),
total == spec_sum(arr@.subrange(0, i as int)),
{
total = total + arr[i];
i = i + 1;
}
total
}
}The requires clause is the precondition. The ensures clause is the postcondition. The invariant block inside the while loop is what makes the proof go through. It tells the SMT solver what stays true on every iteration.
The hard part is the invariant. total == spec_sum(arr@.subrange(0, i as int)) is not obvious. A human writes it by thinking inductively about what stays true after processing the first i elements. AutoVerus generates this automatically by treating invariant synthesis as a search problem guided by verifier feedback.
How AutoVerus Uses LLM Agents as a Search Strategy
AutoVerus is not a single prompt to GPT-4. It is a pipeline of specialized agents that pass structured context to each other.
The first agent reads your Rust function and its doc comments. It extracts the verification conditions and generates an initial draft of requires, ensures, and invariant clauses.
The second agent feeds these annotations into Verus. Verus compiles the annotated code and asks its SMT solver, usually Z3, to discharge the proof obligations. If the solver says UNSAT, the property holds. If it says SAT, it produces a counterexample. Most of the time, the first draft fails.
The repair agent reads the verifier error message and the failed proof obligation. It suggests a stronger invariant, a tighter bound, or an auxiliary lemma. The cycle repeats: generate, verify, repair. AutoVerus reports a median convergence of three LLM calls. More than half of the 150 non-trivial benchmark tasks finish in under 30 seconds.
The insight is not that LLMs are brilliant at logic. Proof search is a local optimization problem, and LLMs are good enough at guessing local improvements to navigate the space faster than a human typing by hand.
What the 90% Figure Actually Means
AutoVerus achieved over 90% proof automation on a benchmark of 150 non-trivial Rust proof tasks. These included array bounds reasoning, loop accumulation, and recursive structure traversal. The benchmark was drawn from real Verus codebases.
The 90% figure means the LLM pipeline generated a proof that Verus accepted without human intervention. It does not mean the specification is what the programmer intended. The LLM infers intent from function names, doc comments, and type signatures. If your function is called process and your doc comment says “handles the thing,” the generated specification will be generic and possibly wrong.
This is the same division of labor that copilots introduced for code generation. The LLM writes the first draft. The human reviews it for domain correctness. The difference is that a wrong proof is silent. A generated proof that passes verification may prove the wrong property. You still need a human who understands what the function is supposed to do.
What AutoVerus Cannot Do
AutoVerus is bounded by what Verus can express. Verus handles a subset of Rust. It does not support async, closures, or certain standard library collections. If your code spawns tasks with tokio, AutoVerus cannot help you yet.
AutoVerus is also pattern-bound. The 90% success rate applies to code that looks like the training distribution: loops over arrays, arithmetic accumulation, bounds checking. If your proof requires a non-obvious auxiliary lemma, the repair agent may loop until it hits its iteration limit. At that point, you are back to writing the proof by hand.
The cost is not zero either. The benchmark tasks cost cents per proof. A full module might cost ten to thirty dollars in API calls. That is two orders of magnitude cheaper than a verification engineer’s time, but it is not free.
Running AutoVerus on Real Code
AutoVerus is available from Microsoft Research. The repository is microsoft/verus-proof-synthesis on GitHub. It expects you to have Verus installed.
Here is the practical workflow:
# 1. Install Verus
git clone https://github.com/verus-lang/verus.git
cd verus && source ./source/vstd.sh
# 2. Clone AutoVerus
git clone https://github.com/microsoft/verus-proof-synthesis.git
cd verus-proof-synthesis
# 3. Set your API key for the LLM backend
export OPENAI_API_KEY="sk-..."
# 4. Run AutoVerus on a Rust file
python autoverus.py --input src/my_module.rs --output src/my_module_verified.rsThe output is an annotated Rust file with requires, ensures, and invariant clauses. Review every annotation. Then run Verus:
verus src/my_module_verified.rsIf Verus reports verification results:: verified, the SMT solver has discharged all obligations. If it reports errors, feed them back into AutoVerus for another repair round or fix them manually.
For CI integration, treat Verus as a separate job that runs only on annotated modules. Verus verification time grows with annotation complexity. Start with the functions that scare you: parsers, protocol state machines, anything that indexes into untrusted buffers.
When to Use AutoVerus and When to Walk Away
AutoVerus is worth trying when you have Rust code that fits the Verus subset and you want unbounded proofs of correctness. Kani gives you bounded proofs without annotations, which is faster for crash-freedom checks but cannot prove properties over unbounded loops. AutoVerus gives you the full unbounded proof, at the cost of needing annotations that it mostly generates for you.
Walk away if your code is async, uses complex closures, or requires proofs about liveness properties like “every request eventually gets a response.” For liveness, you still want TLA+. Walk away if your proof requires a custom mathematical theory. The LLM agents do not invent new mathematics. They retrieve and adapt patterns they have seen before.
The Honest Bottom Line
AutoVerus does not eliminate the need to understand your code. It eliminates the need to spend forty hours writing invariants for code you already understand. The shift is from proof engineering to prompt engineering: you describe the intent, the agents search the proof space, and the SMT solver certifies the result.
That shift is enough to move formal verification from a specialist niche to a CI pipeline step. For the thirty lines of parsing code between your application and untrusted network input, it is now practical to prove they will not panic. The proof is generated in seconds, checked in minutes, and reviewed by a human who knows what the parser is supposed to do.
Start with one function. Write the Rust. Run AutoVerus. Read the annotations. If they match your intent, you have a machine-checked proof. If they do not, you have a starting point better than a blank page.
Frequently Asked Questions
What is AutoVerus and how does it relate to Verus?
AutoVerus is an automated proof generation system built on top of Verus, a Rust verifier from Microsoft Research. Verus checks whether annotated Rust code satisfies its specifications using an SMT solver. AutoVerus generates those annotations using a network of LLM agents.
How accurate is AutoVerus at generating proofs?
On its benchmark of 150 non-trivial Rust proof tasks, AutoVerus achieved over 90% automation. More than half resolved in under 30 seconds or three LLM calls. Accuracy depends on how closely your code matches the training distribution patterns.
Does AutoVerus eliminate the need to learn formal verification?
No. You still need to understand the annotations to review them for correctness. A generated proof that passes verification may prove the wrong property if the LLM misread your intent. AutoVerus reduces proof writing time from days to minutes, but it does not replace human judgment.
What Rust code works with AutoVerus?
Code that fits the Verus subset: functions with loops, array indexing, arithmetic, and recursive structures. AutoVerus does not support async, closures, or many standard library collections. It is best suited for systems code, parsers, and algorithmic functions.
How much does AutoVerus cost to run?
The benchmark tasks cost cents per proof. A full module might cost ten to thirty dollars in API calls. This is significantly less than the 40 to 80 hours of engineering time required for manual proof writing.