Dawn Song's Team Releases Vero, First Repo-Level Formal Verification Benchmark

A team led by Dawn Song, spanning UC Berkeley and other universities, has released Vero, the first formal verification benchmark for codebase-level joint implementation and proof synthesis, designed to assess AI's ability to build formally verified software. Results show frontier models fall far short: with 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, indicating that "fully verified AI-generated software" remains in its early stages.

Confirmed

• Vero consists of 43 multi-module Lean 4 instances curated from real-world repositories in Python, Dafny, Verus, Coq and more, spanning domains such as cryptography and distributed systems; each instance includes fixed data types and API signatures (743 scored APIs in total) plus hand-curated formal specifications (2,705 in total).
• Two task modes are offered: proof-only (prove all specifications against a given reference implementation) and code-and-proof (implement each API first, then prove all specifications against your own code); both require full coverage, since any unproven specification could let slip a bug it was meant to catch.
• A built-in formal audit mechanism lets agents submit machine-checked proofs showing a specification is unsatisfiable or the reference implementation itself is flawed; this mechanism already surfaced potential errors during data curation.
• Locating the capability gap: the strongest agent can pass 87% of individual specifications yet leaves 16 repositories unfinished — the remaining specifications encode cross-module invariants that require reusable lemma libraries, which agents rarely build on their own; roughly 74% of proof lines across 82 complete solutions rely on auxiliary lemmas.

Why it matters

The team notes that existing benchmarks either target single functions or evaluate proof generation only on fixed implementations, whereas truly verified software (OS kernels, cryptographic protocols, distributed systems) exists as multi-module repositories where code, specifications, and proofs intertwine. Vero gives researchers a yardstick for progress toward "fully verified AI-generated software" and pinpoints building reusable lemma libraries as the next key bottleneck.

2026-08-23 ~ 2026-08-23 · 8 related posts

• [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