Vero: Can AI Agents Build Formally Verified Software Repositories?

Vero is the first benchmark to evaluate joint implementation and proof synthesis at the repository level in Lean 4. It contains 43 multi-module instances curated from real-world repositories spanning Python, Dafny, Verus, and Coq, covering domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. The benchmark includes 743 scored APIs and 2,705 specifications. Vero also includes an audit mechanism where agents can formally prove unsatisfiability of provided specifications or incorrectness of reference code, which surfaced 38 adjudicated specification defects across 9 instances during curation. Evaluation of frontier coding-agent configurations with Lean toolchain access shows the strongest agent fully solves only 27 of 43 instances in code-and-proof mode, and 10 instances resist every configuration in both modes. The gap is not local proof skill—the strongest agent passes over 80% of individual specifications—but repository-scale organization: agents fail to discover shared invariants, build reusable lemma libraries, and keep the whole repository consistent and buildable. The benchmark, curation pipeline, and evaluation harness are released at https://github.com/sunblaze-ucb/vero.

Improvements to AI systems:

1. Repository-scale invariant discovery: Train models to infer and propagate shared invariants across multiple modules before writing proofs, rather than solving each specification in isolation. The improved system can automatically identify cross-module dependencies and generate a global lemma library that reduces redundant proof effort.

2. Iterative build-aware proof synthesis: Implement a feedback loop where the AI checks repository buildability after each proof step and re-plans when compilation fails. The improved system can maintain a consistent, compiling Lean 4 repository throughout the proof process, avoiding cascading errors from broken intermediate states.

3. Specification defect detection: Add a meta-reasoning layer that actively tests whether provided specifications are satisfiable and whether reference code is correct, using Lean's kernel to verify contradictions. The improved system can flag and formally prove specification bugs, then adapt its proof strategy to work around or repair them.

4. Cross-language abstraction transfer: Train on multi-language instances (Python, Dafny, Verus, Coq) to learn language-agnostic proof patterns (e.g., induction, case analysis, invariant strengthening) that can be instantiated in Lean 4. The improved system can reuse high-level proof strategies from other formal verification ecosystems.

5. Hierarchical proof planning: Decompose repository-level proofs into a dependency graph of API-level lemmas, then prioritize proving foundational lemmas first. The improved system can allocate time and context window to critical shared lemmas, reducing failure on downstream specifications that depend on them.

6. Self-consistency auditing for repository coherence: After generating proofs, run an automated audit that checks for unused assumptions, inconsistent definitions, or missing imports across modules. The improved system can produce a fully verified, self-contained repository with no dangling references or hidden axioms.

What the improved AI system can do:

• Solve all 43 Vero instances in code-and-proof mode, including the 10 that currently resist all configurations.

• Automatically discover and formalize shared invariants (e.g., global state consistency in distributed systems) without human hints.

• Repair faulty specifications or reference code by providing machine-checkable counterexamples or unsatisfiability proofs.

• Generate reusable Lean 4 lemma libraries that generalize to unseen repository-level verification tasks.

• Maintain a continuously compiling repository during multi-hour proof sessions, with rollback and replanning on any build failure.

AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. Verified code generation, in which an agent produces both an implementation and a machine-checked proof of its specification, offers a stronger path toward trustworthy AI-generated software. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.