Vero: Can AI Agents Build Formally Verified Software Repositories?

AI summary

Overview

Research area: Machine learning / AI coding agents, with a focus on formal verification and benchmark construction (arXiv category cs.LG).

Technical level: Advanced. The paper assumes familiarity with interactive theorem provers and specification languages, though the central question is stated plainly.

Scope: The paper introduces Vero, a repository-scale benchmark of 43 multi-module Lean 4 instances drawn from real-world Python, Dafny, Verus, and Coq repositories, and uses it to measure whether frontier coding agents can jointly synthesize implementations and machine-checked proofs.

What This Paper Is About

AI agents are increasingly used to write software, but their output is normally checked with unit tests and human review, which cannot rule out edge-case bugs and security vulnerabilities. Formal verification offers a stronger guarantee: a machine-checked proof that an implementation satisfies its specification for all inputs. Existing benchmarks for verified code generation either target individual functions or evaluate only proof generation given a fixed implementation, so it remained an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. Vero is built to answer that question at the repository level.

Key Contributions

1. A repository-scale benchmark. Vero is presented as the first benchmark for verified code generation in Lean 4 at the repository level, comprising 43 instances curated from real-world repositories across Python, Dafny, Verus, and Coq, together with a semi-automated, multi-language curation pipeline that supports its construction and future extension.
2. A formal audit mechanism. A separate formal-evidence path accepts machine-checked proofs of specification unsatisfiability or reference implementation incorrectness, turning latent benchmark defects into actionable findings and enabling continuous quality improvement as agents grow more capable.
3. A comprehensive evaluation. Four frontier model configurations under two coding-agent harnesses are evaluated on Vero across two task modes, producing baselines and analyses of where agents succeed and fail.
4. Two task modes plus anti-cheating safeguards. Instances support both a proof-only mode and a code-and-proof mode, with an axiom allowlist, editable-region markers, and detectors for mechanisms that could trivialize proofs.

Main Findings

• Vero is frontier-resistant. The strongest configuration, GPT-5.5 (xhigh), fully solves only 27 of 43 instances in code-and-proof mode and 25 in proof-only mode. Claude Opus 4.8 solves 8 and 10, GPT-5.5 (mid) solves 2 and 6, and Claude Sonnet 5 solves 2 in each mode. Ten instances resist all eight configurations across both modes.
• High per-specification coverage does not imply repository completion. GPT-5.5 (xhigh) passes 87.3% of specifications in code-and-proof and 85.8% in proof-only, yet fails to close whole repositories. It progresses fastest, reaching 25 and 23 full solves within 45 minutes of the 90-minute budget.
• Implementation freedom matters through the proof target. Across 172 matched instance–agent pairs, 26 are fully solved in both modes, 13 only in code-and-proof, 17 only in proof-only, and 116 in neither. In five instance–agent pairs across three repositories, the agent replaced a hard-to-verify reference algorithm with a simpler implementation satisfying the same specifications; those five pairs close all 250 specifications, whereas proving against the fixed reference in proof-only closes only 201.
• Proof volume separates full solves from unfinished runs. Fully solved and unfinished runs write similar amounts of implementation code, while full solves contain roughly twice the proof text and higher proof-to-implementation ratios.
• Completed repositories rely on shared lemma libraries. Across the 82 full solves, agent-written helper theorems contain a median of 73.6% of proof lines in code-and-proof and 71.6% in proof-only. Of the 82 solves, 80 share a helper across at least two specifications and 65 across at least five.
• Deep lemma chains predict where other agents fail. Specifications requiring no helper pass at 83.9% in code-and-proof and 80.1% in proof-only, falling to 50.6% and 39.1% at helper-chain depth four or more.
• Agents commit to implementations early and grow proofs until the deadline. Every configuration reaches its final median implementation size within the first half of the run. GPT-5.5 (xhigh) fixes its median 65 implementation lines by minute 30 and then grows proof text from 883 to 1,077 lines; Claude Sonnet 5 adds only 5 implementation lines after minute 60 while its proof text nearly doubles.
• Failure reasons differ by agent strength. A third of GPT-5.5 (xhigh)'s remaining specifications fail at build time and a further 14% are rejected as cheating, whereas Claude Opus 4.8 and Claude Sonnet 5 leave roughly 78% of theirs with no proof body at all. Only 6 of GPT-5.5 (xhigh)'s 16 unfinished code-and-proof repositories are within five specifications of completion, and nine have more than ten left.
• Global and definition-heavy specifications fail most. Existence-and-coverage specifications have the highest failure rate at 47.1%. Within repositories, specifications that use a supplied helper definition fail 14.9 points more often and those that call one API repeatedly fail 11.7 points more often, while merely referencing several APIs or another module adds little.
• The audit mechanism caught real defects. During curation it surfaced several latent errors that had escaped manual review, using formal witnesses such as counterexamples to guide correction.

Methodology in Plain English

Each Vero instance is a multi-module Lean 4 project in which the curator fixes three layers: data type and helper definitions, API signatures (each with a reference implementation), and formal specifications. Every specification is written as a predicate over a RepoImpl interface structure that collects all required API implementations, and a canonical value is either instantiated from the reference implementations or filled in by the agent. The agent must discharge an implementation obligation for each API and a proof obligation for each specification. In proof-only mode the reference implementations are provided and the agent proves only; in code-and-proof mode the agent supplies both.

Instances were built through a multi-stage pipeline in which each stage runs as an LLM agent and is reviewed by a human curator before the next stage begins. Track 1 covers repositories already written in Dafny, Verus, or Coq, where existing types, definitions, and specifications are translated into Lean 4. Track 2 covers non-formal repositories, typically Python, where implementations are translated and specifications are also written. The stages are discover, select, plan, translate, spec writing (Track 2 only), and validate. Pipeline stages are implemented as modular agent skills with source-language rules for Python, Dafny, Verus, and Coq.

Evaluation uses Codex (v0.140.0) with GPT-5.5 at default (medium) and xhigh reasoning effort, and Claude Code (v2.1.191) with Claude Opus 4.8 and Claude Sonnet 5 at xhigh reasoning effort. All agents have full tool access, including file-system edits, build invocations, and the Lean v4.29.1 toolchain with lake build. Scoring counts fully solved instances rather than partial specification coverage. Anti-cheating measures include explicit markers limiting the regions agents may modify, an axiom allowlist, and a rule-based detector plus an LLM judge screening for proof-trivializing mechanisms such as malicious typeclass instances and noncomputable choice combined with @[implemented_by].

Why This Matters

Research impact. Vero shifts evaluation of verified code generation from single functions to whole repositories, where code, specifications, and proofs are interdependent across files. It provides concrete evidence that current agents lack repository-scale organization, and it supplies an audit mechanism that lets a benchmark correct its own ground truth using machine-checked negative evidence.

Real-world applications (domains the benchmark covers):

• Cryptographic protocols and blockchain smart contracts, where edge-case bugs and security vulnerabilities are most damaging.
• Distributed systems and consensus, where consistency properties span modules.
• Security-critical parsing and encoding infrastructure.
• Core data structures, algorithm collections, and numerical utilities.

Industry relevance. AI agents are already used in software engineering tasks, and their correctness is typically assessed by tests and human review. The paper reports aggregate evaluation cost per configuration, from $633 (Claude Sonnet 5, code-and-proof) and $791 (Claude Sonnet 5, proof-only) to $2,865 (GPT-5.5 (xhigh), code-and-proof) and $2,964 (GPT-5.5 (xhigh), proof-only), summed over all 43 instances. Since the strongest agent fully solves only 27 of 43 instances, the results indicate that automated production of verified software at practical scale remains out of reach for current systems.

Future Directions

• Extension beyond Lean 4. Vero currently targets Lean 4 only. Track 1 already translates Dafny, Verus, and Coq projects, and the curation pipeline is described as extensible to other target languages, but this is left to future work.
• Concurrent and temporal protocols. The corpus favors code that translates cleanly into Lean; the main absent class is concurrent or temporal protocols whose upstream formalizations do not port to a Lean scaffold of moderate size.
• Incremental maintenance tasks. Benchmarking formal verification of incremental maintenance tasks is identified as a valuable future direction.
• Semantic correctness of specifications. The audit mechanism certifies formal satisfiability but cannot ensure specifications are semantically correct or complete, so specifications are manually reviewed and Track 1 specifications are additionally cross-checked against source-language formalizations. The paper also points to helping agents discover shared invariants, build reusable lemma libraries, and refactor implementations into more provable forms rather than grinding on the proof layer.

Target Audience

Researchers working on AI coding agents, neural theorem proving, and verified code generation; developers and tool builders in formal verification (Lean 4, Dafny, Verus, Coq); and teams evaluating whether agents can be trusted with correctness-critical software such as protocols, distributed systems, and security infrastructure. Readers interested in benchmark design and ground-truth auditing will also find the curation pipeline and formal audit mechanism relevant.

Authors’ abstract

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.