Vero Benchmark: Can AI Agents Build Formally Verified Software Repositories?

Forum topic · 小凯 · 2026-08-16

Summary

Vero is a new benchmark that evaluates whether AI agents can jointly generate code and formal proofs at the repository level, moving beyond single-function verification tasks. It comprises 43 multi-module instances drawn from real-world open-source projects, written primarily in Lean 4, with application domains including cryptography, distributed systems, data structures, and systems software. Vero supports two evaluation modes: proof-only (given an implementation, generate the proof) and code-and-proof (generate both from a specification and API). Uniquely, Vero features an audit mechanism that lets AI agents formally challenge benchmark tasks—proving a specification unsatisfiable or a reference implementation incorrect—flagging flawed tasks for removal. Experiments with state-of-the-art agent configurations solved 27 of 43 instances (~63%), while completely failing on the hardest repositories. Failure analysis identifies four bottlenecks: proof strategy selection, cross-module reasoning, specification understanding, and toolchain interaction. Vero signals a shift in AI software engineering from generating plausible code toward mathematically provable correctness, with implications for AI safety and high-assurance software development in safety-critical domains.

Feynman-Style Analysis: Can AI Become a Programmer Who Never Makes Mistakes?

This post is a Chinese forum author's popular-science walkthrough of the Vero benchmark (arXiv:2608.13522): *Can AI Agents Build Formally Verified Software Repositories?* Below is a full English rendition of the article's content.

Prologue: Why Testing Isn't Enough

Testing can only show the presence of bugs, not their absence (Dijkstra). The 1985 Therac-25 radiation therapy accidents—caused by a race condition delivering massive overdoses—showed that software bugs can kill. In safety-critical domains (flight control, pacemakers, nuclear plants, autonomous driving, financial systems), "we tested many times and found nothing" is insufficient.

Formal verification takes a different approach:

Specification: describe what a program should do in rigorous mathematical language
Implementation: write the actual code
Proof: mathematically prove the implementation satisfies the specification

The problem: formal verification is hard, slow, and expensive—writing proofs requires specialized training in tools like Coq, Lean, and Isabelle, and can cost several times the coding effort itself.

AI Programming's Missing Piece

AI coding tools (GitHub Copilot, GPT-4, Devin, agent frameworks) boost productivity but share a fatal weakness: no correctness guarantee. AI-generated code can contain subtle logic errors, edge-case crashes, or security vulnerabilities—and often *looks* correct while hiding the most dangerous bugs.

Existing verification research has further limits:

Focuses on single functions, not full systems
Assumes specifications are already provided
Uses toy problems far from real-world complexity

What Is Vero?

Vero is the first benchmark to evaluate AI's joint implementation and proof synthesis at the repository level.

Composition

43 multi-module instances from real-world open-source projects
Languages: Python, Dafny, Verus, Coq, and primarily Lean 4
Domains: cryptographic protocols (TLS, encryption), distributed systems (consensus, databases, queues), verified data structures (red-black trees, hash tables, graph algorithms), and systems software (file systems, memory management, networking)
Each instance includes a multi-module Lean 4 repository, preset API interfaces, human-curated formal specifications, and reference implementations

Two Evaluation Modes

Proof-only

Code-and-proof

The Audit Mechanism: Benchmark Self-Correction

Vero's most innovative design: AI agents may formally prove that a specification is unsatisfiable or a reference implementation is incorrect. If the challenge succeeds, the AI still gets credit—and the flawed task is flagged and removed from the benchmark. Like an exam where students may point out a faulty question, and the teacher revises it. This prevents unfair judgment of AI and continuously improves benchmark quality.

Results: How Far Is AI from the "Perfect Programmer"?

The strongest AI configuration fully solved 27 of 43 instances (~63%)
On the hardest repositories, no specifications were closed (total failure)

Where AI Falls Short

Proof strategy selection

Cross-module reasoning

Specification understanding

Toolchain interaction

Where AI Succeeds

Structured, classic algorithm/data-structure implementations
Localized modifications to existing codebases (vs. building from scratch)
Domains with clear mathematical definitions (cryptography, data structures)

Why Vero Matters

From "writing code" to "writing provably correct code" — a qualitative shift, like moving from "the car runs" to "the car passed all crash tests"
From function level to repository level — forcing attention on interface consistency, cross-module invariants, and architecture
From human judgment to machine-verifiable evaluation — formal proofs are objective, strict, and reproducible

AI Safety Implications

A New Human-AI Collaboration Model

Epilogue: Open Questions

Does AI truly "understand" what it proves, or is it imitating proof patterns from training data? Practically it may not matter; scientifically it touches the nature of intelligence.
Automated mathematical discovery: if AI masters verification, could it next discover new theorems rather than just verify conjectures?
Most practical near-term application: high-assurance software—aviation, medical firmware, financial systems, cryptographic libraries, blockchain smart contracts—where AI could cut verification costs by an order of magnitude.

References

Ye, Z., Lou, H., Sun, Y., Song, P., Yan, Z., Kasriel, T., Zhang, Q., Yang, K., Kong, S., He, J., & Song, D. (2026). Vero: Can AI Agents Build Formally Verified Software Repositories? arXiv preprint arXiv:2608.13522.
Leino, K. R. M. (2010). Dafny: An Automatic Program Verifier for Functional Correctness. LPAR 2010.
De Moura, L., & Ullrich, S. (2021). The Lean 4 Theorem Prover and Programming Language. CADE 2021.
Bertot, Y., & Castéran, P. (2013). Interactive Theorem Proving and Program Development: Coq'Art. Springer.
Dijkstra, E. W. (1972). The Humble Programmer. Communications of the ACM, 15(10), 859-866.
Leroy, X. (2009). Formal Verification of a Realistic Compiler. Communications of the ACM, 52(7), 107-115.