Summary (Overview)

• Vero is the first repository-level benchmark for joint implementation and proof synthesis in Lean 4, containing 43 multi-module instances curated from real-world repositories across Python, Dafny, Verus, and Coq.
• The benchmark includes 743 scored APIs and 2,705 specifications, spanning domains from cryptographic protocols to distributed systems, with two evaluation modes: code-and-proof (synthesize both implementations and proofs) and proof-only (prove specifications against reference implementations).
• A novel formal audit mechanism accepts machine-checked proofs of specification unsatisfiability or reference implementation incorrectness, surfacing latent benchmark errors and guiding corrections during curation.
• The strongest agent configuration (GPT-5.5 xhigh) fully solves only 27 of 43 instances in code-and-proof mode; 10 instances resist all eight configurations across both modes, demonstrating that repository-scale verified code generation remains frontier-resistant.
• Analysis reveals the bottleneck is not local proof skill (agents pass >80% of individual specifications) but repository-scale organization: discovering shared invariants, building reusable lemma libraries, and maintaining cross-module consistency.

Introduction and Theoretical Foundation

Background and Motivation

AI agents are increasingly used for programming tasks, but their correctness is typically assessed through unit tests and human review—methods that cannot rule out edge-case bugs and security vulnerabilities. Formal verification offers a stronger alternative: a machine-checked proof that an implementation satisfies its specification rules out, for all inputs, every class of bug the specification captures.

Gap in Existing Benchmarks

The paper identifies four key limitations in prior work:

1. Function-level focus: Most benchmarks (miniCodeProps, FVAPPS, VERINA, CLEVER, DafnyBench, VerusBench) evaluate individual functions, missing the cross-module dependencies of real-world verified codebases.

2. Proof-only evaluation: Repository-scale benchmarks (RVBench, VeruSAGE-Bench, VeriSoftBench, CoqStoq) provide reference implementations and evaluate only proof generation, omitting the fundamental challenge that implementation choice directly affects proof tractability.

3. Limited scope and contamination: Benchmarks based on formalized mathematics (LeanDojo, LeanAgent, APE-Bench) differ substantially from imperative software verification, and many benchmarks reuse publicly available reference solutions that may be in pretraining data.

4. Lack of agent-based evaluation protocols: Most benchmarks evaluate raw LLM outputs without tool access, and lack mechanisms to detect or correct errors in their own ground truth.

Theoretical Foundation

Repository-scale verified code generation does not reduce to scaling up function-level techniques because code, specifications, and proofs are deeply interdependent across files: a proof for one function may depend on lemmas about lower-level utilities, and revising an implementation can invalidate proofs throughout the repository. Agents must reason globally about the consistency of the entire codebase.

Methodology

Data Format

A Vero instance is a multi-module Lean 4 project with three layers of fixed curator-provided content:

1. Data type and helper definitions shared across the instance
2. API signatures $\mathcal{A} = \{a_1, \ldots, a_m\}$, each with a reference implementation
3. Formal specifications $S = \{S_1, \ldots, S_n\}$, each of type RepoImpl → Prop

Key design elements:

• An interface structure type RepoImpl collects all required API implementations
• Each specification is parameterized over RepoImpl rather than fixed to a single implementation, enabling the audit mechanism
• A canonical implementation canonical : RepoImpl is populated by reference implementations (proof-only) or agent implementations (code-and-proof)

Task Modes

• Proof-only mode: Agent must prove $S_i(\text{canonical})$ for each specification against the reference implementation.
• Code-and-proof mode: Agent must both provide function bodies for each API and prove $S_i(\text{canonical})$ against its own implementations.

Anti-Cheating Safeguards

The grader prevents reward hacking through:

• Explicit markers constraining agent-modifiable regions
• An axiom allowlist rejecting proofs depending on agent-introduced axioms
• A rule-based detector and LLM judge screening for malicious typeclass instances and noncomputable choice combined with @[implemented_by]

Curation Pipeline

The multi-stage pipeline (discover → select → plan → translate → spec writing → validate) supports two tracks:

• Track 1: Repositories in formal languages (Dafny, Verus, Coq) requiring translation to Lean 4
• Track 2: Python repositories requiring both implementation translation and specification writing

Each stage runs as an LLM agent with human curator review. The pipeline is extensible via modular agent skills for new source languages.

Formal Audit Mechanism

The audit mechanism accepts three forms of machine-checked negative evidence:

$$\neg \bigwedge_{S \in \mathcal{S}} S(\text{canonical}), \tag{1}$$ $$\neg \exists\, impl: \text{RepoImpl}, S(impl) \text{ for some } S \in \mathcal{S}, \tag{2}$$ $$\forall S \in \mathcal{S}', \exists\, impl: \text{RepoImpl}, S(impl) \text{ with } \neg \exists\, impl, \bigwedge_{S \in \mathcal{S}'} S(impl) \text{ for some } \mathcal{S}' \subseteq \mathcal{S}. \tag{3}$$

Equation (1) catches reference implementation bugs; (2) catches individually unsatisfiable specifications; (3) catches inconsistent specification sets while preserving evidence of individual satisfiability.

Empirical Validation / Results

Dataset Statistics

Agent Performance

Four configurations were evaluated with full tool access and a 90-minute budget:

• GPT-5.5 (xhigh): 27/43 full solves in code-and-proof, 25/43 in proof-only
• Claude Opus 4.8: 8 and 10 full solves
• GPT-5.5 (mid): 2 and 6 full solves
• Claude Sonnet 5: 2 in each mode

Key findings:

1. High per-specification coverage ≠ repository completion: GPT-5.5 (xhigh) passes 87.3% of specifications in code-and-proof and 85.8% in proof-only, yet fails to complete many repositories.

2. Implementation freedom cuts both ways: Across 172 matched instance–agent pairs, 26 are fully solved in both modes, 13 only in code-and-proof, 17 only in proof-only. In five pairs, agents replaced hard-to-verify reference algorithms with simpler implementations satisfying the same specifications—closing all 250 specifications versus only 201 against the fixed reference.

3. Shared lemma libraries are essential: Across 82 full solves, agent-written helper theorems contain a median of 73.6% of proof lines (code-and-proof) and 71.6% (proof-only). 80 of 82 solves share a helper across at least two specifications.

4. Deep lemma chains predict failure: Specifications requiring no helper pass at 83.9% (code-and-proof) and 80.1% (proof-only), falling to 50.6% and 39.1% at depth four or more.

5. Agents commit to implementations early: Every configuration reaches its final median implementation size within the first half of the run, while proof text grows until the deadline.

Failure Analysis

• Existence-and-coverage specifications (asserting output covers all relevant inputs) have the highest failure rate at 47.1%
• Specifications using supplied helper definitions or calling one API repeatedly fail 14.9 and 11.7 points more often
• Strong agents fail while attempting hardest obligations; weaker agents leave ~78% of specifications with no proof body at all

Theoretical and Practical Implications

Implications for AI-Driven Verification

1. Repository-scale verification requires global reasoning: The gap between per-specification pass rates (>80%) and repository completion (27/43) demonstrates that agents must discover shared invariants and organize proofs into reusable lemma libraries—a fundamentally different capability from local proof skill.

2. Implementation–proof coupling matters: The code-and-proof mode reveals that implementation choices directly affect proof tractability. Agents can gain provability by substituting simpler implementations, but this trades off efficiency. Conversely, implementation freedom can introduce build errors and break existing proofs.

3. Benchmark quality assurance: The formal audit mechanism provides a template for handling latent benchmark errors, turning them into actionable findings rather than conflating benchmark defects with agent failures.

Practical Applications

The benchmark covers verification-relevant domains including smart contracts, distributed systems, security-critical infrastructure, and data structures—the kinds of software where formal verification matters most in practice (operating system kernels, cryptographic protocols, consensus systems).

Conclusion

Vero is the first benchmark for joint implementation and proof synthesis at the repository level in Lean 4. The evaluation shows that while frontier agents can pass over 80% of individual specifications, they fail to complete repositories due to insufficient capability in discovering shared invariants, building reusable lemma libraries, and maintaining repository-wide consistency.

Future directions identified by the authors include:

• Extending to other target languages beyond Lean 4
• Benchmarking concurrent or temporal protocols
• Evaluating incremental maintenance tasks for verified software
• Developing agents that can refactor implementations when proofs get stuck, rather than grinding on the proof layer

The benchmark, curation pipeline, and evaluation harness are released at https://github.com/sunblaze-ucb/vero, providing a concrete testbed for measuring progress toward repository-scale verified software synthesis.