Vero: Can AI Agents Build Formally Verified Software Repositories?
2026-08-13 • Machine Learning
Machine LearningArtificial IntelligenceLogic in Computer ScienceProgramming LanguagesSoftware Engineering
AI summaryⓘ
The authors created Vero, a new benchmark to test if AI agents can write both code and machine-checked proofs for entire software projects, not just small functions. Vero uses real multi-module codebases with formal specifications and reference implementations in several programming languages. Their tests show current AI agents struggle to fully solve these complex verification tasks, especially on the hardest examples. This benchmark helps measure progress toward trustworthy AI-generated software with guaranteed correctness.
verified code generationmachine-checked proofformal specificationmulti-module codebaseLean 4proof synthesisAI programming agentssoftware verificationbenchmarkrepository-scale synthesis
Authors
Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song
Abstract
AI agents are increasingly used for programming, but do not provide any guarantee on the correctness of generated code. 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. Existing benchmarks in this direction either focus on individual functions or only evaluate proof generation with provided implementations. It is still an open question whether agents can make coherent implementation and proof choices across real multi-module codebases. To bridge this gap, we introduce Vero, the first benchmark to evaluate joint implementation and proof synthesis at the repository level. Vero contains 43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, and covering diverse domains from cryptographic protocols to distributed systems. Each instance consists of a multi-module Lean 4 repository with predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. To improve benchmark reliability, Vero also includes an audit mechanism where agents are allowed to formally prove unsatisfiability of provided specification or incorrectness of reference code, which surfaces and corrects latent code and specification errors during curation. We evaluate frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solves only 27 of 43 instances and closes no specifications on the hardest repositories. Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short. We release the benchmark, curation pipeline, and evaluation harness at https://github.com/sunblaze-ucb/vero.