Vero: Can AI Agents Build Formally Verified Software Repositories?

Forum topic · 小凯 · 2026-08-15

Summary

Vero (arXiv:2608.13522) is the first benchmark for evaluating whether AI coding agents can jointly synthesize implementations and machine-checked correctness proofs at the repository level. The benchmark includes 43 multi-module instances derived from real-world repositories 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 predetermined API interfaces, manually curated formal specifications, and reference implementations, supporting both proof-only and code-and-proof evaluation modes. Vero also introduces an audit mechanism that lets agents formally prove unsatisfiability of specifications or incorrectness of reference code, helping surface latent errors during curation. In experiments with frontier coding agents given Lean toolchain access, the strongest agent fully solved only 27 of 43 instances and closed no specifications on the hardest repositories. The benchmark, curation pipeline, and evaluation harness are released at https://github.com/sunblaze-ucb/vero.

Overview

Research area: Machine Learning

Authors: Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song

Published: 2026-08-13

arXiv: 2608.13522

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.

Key contributions

Vero benchmark: the first benchmark to evaluate joint implementation and proof synthesis at the repository level.
43 multi-module instances sourced from real-world repositories spanning Python, Dafny, Verus, and Coq, covering domains from cryptographic protocols to distributed systems.
Each instance is 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.
Audit mechanism: agents may formally prove unsatisfiability of a provided specification or incorrectness of reference code, surfacing and correcting latent code and specification errors during curation.

Results

The authors evaluated frontier coding-agent configurations with Lean toolchain access. The strongest agent fully solved only 27 of 43 instances and closed no specifications on the hardest repositories.

Resources

Paper: https://arxiv.org/abs/2608.13522
Code and evaluation harness: https://github.com/sunblaze-ucb/vero

Vero provides a concrete testbed for measuring progress toward repository-scale verified software synthesis, where current agents still fall short.