Vero: When AI Starts Proving Itself — Formal Verification and Agent Self-Awareness
Vero: Can AI Agents Build Formally Verified Software Repositories? *Authors: Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song* *arXiv: 2608.13522*
---
Prologue: Testimony Without Evidence
Imagine a courtroom. The defendant is an AI coding assistant.
Prosecutor: "You are charged with generating buggy code that crashed production, causing millions in losses."
AI: "I have no bugs. My code passes all tests."
Prosecutor: "But you haven't *proven* your code is correct. Tests can only show bugs exist — not that bugs don't."
This is the awkward position of today's AI coding assistants: they can write code quickly and elegantly, but they cannot guarantee correctness. Formal verification addresses this — not approximate confirmation through testing, but absolute guarantee through mathematical proof.
---
Chapter 1: Formal Verification — From Faith to Mathematics
In simplest terms: mathematically proving that a program does what it is supposed to do.
An analogy: testing is like trying 100 keys on a lock, failing to open it, and concluding "this lock is secure" — but you don't know about the 101st key. Formal verification is proving that the lock's internal structure makes it impossible for any key to open it — a mathematical proposition that, once proven, is absolute.
Formal verification typically involves three parts:
1. Specification: a formal-language description of what the program should do 2. Implementation: the actual code 3. Proof: a mathematical proof that the implementation satisfies the specification
Famous successes include CompCert, a compiler whose correctness was proven in Coq, and the seL4 microkernel, whose implementation was proven in Isabelle/HOL to satisfy its security specification — meaning certain classes of vulnerabilities are *mathematically impossible*, not just unlikely.
---
Chapter 2: The Trust Crisis of AI Coding Assistants
Current AI assistants (GitHub Copilot, Cursor, various agents) have three key problems:
No guarantees. Generated code may look plausible and pass unit tests, but nobody can guarantee it's bug-free. A 2023 Stanford study found programmers using AI assistants actually wrote *less secure* code — AI tends to produce plausible-looking but vulnerable code, and programmers under-trust-verify due to misplaced confidence in the AI.
Inability to see the whole picture. Existing benchmarks usually evaluate single-function generation, but real systems have multiple modules, complex interfaces, and implicit dependencies.
Specification–implementation disconnect. Existing benchmarks evaluate "generate proof for given implementation" or "generate implementation for given spec" — rarely joint generation with matching between the two.
---
Chapter 3: Vero — The First Repository-Level Verified Benchmark
Vero is the first benchmark evaluating joint implementation-and-proof generation at the repository level.
Composition
- 43 instances from real-world repositories
- 4 languages: Python, Dafny, Verus, Coq
- Domains ranging from cryptographic protocols to distributed systems
- All instances curated into Lean 4 repositories
- Prove a given specification is unsatisfiable (the spec itself is contradictory)
- Prove a reference implementation is incorrect
- For simple, modular, well-specified tasks, AI is already competent
- For complex, cross-module, deep-reasoning tasks, AI has a long way to go
- Short term (1–3 years): better single-function verification, more automated proof generation, human–AI collaborative verification workflows (AI drafts proofs, humans fill critical steps)
- Medium term (3–5 years): multi-module verification, automated specification inference, formal verification as standard practice for high-reliability software (medical, aviation, finance)
- Long term (5–10 years): AI autonomously building and verifying complex systems; "verifiable AI" becomes the norm; formal methods move from academia to industrial infrastructure
Each instance includes predetermined API interfaces, manually curated formal specifications, and reference implementations.
Two Evaluation Modes
1. Proof-Only: given an implementation, the AI generates proofs 2. Code-and-Proof: the AI generates both implementation and proof
The Audit Mechanism
Vero uniquely allows the AI to:
Like a student who can say "this exam question is flawed" — and earn credit if correct. This mechanism uncovered and corrected potential errors in specs and reference code, making the benchmark more reliable.
---
Chapter 4: The Brutal Result — 27/43
Using the strongest agent configuration (with Lean toolchain access), the researchers found:
The strongest agent fully solved only 27 of 43 instances. On the hardest repository, it closed no specifications at all.
Is this a failure? Quite the opposite — this is exactly Vero's value: it honestly tells us how far we are from "AI can build formally verified software repositories."
---
Chapter 5: Why Is This So Hard?
Layer 1 — Technical difficulty. Formal verification requires understanding dependent type theory (e.g., Lean), mastering proof tactics, handling complex type systems, and searching/backtracking extensively. Even humans proficient in Lean proofs are rare.
Layer 2 — Architectural complexity. Repository-level verification means understanding inter-module relations, ensuring interface consistency, optimizing locally under global constraints, and handling circular dependencies — an order of magnitude harder than "write a sorting function and prove it correct."
Layer 3 — Creative reasoning. Hardest of all: proofs often require creative insight — constructing auxiliary functions, introducing intermediate lemmas, applying advanced theorems. This isn't pattern matching or brute-force search; it demands genuine "understanding," much like a brilliant Go move comes from deep positional insight, not pure computation.
---
Chapter 6: A Metaphor — The Mathematical Knight and the Code Castle
Imagine a giant castle (repository) with countless rooms (modules), corridors (interfaces), and mechanisms (dependencies).
An ordinary AI coding assistant is an architect: it draws blueprints and builds walls quickly, but never checks whether the foundation is sound or people can escape a fire. It just says: "Looks good, move in and try."
A formally-verifying AI is a mathematical knight: it not only builds the castle but provides mathematical proof for every brick, wall, and vault — that they won't collapse, leak, or catch fire.
Vero is a knight's trial: given a castle with blueprints (specs), the AI must (1) build to the blueprint, (2) prove each part safe, and (3) flag flaws in the blueprint itself (audit mechanism). The strongest AI knight passed 63% of the trial — good in simple, isolated rooms; struggling in complex, interconnected halls.
---
Chapter 7: Why It Matters — The Foundation of Trust
> Can we trust AI-generated code?
Today's answer: no, at least not fully. Tests catch obvious bugs but can't guarantee absence; static analysis finds patterns but can't guarantee logic; code review depends on fallible humans.
Formal verification offers another path: absolute mathematical guarantee. If a program is formally verified, we can say: *assuming the proof system itself is sound, this program absolutely satisfies its specification.* Not "probably correct" — mathematically guaranteed.
---
Epilogue: The Shape of the Future
Vero is not just a benchmark — it's a signpost for AI-assisted software engineering:
As Feynman said:
> "The first principle is that you must not fool yourself — and you are the easiest person to fool."
Formal verification is the necessary road to truly trustworthy AI.
---
*Reference: 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.*