跳转至

文章背景与核心概要

随着AI智能体在编程任务中的广泛应用，其生成的代码在正确性方面往往缺乏理论保证。验证码生成技术（Verified code generation）要求智能体在产出软件实现的同时，必须提供符合其规范的机器检查证明（machine-checked proof），这是通往值得信赖的AI生成软件的坚实途径。然而，现有的基准测试大多仅关注单一函数，或在给定实现的前提下评估证明生成，无法验证智能体是否能在真实的多模块代码库中做出协调一致的实现与证明决策。

为了填补这一空白，研究人员推出了 Vero——首个旨在评估代码库级别联合实现与证明综合（joint implementation and proof synthesis）的基准测试。该基准包含来自现实世界仓库的43个多模块实例，涵盖密码学协议、分布式系统等多个领域，并支持纯证明以及代码与证明双模式评估。此外，Vero引入了审计机制以纠正潜在的标注错误。实验表明，当前最先进的前沿编程智能体在面对复杂代码库时仍显不足，在43个实例中仅能完全解决27个，且在最复杂的仓库上完全无法闭环规范，这为度量迈向代码库规模的形式化验证软件综合进展提供了重要的测试平台。

Vero: Can AI Agents Build Formally Verified Software Repositories?

arXiv: 2608.13522 [cs.LG]
Submitted on: August 13, 2026
Authors: Zhe Ye, Hantao Lou, Yuechun Sun, Peiyang Song, Zhengxu Yan, Timothe Kasriel, Qingyang Zhang, Kaiyu Yang, Soonho Kong, Jingxuan He, Dawn Song

📋 Summary

While AI agents are increasingly utilized for programming tasks, they typically lack guarantees regarding the correctness of the code they generated. Verified code generation—where an agent produces both a software implementation and a machine-checked proof of its specification—offers a robust pathway toward trustworthy AI-generated software.

To evaluate whether AI agents can make coherent implementation and proof choices across real multi-module codebases, researchers introduce Vero, the first benchmark designed to assess joint implementation and proof synthesis at the repository level. Evaluations show that current frontier coding agents still fall short, fully solving only 27 out of 43 instances and failing completely on the most complex repositories.

🛠️ Abstract

AI 智能体正越来越多地被用于编程任务，但它们无法为生成的代码提供任何正确性保证。验证码生成技术（Verified code generation）要求智能体同时产出软件实现以及符合其规范的机器检查证明，这为打造值得信赖的AI生成软件开辟了一条更可靠的途径。现有的相关基准测试要么侧重于单个函数，要么仅在提供实现的情况下评估证明生成。智能体是否能够在真实的多模块代码库中做出连贯一致的实现与证明决策，仍然是一个悬而未决的问题。

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.

为了弥合这一差距，我们推出了 Vero，这是首个在代码库级别评估联合实现与证明综合的基准测试。Vero 包含了 43 个多模块实例，这些实例源自 Python、Dafny、Verus 和 Coq 的真实代码库，涵盖了从密码学协议到分布式系统的多样化领域。每个实例都由一个包含预定 API 接口、人工精心策划的形式化规范以及参考实现的 Lean 4 多模块代码库组成，同时支持纯证明以及代码与证明评估模式。

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.

为了提高基准测试的可靠性，Vero 还引入了一种审计机制，允许智能体对所提供的规范的不满足性或参考代码的不正确性进行形式化证明，从而在整理过程中浮现并纠正潜在的代码和规范错误。我们对具备 Lean 工具链访问权限的前沿编程智能体配置进行了评估。最强大的智能体在 43 个实例中仅完全解决了 27 个，并且在难度最高的代码库上未能闭环任何规范。Vero 为衡量向代码库规模形式化验证软件综合迈进的进展提供了一个具体的测试平台，而当前的智能体在这方面仍有欠缺。

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.

📊 Metadata & Classification

  • Primary Subject: Machine Learning (cs.LG)
  • Secondary Subjects:
  • Artificial Intelligence (cs.AI)
  • Logic in Computer Science (cs.LO)
  • Programming Languages (cs.PL)
  • Software Engineering (cs.SE)
  • DOI: 10.48550/arXiv.2608.13522