AI 程式代理與評測
Vero Pushes Coding Agents Across Entire Lean 4 Repositories; the Strongest Configuration Fully Solves Just 27 of 43 Tasks
Vero requires agents to implement multi-module software while submitting machine-verifiable correctness proofs, rather than merely passing unit tests. Across four frontier-agent configurations, the best still failed to fully solve 16 repositories, while 10 defeated every configuration.
Vero expands “verified program generation” from individual functions to entire repositories. Its 43 Lean 4 projects were drawn from Python, Dafny, Verus, and Coq libraries and collectively contain 743 APIs to implement and 2,705 formal specifications, spanning cryptographic protocols, consensus systems, parsers, and data structures. Each task fixes the data types, API interfaces, and specifications; the agent must fill in the implementations and then generate proofs for every specification that can be checked by the Lean kernel.
The evaluation is divided into proof-only and code-and-proof modes. The former provides a reference implementation, while the latter allows the agent to rewrite algorithms. This means an agent may choose a version that is easier to reason about inductively, but it may also invalidate proofs across modules. To prevent shortcuts such as adding axioms or tampering with tasks, the evaluator extracts only modifications from designated regions, rebuilds the project in a clean copy, and checks which axioms the proofs depend on. The benchmark also accepts formal counterproofs showing that a specification is unsatisfiable or that a reference implementation is incorrect, preventing dataset defects from being counted as model failures.
The authors tested Codex and Claude Code with four frontier-model configurations. The best-performing setup, GPT-5.5 xhigh, fully solved 27 of 43 tasks in code-and-proof mode. Ten tasks remained unsolved by every configuration in both modes. Failures clustered around cross-module invariants, protocol consistency, and custom mathematical theories: agents often attempted local proofs one at a time instead of first building a reusable library of lemmas.
This makes Vero more representative of verification work for safety-critical software than conventional “do the tests pass?” benchmarks, but it is not a direct measure of everyday software-development ability. The dataset contains only 43 manually translated projects, and the results are also influenced by agent tooling, reasoning budgets, and Lean expertise. The next step is to examine whether different teams can reproduce the rankings and whether agents can proactively plan cross-file lemmas instead of merely extending their search.