vero-can-ai-agents-build-formally-verified-software-repositories
Extract — Vero: Can AI Agents Build Formally Verified Software Repositories?
Section titled “Extract — Vero: Can AI Agents Build Formally Verified Software Repositories?”- URL: https://arxiv.org/abs/2608.13522 (HTML: https://arxiv.org/html/2608.13522 ; PDF: https://arxiv.org/pdf/2608.13522)
- Authors: Zhe Ye et al. (Caltech / Stanford / UC Berkeley / Apodex / AWS / UChicago)
- arXiv: 2608.13522v1 (submitted 2026-08-13)
- Code: https://github.com/sunblaze-ucb/vero
- Read via: defuddle (abs + html/experimental)
Claims
Section titled “Claims”- First repo-level bench for joint code+proof in Lean 4: agents must fill API implementations and prove all specs, not only complete proofs against a fixed impl.
- 43 multi-module Lean 4 instances from real repos (Python, Dafny, Verus, Coq); 743 scored APIs, 2,705 specs. Two modes: code-and-proof and proof-only.
- Frontier-resistant: best config fully solves 27/43 code-and-proof and 25/43 proof-only; 10 instances resist every configuration in both modes.
- Gap is not local proof skill but repo organization: best agent passes 87.3% / 85.8% of specs (cp/po) yet fails shared invariants, lemma libraries, build consistency.
- Novel formal audit mechanism: agents may prove ref-impl incorrectness, individual unsat, or joint-unsat of spec sets → curator repairs (38 defects across 9 instances during curation).
- Anti-cheating: slot-scoped re-render, axiom allowlist (only Classical.choice / propext / Quot.sound + trusted), declaration screening (
native_decide, hollow typeclasses,@[implemented_by]oracle split).
Key numbers
Section titled “Key numbers”| Metric | Value |
|---|---|
| Instances | 43 (Track1 formal 13; Track2 Python 30) |
| APIs / specs | 743 / 2,705 |
| Mean APIs (overall) | 17.3 (max 88) |
| Mean specs | 62.9 (max 203) |
| Source LoC mean / max | 2,899 / 56,887 |
| Best full solves (cp / po) | GPT-5.5 xhigh: 27 / 25 |
| Opus 4.8 | 8 / 10 |
| GPT-5.5 mid | 2 / 6 |
| Sonnet 5 | 2 / 2 |
| Spec pass (best cp) | 87.3% |
| Untouchable instances | 10 |
| Helper depth ≥4 pass rate | ~50.6% cp / 39.1% po (vs ~80%+ at depth 0) |
| Existence/coverage fail rate | 47.1% (highest semantic type) |
| Eval cost GPT-5.5 xhigh cp | **106 / full solve) |
| Curation model $ / instance | ~$60 |
| Lean version in eval | v4.29.1 |
| Harnesses | Codex v0.140.0; Claude Code v2.1.191 |
| Budget | 90 minutes / instance |
Mode pairing (172 instance–agent pairs): 26 both modes; 13 cp-only; 17 po-only; 116 neither. Agents often fix impl early (~median 65 impl lines by min 30 for GPT-5.5 xhigh) then grind proofs. Union of all agents = same 33 distinct repos as strongest alone (ensembling adds nothing at repo level). Spec union: 2,486/2,705 (91.9%) vs best cell 87.3%; 219 specs never passed (clustered in the 10 hard instances; e.g. dedekind_reals 82/82 never proved).
Quotes
Section titled “Quotes”“The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories.”
“High per-specification coverage therefore does not imply repository completion.”
“Completing a repository-level formal verification is a matter of sustained proof work rather than implementation volume.”
“Vero is, to our knowledge, the first benchmark that evaluates agents on joint code-and-proof generation at the repository level.”
Audit during curation: 38 adjudicated spec defects (mistranslation 18, missing domain 17, ref mismatch 2, direct conflict 1) + 6 joint-unsat groups — all repaired before released eval.
DIY / fleet relevance
Section titled “DIY / fleet relevance”- Treat full-repo gate (all specs + build + axiom allowlist) as the unit of success; per-spec % will flatter agents.
- Expect lemma-library / invariant discovery as the hard part; budget for deep helper chains.
- Code-and-proof can help strong agents (simpler provable impls; 5 pairs closed 250 specs vs 201 against fixed ref) but hurts slow agents (Opus loses 360 specs when forced to implement first).
- Cost: unfinished runs often more expensive than finishes; ~23% of spend went to the 10 unsolvable instances.
- Harness patterns worth copying: marker-scoped edits, axiom print checks, reject
implemented_byin impl slots.
Caveats
Section titled “Caveats”- Lean-only target; concurrent/temporal protocols largely absent.
- Spec semantic completeness still human-reviewed; audit certifies satisfiability, not “right requirement.”
- Contamination mitigated by novel Lean formalizations (no public Lean ground truth).