UC Berkeley 等发布 Vero 基准：检验 AI 智能体能否构建形式化验证的完整软件仓库

AI 编程智能体如今能够跨整个代码仓库进行修改。但当智能体输出“所有测试通过”之后，我们真的能信任它们和它们写的代码吗？

AI 编程智能体如今能够跨整个代码仓库进行修改，而且它们通常会在最后报告所有测试通过。但这份报告的实际价值比听起来要低，因为测试只能检查那些有人想到要写下来的用例。形式化验证则能提供强得多的保证。它能生成一份机器可检查的证明，证明某个实现在其规范所覆盖的每一个输入上都满足该规范，而不仅仅是测试套件里的那些输入。因此，一个自然而然的问题是：AI 智能体是否真的能在真实代码库上达到这一标准？它能否在多模块仓库中实现每一个必需的 API，证明每一条给定的规范，并让代码、证明和构建过程自始至终保持一致？我们构建了 Vero 来精确衡量这一点。

摘要速览

据我们所知，Vero 是第一个要求智能体在仓库级别同时编写实现和证明的基准测试。它包含 43 个多模块 Lean 4 实例，这些实例选自原本用 Python、Dafny、Verus 和 Coq 编写的真实项目。在整个测试套件中，智能体需要面对 743 个计分 API 和 2,705 条形式化规范。

该基准测试有两种运行模式。在纯证明模式下，智能体会收到参考实现，并针对这些实现证明规范。在代码加证明模式下，智能体需要自己编写每一个必需的 API，然后证明自己的代码满足每一条规范。

我们评估的最强配置是 GPT-5.5 (xhigh) 搭配 Codex，它在代码加证明模式下完整解决了 43 个实例中的 27 个，在纯证明模式下解决了 43 个中的 25 个。它分别通过了 87.3% 和 85.8% 的单个规范。即便如此，仍有 10 个实例在所有配置的两种模式下都未能解决。综合来看，这些数字表明，证明单个规范已不再是难点。难点在于将整个证明仓库整合在一起，确保所有内容都能构建、所有义务都能闭合。

关键要点

• 仓库完成远比单规范成功更难。GPT-5.5 (xhigh) 在代码加证明模式下通过了 87.3% 的规范，在纯证明模式下通过了 85.8%，但完整完成的实例分别只有 27/43 和 25/43。Vero 只有在所有提供的规范都被证明、且评分仓库保持可构建且无公理污染时，才将一次运行计为完整解决。

• 可复用的引理库是完整解决中一贯出现的模式。在 82 次完整解决的运行中，智能体编写的辅助定理在代码加证明模式下中位数包含 73.6% 的证明行，在纯证明模式下为 71.6%。在 82 次完整解决中，有 80 次至少有一个辅助定理支持两个或更多规范；有 65 次，一个辅助定理至少支持五个规范。

• 实现自由度既有利也有弊。智能体有时会用满足相同规范的更简单实现，替换难以证明的参考算法。论文识别出跨三个仓库的五个实例-智能体对，在这些情况下这种做法是有帮助的。相反，有 17 对匹配组合在纯证明模式下是完整解决，但在代码加证明模式下却不是。

• 该基准仍有相当大的提升空间。43 个实例中有 10 个在所有配置的两种模式下都未被解决。论文将许多残余失败归因于全局不变量、重复行为、提供的定义，以及可复用引理的深层链条。

为什么 Vero 是新颖且重要的

大多数验证代码基准都聚焦于单个函数。少数仓库级基准通常提供固定实现，仅评估证明生成。因此，它们遗漏了真实验证工作的一个核心难点：实现与证明的选择会在整个代码库中相互影响。

Vero 将这种耦合关系本身转化为任务。智能体必须在一个多模块的 Lean 4 项目中做出连贯的决策，而不是解决一系列相互独立的证明空缺。这暴露了函数级评测无法衡量的长周期证明工程、实现与证明之间的协调，以及构建保持能力。

Vero 的工作原理

仓库脚手架

每个 Vero 实例都是一个自包含的 Lean 4 项目。Lean 4 是一种编程语言和定理证明器，其中的证明由一个小型可信内核进行校验。策展方提供三个固定不变的内容层：

• 共享数据类型和辅助定义。

• 定义必须实现内容的 API 签名。

• 以谓词形式编写的形式化规范，这些谓词作用于整个仓库范围的实现接口。

智能体负责填充实现主体和证明义务。当评分器从干净的基准源码重新构建仓库时，完整求解要求所有指定的义务均能通过。

图 1. Vero 端到端的构建、评测、评分和形式化审计流程。

一个脚手架，两种模式

仅证明模式。基准提供参考实现。智能体必须针对该实现证明每一条规范。这隔离了证明构建过程，同时保留了仓库规模的依赖关系。

代码与证明模式。参考实现主体被隐藏。智能体需要编写每个必需的 API 主体，并针对自己的实现证明每一条相应的规范。这是 Vero 主要的联合生成场景。

代码与证明模式在任务叠加之外增加了实现义务。一个对证明友好的算法可能比一个忠实但困难的参考算法更容易验证，而一个糟糕的实现选择则可能产生新的证明义务或破坏构建。

独立评分与防作弊保障

评分器仅从允许智能体编辑的区域提取内容，将其插入到根据基准源码渲染的全新项目中，并重建整个项目。它会对照公理白名单检查证明依赖关系，并使用基于规则和 LLM 评判的筛选机制，拒绝那些使证明义务变得微不足道的声明或类型类实例。这些保障措施旨在确保被认可的证明经过机器校验，且不依赖于对冻结基准内容或不允许的公理所做的编辑。

基于真实代码仓库构建

Vero 包含 43 个实例：其中 13 个来自用 Dafny、Verus 或 Coq 编写的、具备验证意识的项目，另外 30 个来自 Python 项目，策展人为这些项目额外编写了形式化规范。该套件涵盖智能合约与区块链协议、分布式系统与共识、安全关键型基础设施、形式化数学、数据结构、算法以及数值工具。

策展流程遵循发现、筛选、规划、翻译、按需编写规范以及验证这几个步骤。每个阶段都由 LLM 智能体在人工审核把关下运行。由此产生的 Lean 4 实现、规范和真值证明属于全新的策展工作；对于所评估的实例，此前并不存在公开可用的 Lean 4 真值。

评估与主要结果

评估覆盖了两种智能体框架下的四种前沿编码智能体配置。每次运行都拥有完整的文件系统、构建和 Lean 工具链访问权限，以及 90 分钟的墙钟时间预算。

表 1. 90 分钟预算内的完整代码仓库求解结果。

GPT-5.5 (xhigh) 在 45 分钟内完成了 25 个代码与证明以及 23 个仅证明的完整求解。即便如此，大多数已求解的实例仅由单一配置完成，并且有 10 个实例在所有八种智能体模式组合下均未能求解。

图 2. 完整求解轨迹与精确完整求解矩阵。

Vero 将完整求解作为主要结果指标，因为部分规范覆盖率可能因较容易的义务而被高估。在代码加证明模式下，未获证明的规范可能意味着两种情况：要么缺少证明，要么实现未通过该规范。按规范统计的覆盖率在诊断层面仍有价值，但只有完整覆盖率才能证明所提交的实现满足基准测试中的全部规范。

结果揭示了什么

完整求解运行建立在证明依赖之上

在 82 次完整求解运行中，辅助定理在代码加证明模式下平均包含 73.6% 的证明行，在纯证明模式下为 71.6%。在 82 次完整求解中，有 80 次存在一个辅助定理至少支撑两个规范，65 次中至少支撑五个规范。

在其他运行中，辅助链深度与较低通过率相关。没有辅助定理的规范在代码加证明模式下的通过率为 83.9%，纯证明模式下为 80.1%。当链深度达到 4 或以上时，通过率分别降至 50.6% 和 39.1%。这一规律表明，需要更好的不变量发现、证明依赖规划以及可复用的本地库。

图 3. 证明辅助定理的复用、证明行占比及辅助链通过率。

实现自由度

我们的论文在 3 个代码库中识别出 5 对实例-智能体组合，其中智能体用满足相同规范的更简单实现替换了困难的参考算法。通过修改这 5 对组合，代码加证明模式关闭了全部 250 个规范，而针对固定参考实现的纯证明运行关闭了 201 个。实现带来的增益主要在于可证明性，而不一定是生产质量。某些替换牺牲了渐近效率。

自由度也可能增加难度。有 17 对匹配的实例-智能体组合在纯证明模式下是完整求解，但在代码加证明模式下不是。轨迹分析显示，智能体倾向于在早期就确定一种实现，并持续扩充证明直到截止时间，而不是在证明计划反复受阻时重新审视定义。

基准测试的持续改进

形式化验证基准测试中仍可能潜藏着能够通过类型检查、成功构建和人工审核的隐性错误。Vero 将这些错误转化为一个迭代式的质量改进循环：它不把无法完成的证明义务视为智能体失败，而是通过其审计机制接受三种形式的机器可验证的反面证据：

• 参考实现违反了某个规范。

• 没有任何实现能够满足某个单独的规范。

• 一组规范虽然各自都能被单独满足，但合在一起却是不一致的。

每份形式化证据都会将受影响的实例送回人工审核，并帮助引导修正。所有已确认的缺陷都在报告评估之前得到了修复。同样的反馈循环还能推动基准测试的持续改进——随着未来智能体能力增强、发现更细微的问题，这一机制将不断发挥作用。

Vero 为何重要

仓库级验证代码生成为比单纯测试更强的保证形式提供了试验场，尤其适用于高可靠性要求的软件。结果表明，当前智能体能够通过构建大量证明库、识别基准测试缺陷，以及有时优化现有算法以提升可证明性，来完成这类任务中相当可观的一部分。剩余的差距在于仓库级的组织协调：发现共享不变量、协调代码与证明，以及保持整个产物的连贯性和可构建性。

资源与引用

@article{ye2026vero,
  title={Vero: Can AI Agents Build Formally Verified Software Repositories?},
  author={Ye, Zhe and Lou, Hantao and Sun, Yuechun and Song, Peiyang and Yan, Zhengxu and Kasriel, Timothe and Zhang, Qingyang and Yang, Kaiyu and Kong, Soonho and He, Jingxuan and others},
  journal={arXiv preprint arXiv:2608.13522},
  year={2026}
}