Vero: Can AI Agents Build Formally Verified Software Repositories? — A Feynman-Style Deep Dive

*An editorial walkthrough of the Vero benchmark (arXiv:2608.13522), exploring whether AI can become a programmer that provably never errs.*

Prologue: Why Testing Is Not Enough

The post opens with a familiar scene: two exhausted programmers testing code for the hundredth time, knowing "should work" is not "provably works." It then grounds the stakes in history: the Therac-25 radiation therapy machine (1985) killed patients due to a race condition that delivered 100x the safe dose. In safety-critical domains—flight control, pacemakers, nuclear plants, autonomous vehicles, financial engines—testing is insufficient:

• As Dijkstra noted, testing can only show the presence of bugs, not their absence.
• Complex systems have astronomically many possible states; you can never test them all.

Formal verification offers a different guarantee: a strict mathematical *specification*, an *implementation*, and a *proof* that the implementation satisfies the specification. If the proof passes, correctness holds for all inputs—a certainty like "2+2=4." The catch: formal proofs are far harder, slower, and more expensive to write than code, requiring tools like Coq, Lean, or Isabelle.

AI Coding's Missing Piece

GitHub Copilot, GPT-4, Devin, and agent frameworks boost productivity but share a fatal weakness: no correctness guarantee. AI-generated code can contain subtle logic errors, boundary-case crashes, or security vulnerabilities—and often *looks* correct. Existing "verified code generation" research has three limitations:

1. Function-level focus — real software is a system of hundreds of modules. 2. Assumes specifications are given — writing specs is itself one of the hardest tasks. 3. Toy problems — lacking real-world complexity.

What Is Vero?

Vero is the first repository-level benchmark for joint implementation and proof synthesis, titled "Can AI Agents Build Formally Verified Software Repositories?"

Composition: 43 real-world challenges

Each instance contains:

• A multi-module Lean 4 repository with real code structure (languages touched on include Python, Dafny, Verus, and Coq as ecosystem context)
• Predefined API interfaces, like an existing real project
• Human-curated formal specifications defining "correct" mathematically
• Reference implementations verified by human experts

Domains covered: cryptographic protocols (TLS, encryption, secure communication), distributed systems (consensus, databases, message queues), verified data structures (red-black trees, hash tables, graph algorithms), and systems software (filesystems, memory management, network protocols).

Two evaluation modes

• Proof-only: given code and spec, generate the proof.
• Code-and-proof: given spec and API, generate both implementation and proof (harder, closer to reality).

The Audit Mechanism: A Benchmark That Can Be Challenged

Vero's most elegant design: agents may formally prove that a specification is unsatisfiable or that a reference implementation is incorrect. Unlike one-way benchmarks (humans pose, AI answers, humans judge), Vero is bidirectional:

• If the agent completes the task → the task is valid, the agent wins.
• If the agent proves the task itself is flawed → the agent still wins, and the flawed task is flagged and removed from the benchmark.

This prevents AI from being unfairly penalized for defective tasks and continuously improves benchmark quality—a "meta-verification" approach rarely seen in benchmark design.

Results: How Far Is AI from the Perfect Programmer?

• The strongest agent configuration fully solved 27 of 43 instances (~63%)—remarkable for fully autonomous verified development.
• On the hardest repositories, zero specifications were closed—complete failure above a complexity threshold.

Where AI fails

1. Proof strategy selection — many valid proof paths exist; AI gets stuck cycling between suboptimal ones. 2. Cross-module reasoning — a module's proof may depend on another's guarantees; AI often drops preconditions across module boundaries. 3. Specification comprehension — semantic misunderstanding of abstract logical specs, like a student misreading a problem. 4. Toolchain interaction — misusing Lean 4's ecosystem, libraries, and dependencies.

Where AI succeeds

• Structured algorithm implementations (sorting, searching, stacks, queues) with abundant training patterns.
• Localized modifications to existing codebases, learning from surrounding style.
• Domains with clear mathematical definitions, like cryptography, where correctness needs less "engineering intuition."

Why Vero Matters

• From "compiles and looks right" to "provably right": evaluation via formal proofs is objective, strict, and machine-checkable—no human judgment gray areas.
• From function-level to repository-level: forcing attention to interface consistency, cross-module invariants, and global architecture.
• For AI safety: formal verification can offer deterministic guarantees about components of unpredictable AI systems—though it cannot cover compiler/hardware bugs or a wrong specification.
• New human-AI collaboration: humans define architecture, design interfaces, write high-level specs, and make creative decisions; AI fills in implementations, generates proofs, checks consistency, and refactors.

Epilogue: Open Questions

• Does AI genuinely *understand* what it proves, or merely imitate proof patterns from training data? Practically it may not matter; scientifically it touches the nature of intelligence.
• Automated mathematical discovery may follow automated verification—AI finding new theorems, not just checking existing ones.
• The most pragmatic near-term application: high-assurance software—aerospace, medical firmware, financial cores, cryptographic libraries, blockchain contracts—where AI could cut verification costs by an order of magnitude.

The places where AI stumbles on Vero—strategy selection, cross-module reasoning, specification understanding—are the same hurdles human students face learning formal methods. As the author puts it: proving correctness is itself one of the highest forms of understanding.

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.

*Explainer published August 17, 2026.*