An AI Agent with Verus

Formal verification and LLM agents look like a natural pair: the agent proposes, the verifier decides. I wanted to know what that pairing buys in practice, so I tried it on 14 open-source Rust crates, most of them widely used, with Verus as the verifier. The full list is at the end.

I measured two jobs separately: proving that code is correct, and finding bugs in it.

All agents ran Claude Opus 5.5 with the same settings in every arm, and the verifier was Verus 0.2026.10.26. These results are for one model; a weaker model might gain more from the verifier.

Proving correctness: worth it

The Verus decider (the setup is below) ported each library function into Verus faithfully, turned each property into a Verus spec, and proved 136 of them for every possible input. Examples: formatting and re-parsing a duration gives back the same value for every 64-bit seconds count, and a hex encoder leaves its output buffer untouched whenever it fails. Tests can only sample inputs, so for these properties the test-only agent could never say more than “probably fine”.

The catch is that a verifier will also happily “prove” nonsense. In three cases a result reported as verified was not: a theorem whose premise could never hold, a set of axioms that contradicted each other, and a proof that leaned on a guarantee the verifier had itself rejected. A separate skeptic agent caught all three. The checks I now treat as mandatory:

  • a negative control for every proof (ensures false under the same assumptions must fail);
  • every axiom checked against the real code, exhaustively where the domain is finite;
  • an independent review that the ported model behaves like the original.

Finding bugs: a tie, once the baseline was fair

Getting a bug-hunting setup worth measuring took six iterations. The first versions were elaborate: a spec writer that never saw the code, auditors attacking the spec and the ported model, five independent specs merged by vote, even the git history as a source of intent. Each version changed one thing so I could see what helped. Most of the machinery didn’t. The specs grew, the auditors trimmed most of the growth back, and recall stayed low. The design that worked was the simplest one.

The bug-hunting loop A hunter agent reads the crate and proposes properties to check. The same properties go to two deciders, one using Verus and one using tests only. A skeptic agent, blind to which decider reported a bug, judges every claimed bug. The output is confirmed bugs, each with a failing test. Hunter agent reads tests, docs and code Verus decider ports, specs, proves Test decider test and reason Skeptic agent blind to which decider reported it reruns the test, checks the promise Confirmed bugs each with a failing test same properties to both

In that design, one agent proposed suspicious properties. Two agents then decided each one: one with Verus, one with tests only. The bugs were real (dozens, each with a failing test, about a third already reported upstream), but Verus rarely made the difference. The bugs came from the agent reading the code.

Once, it looked like Verus had won. It confirmed a subtle bug in a random number generator that the test-only agent gave up on. Before believing it, I preregistered a rerun and told the test-only agent to reason mathematically and not stop early. It found the bug three times out of three. The Verus agent found it two times out of three. The “win” came from a weak baseline.

What I take from it

  1. Use the verifier for proof, not search. Its value is a guarantee over all inputs, which nothing else gives you.
  2. Check the proofs. “Verified” means little until a negative control fails and the axioms are checked.
  3. Make the baseline try hard. A tool can look great against an agent that gives up early.

Crates tested