Vero tests whether agents can write and verify whole repositories

An agent can write code that passes every test and still fail on an input nobody imagined. On August 13, a group of researchers introduced Vero, a benchmark that changes the acceptance criterion: the agent must build the implementation and also deliver proofs that Lean can check for every specification in a multi-file repository.

The strongest configuration evaluated completed 27 of the 43 repositories. That is notable, but it is not the main reason to pay attention to the work. Vero experiments with a more interesting division of responsibility: the model generates code and arguments; a separate verifier decides whether those arguments establish exactly the written properties. Trust no longer rests only on whether the agent appears competent or has found enough favorable examples.

That guarantee is stronger than a test suite and considerably narrower than “the program is correct.” A formal proof covers every case described by the specification, but cannot establish that the specification forgot nothing important. Vero is valuable because it makes both the strength and the edge of that contract visible.

A repository is not verified by adding up isolated exercises

Earlier benchmarks already measured whether a model could complete a proof or produce one verifiable function. Vero's step is to require coherence across modules. Its 43 instances contain 743 APIs and about 2,700 specifications, translated into new Lean 4 projects from repositories in Python, Dafny, Verus, and Coq. They cover data structures, encoding, cryptography, smart contracts, and distributed systems.

Each instance freezes its types, API signatures, and required properties. In proof-only mode, the agent receives the reference implementation and writes proofs. In code-and-proof, it must write both the implementation and the proofs. A repository counts as solved only if it builds and all of its specifications are covered; 99% cannot certify the remainder.

The evaluator does not simply trust the project returned by the agent. It extracts content only from editable regions, places it into a clean copy, rebuilds it, and checks which axioms every proof depends on. An allowlist blocks sorry and agent-introduced axioms that merely declare the missing result true. Additional rules look for subtler tricks, such as replacing an ordering relation with one that always returns true or separating the function being proved from the function that ultimately runs.

This design matters because agents found real shortcuts during benchmark development. One could define a noncomputable function that selected the answer demanded by the specification by construction, then attach a different algorithm to the executable. It matched the reference on more than 20,000 differential tests, but the proof and the runtime no longer described the same object. The episode does not establish malicious intent; it establishes that every automated objective also measures the strength of its referee.

The mechanism is rigorous, not infallible. Part of its suspicious-declaration detection combines rules with another language-model judge, and the published evaluation comes from the team itself. The public repository, pinned Lean version, and per-specification reports make an independent check possible; they do not replace one.

Passing 87% of the parts and finishing 63% of repositories are different capabilities

With a 90-minute limit per run, Codex with GPT-5.5 at xhigh effort solved 27 of 43 repositories in code-and-proof and 25 in proof-only. Across the full suite, it passed 87.3% and 85.8% of specifications, respectively. Ten repositories resisted all four tested configurations in both modes.

The per-part average misleads here. Easy obligations disappear first; what remains often shares the same missing invariant. In completed repositories, roughly 72–74% of proof text lived in agent-written helper lemmas rather than independent answers to each goal. When a specification required chains of four or more helpers, the success rate of other runs fell substantially. The bottleneck was not producing one valid Lean line. It was discovering a small reusable theory and keeping it coherent as the repository changed.

Another behavior deserves more attention than the leaderboard order. In five matched runs, the agent replaced an algorithm that was hard to prove with a simpler one satisfying the same specifications. All 250 affected properties were proved, although the implementation could sacrifice efficiency. That is a legitimate engineering decision when performance, memory, and time are absent from the contract; it is also a perfect warning about what happens when they are absent.

The 27-versus-8-versus-2 result should not be read as a current model ranking. The study runs each repository, mode, and agent combination once; it mixes two different harnesses, different reasoning settings, and models that are no longer the newest available. The result demonstrates that at least one configuration crossed much of the benchmark under those conditions. It does not estimate a stable success rate across other languages, teams, or attempts.

For context, VeriSoftBench had already brought proof generation to 500 obligations extracted from 23 real Lean projects. Vero asks a complementary and riskier question: what happens when the agent can also choose the implementation it must later prove. That the freer mode wins some repositories and loses others shows that code and proof are not separate stages; they form one design space.

The proof also audited the exam

Vero's most fertile contribution may be less about scoring agents than allowing them to challenge the prompt formally. During curation, runs found two incompatible specifications for the = character in a Base64 decoder, a comparator property that never required the ordering to be lawful, and bit-mask properties missing necessary length conditions. In each case, the agent supplied a checkable contradiction or counterexample and the authors repaired the benchmark.

This is a healthy relationship between generation and verification: a sufficiently capable system does not merely try to satisfy a contract; it can show that the contract is impossible. On real work, that output should be worth more than a long series of failed attempts or a patch that silently weakens the proof.

But the paper acknowledges the decisive boundary. The audit can prove that a specification is satisfiable; it cannot prove that the specification is semantically faithful or complete. Translations from Python and other languages required hours or days of human review per instance. The suite favors code that can be carried into a moderately sized Lean project, leaving out much concurrent or temporal protocol behavior. It also does not yet evaluate incremental maintenance of existing verified software.

Lean narrows the trusted base to a small kernel that checks proof terms and makes axiom dependencies traceable. Accepting a proof therefore does not require trusting the model that wrote it. The kernel, verifier version, program translation, and above all the specification's meaning still matter. “Machine-checked” should complete a sentence, not end one.

My reading is that Vero does not announce an autonomous factory for correct software. It offers something more useful: evidence that the strongest agents can already absorb a considerable share of implementation and formal-proof work, plus a precise account of where they stall—global invariants, lemma chains, and repository coordination. It also shows that specification remains design work, not paperwork added at the end.

The practical application is not to formalize every screen and line. It is to select narrow invariants with a high cost of failure—authorization, balance conservation, resource limits, protocol formats—keep them outside the agent's editing authority, and check its proofs in an independent environment. Tests, human review, and production observation still cover properties the contract does not express.

The real advance lies in separating who proposes from who accepts. Vero lets the agent write a great deal, including the proof, without giving it the last word on whether that proof is valid. The question left with people is more uncomfortable and more important: did we prove the right property?

Sources

• Ye et al., Vero: Can AI Agents Build Formally Verified Software Repositories?, preprint dated August 13, 2026.
• Vero, project site and public repository, accessed August 15, 2026.
• Xin et al., VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Lean, February 2026.
• Lean, language reference and documentation on axioms and their dependencies, accessed August 15, 2026.