Dawn Song's Team Releases Vero, First Repository-Level Formal Verification Benchmark
Dawn Song's team (UC Berkeley and partner universities) released Vero, the first repository-level benchmark for joint implementation and proof synthesis, designed to evaluate AI's ability to build formally verified software. Frontier models fall far short: under a 90-minute budget, the best configuration, GPT-5.5 (xhigh reasoning, code-and-proof mode), fully verified only 27 of 43 repositories (25 in proof-only mode), and 10 repositories failed under every configuration, showing that fully verified AI-generated software remains in its infancy.
Confirmed
- Vero consists of 43 multi-module Lean 4 instances curated from real-world repositories in Python, Dafny, Verus and Coq, spanning cryptography and distributed systems; each instance fixes data types and API signatures (743 scored APIs) with hand-curated formal specs (2,705 total).
- Two task modes: proof-only (prove all specs against a given reference implementation) and code-and-proof (implement each API, then prove all specs against one's own code); both require full coverage, as any unproven spec could miss the bug it was meant to catch.
- A built-in formal audit mechanism lets agents submit machine-checked proofs that a spec is unsatisfiable or a reference implementation is wrong; this mechanism already caught potential errors during data curation.
- Capability gap: the strongest agent passes 87% of individual specs but leaves 16 repositories incomplete—the remaining specs encode cross-module invariants requiring reusable lemma libraries that agents rarely build; across 82 full solves, roughly 74% of proof lines rely on auxiliary lemmas.
Why it matters
The team argues that as AI agents write more software, code that merely runs is not enough—machine-checkable correctness and security guarantees are needed. Existing benchmarks target single functions or proof generation on fixed implementations, while real verified software (OS kernels, cryptographic protocols, distributed systems) lives in multi-module repositories where code, specs and proofs interleave. Vero gives researchers a yardstick for progress toward fully verified AI-generated software and identifies reusable lemma-library construction as the key bottleneck.
2026-08-23 ~ 2026-08-24 · 9 related posts
Primary sources
- Vero: First Benchmark for Repository-Scale Formal Verification by AI Agents — dawnsongtweets ·
- Vero shows the gap: agents rarely build reusable lemma libraries (74% of proof lines) — dawnsongtweets ·
- GPT-5.5 fully verifies only 27/43 repos; 10 unsolved across all 8 configs — dawnsongtweets ·
- [source] Vero: First Benchmark for Repository-Scale Formal Verification by AI Agents — dawnsongtweets · 2026-08-23
- Why repo-level verification: single-function benchmarks miss real software — dawnsongtweets · 2026-08-23
- Vero composition: 43 Lean 4 repos, 743 APIs, 2,705 formal specs — dawnsongtweets · 2026-08-23
- Vero's two task modes: proof-only and code-and-proof, both requiring full coverage — dawnsongtweets · 2026-08-23
- [source] GPT-5.5 fully verifies only 27/43 repos; 10 unsolved across all 8 configs — dawnsongtweets · 2026-08-23
- [source] Vero shows the gap: agents rarely build reusable lemma libraries (74% of proof lines) — dawnsongtweets · 2026-08-23
- Dawn Song's Team Releases Vero Benchmark for AI-Generated Formally Verified Software — dawnsongtweets · 2026-08-23
- Vero includes formal audit mechanism for machine-checked spec errors — dawnsongtweets · 2026-08-23
- New Vero Benchmark Shows Top Agent Fully Verifies Only 63% of Repos — shizhediao · 2026-08-24