🤖 Vero: repository-level verified-code evaluation

This note studies “Vero: Can AI Agents Build Formally Verified Software Repositories?” as part of the AutoVerus citation watch. The paper is an arXiv v1 preprint dated 2026-08-13 in the saved evidence set. The official artifact is the public sunblaze-ucb/vero repository. Sources: VERO-status, VERO-artifact.

bottom line

Vero is more important as an evaluation threat than as a direct tool threat. It is not another AutoVerus-like Verus proof generator. It is a Lean 4 benchmark for testing whether coding agents can complete curated multi-module verified-code instances: implementations plus proofs against manually curated specifications. Sources: VERO-scope, VERO-inputs, AUTO-scope.

Vero can machine-check that code satisfies formal Lean specifications. It cannot prove that those specifications are complete or match human intent. The paper explicitly says the audit mechanism “cannot ensure that specifications are semantically correct or complete.” Human review remains part of the benchmark construction. Sources: VERO-limitations, VERO-curation.

This study integrity-checked the saved PDF, metadata, and artifact archive. It did not rerun the Vero benchmark or reproduce the reported scores. Source: VERO-artifact.

capability threat: medium

The authors report that frontier coding agents can complete nontrivial curated Lean verification instances. The strongest reported setup fully solves 27 of 43 code-and-proof instances and 25 of 43 proof-only instances. Sources: VERO-results, VERO-models.

The threat is bounded because Vero is not a production Verus/Rust system. It is a Lean 4 benchmark. It includes Verus-derived tasks, but those are translated into Lean and evaluated there.

novelty threat: medium to high

Against AutoVerus, the scope is different. AutoVerus starts from Rust code and its specifications and generates Verus proofs for single-function tasks. Vero starts from curated Lean repositories and asks an agent either to prove a reference implementation or to write implementations and prove all specifications.

evaluation threat: high

First, it uses full-repository completion, not just partial specification coverage.

Second, the grader does not trust the agent’s edited project. It extracts only allowed marker-slot bodies into a fresh benchmark copy, then builds and checks proof axioms.

Third, it treats benchmark defects as a separate class. Agents can submit machine-checked evidence that a specification is unsatisfiable, a reference implementation is wrong, or specifications conflict. The authors then adjudicate those closures by hand.

Fourth, the paper analyzes why agents fail. The key reported bottleneck is not local proof skill. It is failure to discover shared invariants, organize reusable lemma libraries, and keep the repository buildable.

practical competitive threat: low to medium

Vero is a public benchmark and artifact, but it is not a turnkey competitor for verified Rust work. It does not produce Verus proofs for real Rust repositories. It gives competitors a public measuring stick for repository-level verified-code agents. Sources: VERO-scope, VERO-artifact, AUTO-scope.

what Vero actually evaluates

A Vero instance is a curated multi-module Lean 4 project, not an entire upstream Rust, Python, Dafny, Verus, or Coq repository. The curator provides fixed data types and helpers, API signatures, formal specifications, and reference implementations. The agent fills allowed slots. Sources: VERO-scope, VERO-inputs.

There are two task modes.

In proof-only mode, the reference implementation is fixed. The agent must prove every specification against it. Source: VERO-modes.

In code-and-proof mode, the agent writes each API implementation and proves every specification against the implementation it wrote. Source: VERO-modes.

The key scoring rule is all-or-nothing at the repository level. Vero counts an instance as solved only if all required specifications pass. The paper argues this is necessary because easy specifications can inflate partial coverage. Source: VERO-full-coverage.

what the results mean

The authors report that the strongest configuration is Codex version 0.140.0 with GPT-5.5 at xhigh reasoning effort. It solves 27 of 43 instances in code-and-proof mode and 25 of 43 in proof-only mode. Ten instances resist every tested configuration across both modes. Sources: VERO-models, VERO-results.

This creates a useful distinction. The best agent passes more than 80 percent of individual specifications, but it still misses many full repositories. Vero therefore supports measuring completion at the artifact level, not only at the theorem level.

implementation freedom is double-edged

Vero’s code-and-proof mode allows the agent to choose its own implementation. Sometimes that helps. The paper reports five instance-agent pairs where the agent replaced a hard-to-prove reference algorithm with a simpler implementation satisfying the same specifications. Source: VERO-implementation-freedom.

evaluation reliability

Vero’s anti-cheat design is useful because the core oracle is Lean plus additional checks, not agent self-report. Source: VERO-anticheat.

The grader extracts only allowed slot contents and inserts them into a fresh source benchmark. It rejects untrusted axioms and sorry dependencies. It also screens for declarations that can decouple logical semantics from executable behavior.

specification-intent gap

Vero does not solve the specification completeness problem.

For formally sourced benchmarks, Vero translates Dafny, Verus, and Coq projects into Lean and cross-checks against source-language formalizations. For Python-sourced benchmarks, it writes specifications from documentation and tests, then manually reviews them. Sources: VERO-curation, VERO-limitations.

That is useful curation, not proof of intent. The paper’s own limitation is explicit: the audit mechanism certifies formal satisfiability but cannot ensure semantic correctness or completeness.

comparison with AutoVerus

The two papers are therefore complementary. AutoVerus is stronger evidence for Verus proof-generation mechanics. Vero is stronger evidence for how to evaluate repository-level verified-code agents.

Vero primary sources

VERO-status: arXiv metadata XML and official CFF file. Claim: Vero is an arXiv v1 preprint in the saved evidence set. Quote: “http://arxiv.org/abs/2608.13522v1”. Quote: “2026-08-13T17:41:27Z”. Quote: “10.48550/arXiv.2608.13522”. Uncertainty: no proceedings, publisher venue, or acceptance record was found.

VERO-scope: Vero paper. Claim: benchmark scope is repository-level joint implementation and proof synthesis over curated Lean instances. Quote: “first benchmark to evaluate joint implementation and proof synthesis at the repository level”. Quote: “43 multi-module instances sourced from real-world repositories”. Boundary: these are not full arbitrary upstream projects.

VERO-inputs: Vero paper. Claim: each instance has fixed scaffold, APIs, specs, and reference implementations. Quote: “predetermined API interfaces, manually curated formal specifications, and reference implementations”. Quote: “data type and helper definitions, API signatures, and formal specifications”.

VERO-modes: Vero paper. Claim: the benchmark has proof-only and code-and-proof modes. Quote: “prove every specification against the reference implementation”. Quote: “both implement every API and prove every specification”.

VERO-full-coverage: Vero paper. Claim: full coverage is the main score. Quote: “Full coverage is necessary”. Quote: “partial coverage can be inflated by easy ones”.

VERO-anticheat: Vero paper. Claim: grading uses fresh source re-rendering, axiom checks, and declaration screening. Quote: “fresh copy of the source benchmark”. Quote: “axiom allowlist rejects proofs”. Quote: “rule-based detector and an LLM judge”.

VERO-curation: Vero paper. Claim: curation is LLM-assisted and human-reviewed. Quote: “Each stage runs as an LLM agent”. Quote: “reviewed by a human curator”.

VERO-contamination: Vero paper and official README. Claim: the authors argue that novel Lean translations reduce ground-truth leakage. Quote: “no Lean 4 ground-truth proof”. Quote: “no Lean 4 ground-truth solution exists online”. Uncertainty: this does not prove absence of source-language leakage.

VERO-results: Vero paper. Claim: current frontier agents are incomplete at repository level. Quote: “fully solves 27 of 43 instances”. Quote: “10 instances resist all eight configurations”. Quote: “passes 87.3% of specifications”.

VERO-models: Vero paper. Claim: evaluated harnesses are Codex and Claude Code with Lean access. Quote: “Codex (v0.140.0)”. Quote: “GPT-5.5 profiles”. Quote: “Claude Code (v2.1.191)”. Quote: “Lean v4.29.1”.

VERO-lemma-library: Vero paper. Claim: full solves depend on shared lemma libraries. Quote: “shared lemma libraries”. Quote: “median of 73.6% of proof lines”. Quote: “80 of the 82 solves share a helper”.

VERO-implementation-freedom: Vero paper. Claim: implementation freedom can trade efficiency for provability. Quote: “simpler implementation of its own”. Quote: “what it gives up is efficiency”.

VERO-audit: Vero paper. Claim: the audit mechanism found and repaired benchmark defects. Quote: “38 adjudicated specification defects”. Quote: “All of them are repaired”. Quote: “adjudicating every closure by hand”.

VERO-auditor-overlap: Vero paper. Claim: a second auditor gives modest extra value. Quote: “A second auditor adds little”. Quote: “5 additional cases”.

VERO-limitations: Vero paper. Claim: Vero is Lean-only and does not solve semantic completeness. Quote: “currently targets Lean 4 only”. Quote: “cannot ensure that specifications are semantically correct or complete”.

VERO-artifact: official GitHub metadata and README. Claim: the artifact is public, Vero-owned code and scaffolding are Apache-2.0, and the artifact exposes benchmark inventory. Quote: “https://github.com/sunblaze-ucb/vero”. Quote: “Apache License 2.0”. Quote: “Three active benchmarks derive from copyleft upstreams”. Quote: “43 benchmark instances, 743 APIs, 2,705 scored specs”.

AutoVerus baseline

AUTO-status: preserved AutoVerus PDF and Markdown extract. PDF SHA-256: 6c750ff7c3f0de09be7685fa797ee338d669778bc38adbd44230e9668582c5fc. Markdown extract SHA-256: 17a397c18e7f148a1a82d7b2d03856547568e2dc2f3808757af8c67ec4bbf514. Claim: AutoVerus is a PACM PL/OOPSLA 2025 publication. Quote: “Proc. ACM Program. Lang.” Quote: “OOPSLA2”.

AUTO-scope: preserved AutoVerus Markdown extract. Claim: AutoVerus starts from Rust code and specifications, with a single-function task unit. Quote: “provided with Rust code and its specifications”. Quote: “a single Rust function is the unit”.

AUTO-method: preserved AutoVerus Markdown extract. Claim: AutoVerus uses proof construction and verifier-guided debugging. Quote: “three phases of proof construction”. Quote: “debugging guided by verification errors”.

Last edited: 2026-10-31