A UC Berkeley team released Vero on August 13, 2026 — the first benchmark to evaluate whether AI agents can produce formally verified software at the repository level. The benchmark generates both Lean 4 implementations and machine-checked proofs that implementations satisfy their specifications. The strongest frontier agent fully solves only 27 of 43 instances and closes zero specifications on the hardest repositories.
Vero's 43 instances are sourced from real-world codebases originally written in Python, Dafny, Verus, and Coq, spanning cryptographic protocols to distributed systems. Each instance is a self-contained multi-module Lean 4 project. Curators freeze three layers — shared data types, API signatures, and formal specifications — and the agent writes implementations and discharges proofs. Every instance is manually translated to Lean 4 with no online ground truth, preventing training-data contamination.
The benchmark runs in two modes. Proof-only mode supplies a reference implementation; the agent must prove every spec against it. Code-and-proof mode withholds the reference and the agent writes both from scratch. The grading harness renders a clean Lean project from frozen source, overlays the agent's proof bodies, compiles with Lake, and checks each proof's axiom set against an allowlist. A proof leaking a `sorry` placeholder or foreign axiom does not count. The CLI is simple: `vero run benchmark=bankledger agent=claude mode=proof` writes per-spec reports with axiom breakdowns to `agent_runs/<run>/eval/<name>/report.md`.
| Mode | What Agent Receives | Agent Must Produce | Grading Target |
|---|---|---|---|
| Proof-only | Frozen types + API signatures + specs + reference implementation | Proof bodies for all specifications | Every spec proved against the supplied implementation; no sorry or foreign axioms |
| Code-and-proof | Frozen types + API signatures + specs only (no reference implementation) | Full Lean 4 implementation + all proof bodies | Full Lake compilation + axiom-clean proofs for all specs |
The prior function-level benchmark VERINA — from the same lead author — showed OpenAI o3 achieving 72.6% code correctness, 52.3% specification soundness, and 4.9% proof success on a single trial per task. Vero asks whether agents maintain coherent implementation and proof choices across multi-module codebases, not just at function boundaries. The answer: even the strongest agents fail on more than a third of instances and collapse on the hardest ones.
Rather than silencing benchmark errors, Vero gives agents formal slots to prove a specification unsatisfiable or reference code incorrect. That turned latent curation bugs into machine-checked findings during construction — a technique directly applicable to CI pipelines in codegen workflows where specs may be misstated rather than the agent at fault.
Proof-synthesis collapses when module boundaries introduce cross-file dependencies. Agents fail to maintain consistency between implementation choices in one file and proof obligations in another. The 27/43 full-solve rate obscures the harder truth: zero specifications closed on hardest instances. Agents hit a ceiling that more prompting or token budget will not clear.
If evaluating codegen agents for safety-critical pipelines, "does it compile and pass tests" is not sufficient. Vero provides a reproducible harness to add "does it close its proofs without sorry" to your evaluation suite, available today on Python 3.10 with Lean 4.29.1.