Summary
This paper introduces Vero, the first benchmark evaluating whether AI agents can jointly synthesize implementations and machine-checked proofs at the repository level. Existing verified-code-generation benchmarks focus on single functions or proof-only tasks with provided implementations, leaving open whether agents can make coherent implementation and proof decisions across multi-module codebases. Vero contains 43 multi-module instances drawn from real-world repositories originally written in Python, Dafny, Verus, and Coq, spanning domains from cryptographic protocols to distributed systems. Each instance is a multi-module Lean 4 repository with fixed API interfaces, human-curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation. An audit mechanism lets agents formally prove specification unsatisfiability or reference-code incorrectness, exposing and fixing latent errors during curation. The authors evaluate frontier coding agents with Lean toolchain access; the strongest configuration solves only 27 of 43 instances and closes no specifications on the hardest repositories. Benchmark, curation pipeline, and evaluation harness are open-sourced.
Vero: Can AI Agents Build Formally Verified Software Repositories?
Paper: arXiv:2608.13522
Authors: Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song
Released: 2026-08-13
Overview
AI agents are increasingly used for programming, yet provide no correctness guarantees on the code they produce. 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. Prior benchmarks focus on individual functions or evaluate proof generation given a fixed implementation, leaving open whether agents can make coherent implementation-and-proof choices across real multi-module codebases.
Contributions
- Vero: the first repository-level benchmark for joint implementation and proof synthesis.
- 43 multi-module instances sourced from real-world repositories originally written in Python, Dafny, Verus, and Coq, covering domains ranging from cryptographic protocols to distributed systems.
- Each instance is a multi-module Lean 4 repository with a fixed API, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes.
- An audit mechanism lets agents formally prove that a specification is unsatisfiable or that the reference code is incorrect, surfacing and correcting latent errors during benchmark curation.
Evaluation
The authors evaluate frontier coding agents with Lean toolchain access:
- The strongest agent configuration fully solves only 27 of 43 instances.
- On the hardest repositories, the agents close no specifications.
Takeaway
Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short.Resources
- Paper: https://arxiv.org/abs/2608.13522
- Code & benchmark: https://github.com/sunblaze-ucb/vero
---
*Auto-collected 2026-08-15*
This page is an English static mirror generated for search and AI citation.
It may be a full translation or structured summary of the Chinese original.
Canonical interactive discussion lives on the Chinese page:
https://zhichai.net/topic/178633506