← 返回 PaperDaily 大模型与智能体

UC Berkeley新基准Vero：最强AI写证明，43个代码仓库只通关27个

AI生成的代码，你敢直接上生产吗？单元测试过了不代表没bug，仓库级形式化验证才是终极保险丝。UC Berkeley等机构提出Vero，要求智能体在一个多模块Lean 4代码仓库里同时写实现和证明，结果最强配置只通关27/43——答案藏在仓库级一致性和共享引理库的组织能力里。

龙哥读论文发布于 2026-08-17 00:20:16 阅读 6 查看原文

#AI科研 #大语言模型 #Agent #数据集

UC Berkeley新基准Vero：最强AI写证明，43个代码仓库只通关27个

原论文信息如下：

论文标题:
Vero: Can AI Agents Build Formally Verified Software Repositories?

发表日期:
2026年08月
发表单位:
UC Berkeley（加州大学伯克利分校）等
原文链接:
https://arxiv.org/pdf/2608.13522v1.pdf
开源代码链接:
https://github.com/sunblaze-ucb/vero

引言：AI写代码，你敢放心用吗？

先抛一个问题：如果一个AI智能体帮你写完了一个分布式共识协议或者一个密码学库，代码编译通过、单元测试也全绿，你敢直接部署到生产环境吗？

大概率不敢。测试只能证明存在过的输入没问题，却无法保证没测到的边界情形里藏着致命bug。这在普通业务系统里或许能靠运维兜底，但在协议软件、操作系统内核、安全基础设施里，一个没被测试覆盖的角落，可能就是漏洞被利用的入口。单元测试的覆盖范围永远是有限的，它无法穷举所有可能的输入组合，更无法证明代码在所有可能执行路径上的行为都符合预期。

形式化验证给出了一个更硬核的答案：让机器检查证明，证明实现满足规范。只要证明通过，理论上对所有输入，规范能捕获的每一类bug都不存在。传统上这是专家用Coq、Isabelle等证明助手手工完成的苦力活，但近两年大模型开始介入这个领域——问题来了：AI智能体真的能胜任仓库规模的形式化验证吗？这里的“仓库规模”不是指几百行代码的小项目，而是指包含多个模块、多个文件、相互依赖的完整软件仓库。在这样的规模下，代码、规范、证明三者之间的复杂关系会指数级增长，对智能体的全局推理能力提出了前所未有的要求。

UC Berkeley的Dawn Song团队联合多家机构给出了一个衡量答案的尺子——Vero基准。这是全球第一个在仓库级别评估“实现+证明联合生成”的测试平台，结果相当扎心：当前最强的智能体配置，完整通关率也只有62.8%（27/43）。这个数字意味着，即使是最先进的AI系统，在面对真实世界的软件验证任务时，仍有超过三分之一的仓库无法完整解决。更值得关注的是，有10个仓库是所有测试配置都无法攻克的，它们代表了当前AI能力的真正边界。

形式化验证的挑战：从单函数到仓库级代码

先说说已有的验证基准都干了些啥。最早的miniCodeProps、FVAPPS、VERINA、CLEVER等基准，基本都在单个函数的层面打转：给一个算法题（比如排序、链表反转），要求模型生成实现加证明。这类基准推动了“函数级”的验证能力进步，但现实世界的软件不是孤立的函数。一个真实的软件系统，比如一个区块链节点，包含网络层、共识层、存储层、加密模块等多个子系统，每个子系统又包含数十个相互调用的函数。函数之间的调用关系、共享的数据结构、跨模块的不变量，这些都是单函数基准无法覆盖的。

后来出现了RVBench、VeriSoftBench、VeruSAGE-Bench等仓库级基准，但它们只评估“证明生成”——参考实现是给定的，智能体只需要补出证明。这遗漏了一个核心问题：实现的选择直接影响证明的难度。同一个规范，用一个难以推理的复杂算法去实现，证明可能需要几百行引理；换一个简单但效率稍低的实现，证明可能几十行就搞定。真实开发中，工程师往往会在实现和证明之间反复权衡，这种耦合是仓库级验证的核心矛盾。比如，要实现一个有序映射，用红黑树实现需要证明复杂的平衡不变量，而用链表实现则只需证明线性搜索的正确性——前者性能好但证明难，后者性能差但证明简单。这种权衡在单函数基准中几乎不存在，但在真实项目中却是家常便饭。

更深层的挑战在于跨模块一致性。一个函数A的证明可能依赖底层工具函数B的引理；如果智能体修改了B的实现，A的证明可能瞬间失效。代码、规范、证明在多个文件之间深度交织，智能体必须像程序员一样全局思考整个代码库的一致性，而不是局部盯着一个函数敲定理。这种“全局推理”能力，恰恰是当前模型最稀缺的。想象一下：你正在证明一个交易处理函数的正确性，它调用了三个辅助函数，每个辅助函数都有自己的规范。如果你修改了其中一个辅助函数的实现，不仅这个辅助函数自己的证明需要更新，所有调用它的函数的证明也可能需要调整。这种级联效应在大型代码库中非常普遍，也是形式化验证工程中最耗时、最需要全局视野的部分。

Vero就是要在这个空白地带立起一根标杆：让智能体在一个多模块Lean 4仓库里，从零开始同时完成实现和证明。做不到？没关系，测评报告会告诉你差距在哪里。Vero的设计目标不是让所有智能体都能通关，而是精确地量化当前AI在仓库级验证上的能力边界，为后续研究提供可比较的基准。每个实例都经过人工审核，确保规范的正确性和可实现性，避免出现“不可能完成的任务”这种无效测试。

Vero基准：首个仓库级形式化验证测试平台

Vero的核心思路很直接：从真实世界代码仓库中挖掘测试任务，把每个任务做成一个完整的Lean 4项目，包含类型定义、API签名、人工审核过的形式化规范，以及参考实现。智能体的任务就是在这个脚手架上，把所有API实现出来，并且证明它们满足全部规范。这里的“完整”意味着：不是只验证几个核心函数，而是仓库中所有公开的API都要有实现和证明。这模拟了真实软件工程中“交付一个完整可验证的软件模块”的场景。

整个基准包含43个多模块实例，来源横跨Python、Dafny、Verus、Coq四种语言的真实项目——从区块链智能合约、分布式共识协议、安全关键的编码解析，到形式化数学算法库和基础数据结构。每个实例都是一个完整的Lean 4项目，包含类型定义、API签名、人工审核的规范以及参考实现。智能体的任务就是在一个完整的代码仓库里，同时产出所有API的实现和对应的正确性证明。这种多语言来源的设计非常关键：它确保基准不是针对某一种编程语言的特性设计的，而是反映了不同语言生态中形式化验证的共性挑战。比如，从Python项目翻译过来的实例，其规范往往更偏向业务逻辑；而从Coq项目翻译过来的实例，则可能包含更复杂的数学推理。

图1：Vero端到端构建与评估流程图。人工把关的流水线将真实世界的Python和形式化语言仓库转换为Lean 4基准实例（包含固定定义、API签名、规范和参考实现）。智能体以仅证明或代码加证明模式接受评估，并由独立评分器打分，而正式审计路径将基准缺陷的机器检查证据返回给流水线。

图1展示了Vero从基准构建到智能体评估的完整工作流。这里的“仓库级”不是把几个函数堆在一起就完事，而是要求代码、规范、证明在多个文件之间深度交织：一个函数的证明可能依赖底层工具函数的引理，修改一个实现可能让其他模块的证明全部失效。这种跨模块的全局一致性推理，才是真实形式化验证工作的日常。图1中特别值得注意的是“人工把关”环节——每个从上游仓库挖掘的实例都要经过人工审核，确保规范的正确性、参考实现的合理性，以及翻译到Lean 4过程中的忠实性。这个环节虽然成本高昂，但保证了基准的质量，避免了“规范本身有错”这类问题干扰智能体的评估。

表1：Vero按来源轨道划分的统计汇总。报告了每个指标的实例均值和最大值。源代码行数是上游仓库中选定用于策展的有效代码行数，不含空行和注释。

从表1可以看到Vero的规模：整体743个计分API、2705条规范，平均每个实例17.3个API、62.9条规范。其中形式化语言轨道（Track 1）的实例更大，平均36个API、92.8条规范，最大实例有88个API、203条规范、源仓库超过5.6万行代码。Python轨道（Track 2）虽然单个实例偏小，但胜在覆盖面广，30个实例涵盖了从密码库到图算法的各类常用代码。这种规模设计是有意为之：Track 1的实例更接近“真实的形式化验证项目”，需要处理复杂的数学推理和深层的不变量；Track 2的实例则更接近“日常的软件开发任务”，考验智能体对常见编程模式的验证能力。两个轨道互补，共同构成了对AI验证能力的全面测试。

核心设计：接口、规范与实现的三层解耦

Vero的数据格式设计有一个很巧妙的地方：每个规范（specification）不是绑定某个具体实现，而是参数化在一个叫RepoImpl的接口结构体上。这个结构体把所有的API签名收集在一起，每个API是这个结构体的一个字段。规范被定义成“关于RepoImpl的谓词”，即给定任意一个实现，判断这个实现是否满足规范。这种设计模仿了依赖类型编程中的“模块接口”概念：接口定义了所有公开的函数签名，实现必须提供这些函数的具体定义，而规范则是对这些函数行为的约束。

为什么这样设计？因为Vero要支持两种评估模式。在仅证明模式（proof-only）下，参考实现直接填入RepoImpl，智能体只需要证明这些规范对参考实现成立。在代码加证明模式（code-and-proof）下，RepoImpl由智能体自己填充——它既要写实现，又要证明自己的实现满足规范。这个设计不仅让两种模式共用同一套规范定义，还给审计机制留了后门：如果规范本身有问题，智能体可以针对任意实现（不只是参考实现）给出反例。这种三层解耦（接口、规范、实现）的设计，使得Vero可以灵活地评估智能体的不同能力维度：仅证明模式测试“给定实现，能否证明正确性”，代码加证明模式测试“能否同时设计实现和证明”。

图2展示了一个简化示例：左边是API签名（比如CreateAccountSig代表账户创建），中间是RepoImpl结构体把三个API收集在一起，右边是一条规范——新建账户的余额应该为零。智能体在代码加证明模式下要填充canonical实现，并证明所有规范。这个示例虽然简单，但清晰地展示了Vero的核心抽象：API签名定义了函数的输入输出类型，RepoImpl结构体将这些签名组织成一个统一的接口，规范则用逻辑公式描述函数的行为。智能体需要同时处理这三层：实现代码满足类型签名，证明代码满足规范。

Vero还有一个防作弊机制值得一提。评分时，评分器会从原始基准文件重新渲染一份全新的Lean项目，只取出智能体在标记区域内写的代码，插入到这份干净副本中编译检查。同时，一个公理白名单机制会拒绝所有依赖智能体自行引入的不受信公理的证明——防止智能体靠声明一个公理来“证明”一切。还有一个规则检测器加一个LLM裁判，打击通过恶意类型类实例或不可计算选择等机制作弊的行为。这些机制共同确保了评估的公平性：智能体必须真正写出合法的证明，而不是通过某种“漏洞”绕过验证。比如，如果智能体声明了一个公理“所有命题都成立”，那么任何证明都会通过——但公理白名单会拒绝这种不受信的公理，迫使智能体写出真实的证明步骤。

审计机制：让基准自我纠错

做形式化验证基准有个很尴尬的问题：你精心设计的规范和参考实现，可能本身就藏着bug。规范可能写得过强，没有任何实现能满足；参考实现可能写错了，不满足它自己的规范。这种错误非常隐蔽，能通过类型检查、能通过构建、甚至能通过人工评审，但当智能体尝试证明时就会暴露出来。比如，一个规范可能要求“所有操作都保持列表有序”，但参考实现中某个操作实际上会破坏有序性——这个bug在人工评审时可能被忽略，但智能体在尝试证明时就会发现矛盾。

Vero引入了一个审计机制：如果智能体认为基准本身有问题，可以提交三种机器可检查的“负面证据”：一是证明参考实现不满足某条规范；二是证明某条规范本身就不可能被任何实现满足；三是证明一组规范互相矛盾。这些证据通过Lean检查后，会触发人工审核，帮助修正基准本身的问题。这等于把基准的“自我纠错”从人工评审扩展到了机器检查层面。这种机制在之前的基准中从未出现过——它让智能体不再只是被动的“考生”，而是可以主动指出“考题本身有误”的“审查者”。

别小看这个机制。论文报告说，在基准开发过程中，审计机制确实发现了多个人工评审漏掉的潜在错误，为修正提供了正式的反例证据。这也开启了一个良性循环：随着智能体越来越强，它们能发现更多基准问题，基准也随之变得越来越可靠。这种“人机协同”的基准维护方式，可能是未来所有AI评估基准的发展方向——不是静态地发布一个测试集，而是让测试集在使用过程中不断进化，通过智能体的反馈来发现和修复自身的缺陷。

前沿智能体的表现：27/43的突破与10个未解难题

论文评估了四种前沿配置：GPT-5.5（默认推理强度）、GPT-5.5（xhigh超高推理强度）以及Claude家族两款模型，各搭配对应的编码智能体框架，给90分钟的推理预算。结果不出所料——最强配置GPT-5.5（xhigh）在代码加证明模式完整解决了27/43个实例，仅证明模式解锁25个；Claude Opus 4.8能解8个（代码加证明）/10个（仅证明）；GPT-5.5默认配置只有2个，Claude Sonnet 5也是2个。差距不是一点半点。这个结果清晰地展示了当前AI模型在形式化验证任务上的能力分层：顶尖模型（GPT-5.5 xhigh）已经能够处理相当一部分仓库级验证任务，但大多数模型仍然力不从心。

图3：智能体在Vero上的表现。(a,b) 在90分钟预算内，代码加证明和仅证明模式下的累计完整解答数（共43个）；菱形标记了各配置的中位运行时间。(c) 每种配置在每种模式下完整解决了哪些实例。

图3清晰展示了这个“前沿抗性”（frontier-resistant）现象：最强的GPT-5.5（xhigh）在45分钟内就能完成大部分通关，但始终有10个实例是所有八种配置（四种模型×两种模式）都未能解决的。更值得注意的是，大部分被解决的实例只有一种配置能通关——这意味着模型之间的能力差异和互补性都很明显。比如，某个实例可能GPT-5.5（xhigh）能解但Claude Opus 4.8解不了，另一个实例则相反。这种互补性暗示着不同模型在形式化推理上可能有不同的“强项”和“弱项”，未来或许可以通过模型集成来提升整体性能。

一个扎眼的发现：GPT-5.5（xhigh）在代码加证明模式下达成了87.3%的规范通过率（仅证明模式85.8%），但仓库级完整通关率只有62.8%。这说明瓶颈不在单条规范的证明技巧，而在于如何把所有规范组织起来：很多规范需要先建立跨模块的共享引理，再逐层推导到最终目标。智能体像是能单独打赢每一场战斗，却还不太会打一场需要整体协同的战争。换句话说，模型已经非常擅长“局部证明”——给定一个具体的证明目标，它能找到正确的证明步骤。但“全局组织”——决定先证明哪些引理、如何组织证明结构、如何让不同模块的证明相互配合——仍然是它的软肋。

图4进一步揭示了两种模式间的关系。在172对“实例-智能体”组合中，只有26对在两种模式下都通关，13对仅代码加证明模式通关，17对仅仅证明模式通关，剩下的116对双双失败。这说明“实现+证明联合生成”确实是全新的挑战——实现自由既可以是助力，也可能是阻力。值得注意的是，有13对组合在代码加证明模式下成功但在仅证明模式下失败，这说明智能体通过选择更简单的实现，成功降低了证明难度。而17对组合则相反——在仅证明模式下成功，但在代码加证明模式下失败，这通常是因为智能体自己写的实现引入了额外的证明负担。

图4：按任务模式划分的完整仓库结果与产出规模。(a) 172对实例-智能体组合在两种模式下的配对完整解答结果。(b–d) 344次运行结束时的实现代码行数、证明行数及其比值，按模式和是否为完整解答分类。菱形标记中位数，粗线段标记四分位距。

图4(b–d)给出了一个耐人寻味的统计：完整通关和失败运行写出的实现代码量差不多，但通关运行的证明文本量约为失败运行的两倍，证明与实现的比例也显著更高。所谓“仓库级形式化验证”，本质上是持续的证明工程劳动，而不是实现代码的堆砌。这个发现对AI智能体的设计有重要启示：与其花更多精力优化实现代码，不如把更多资源投入到证明生成上。在Vero的任务中，证明的“量”和“质”比实现的“优雅”更重要。

更深层的发现来自对证明结构的分析。在82次完整通关中，智能体自己写的辅助引理（helper theorems）占了证明行数的中位数的73.6%（代码加证明）和71.6%（仅证明）。这些引理不是只服务单条规范——80次通关中至少有一个引理被两个以上规范共享，65次中至少有一个引理被五个以上规范共享。这说明通关的仓库都是围绕“可复用的引理库”组织起来的，而不是每个规范独立证明。这种“引理库”的组织方式，正是人类形式化验证工程师的核心工作模式：先建立一组基础引理，然后在此基础上逐层构建更复杂的证明。智能体在通关过程中自发地采用了这种模式，说明它已经“领悟”到了形式化验证的某些关键技巧。

图5：82次完整解答中的证明结构。辅助引理是智能体为了支持其规范证明而编写的定理。(a) 一个辅助引理被多少条规范共享。(b) 辅助引理在证明文本中的行数占比。(c) 其余七次运行中的通过率，按GPT-5.5（xhigh）仅证明模式解决方案中每条规范的辅助引理链深度分组。

图5(c)揭示了一个关键规律：不需要辅助引理的规范，在其他运行中的通过率高达83.9%（代码加证明）和80.1%（仅证明）；但需要四层以上引理链的规范，通过率骤降到50.6%和39.1%。深层的规范需要层层递进的全局推理，这正是当前智能体的软肋。这个发现量化了“证明深度”对AI能力的挑战：浅层的证明（不需要辅助引理或只需一层引理）已经基本被攻克，但深层的证明（需要多层引理链）仍然困难重重。这也为未来的研究指明了方向：如何让模型学会构建和复用深层引理链，是提升仓库级验证能力的关键。

实现自由度：双刃剑效应

代码加证明模式给了智能体一个仅证明模式没有的杠杆：可以自己选择实现方式。这到底算优势还是负担？Vero的回答是：看情况。实现自由度是一把双刃剑——用得好可以大幅降低证明难度，用得不好则可能引入额外的证明负担。

图6：智能体早期确定实现，直到截止时间都在增加证明。列是不同的智能体配置。顶行显示两种模式下随时间推移编写的证明行数；底行显示代码加证明模式下编写的实现行数。细线是每个仓库的轨迹，粗线是中位数，带状区域是四分位距。计数不包括空行、注释和占位符。

论文在代码加证明模式下发现了五对“实例-智能体”组合，智能体把难以验证的参考算法换成了自己写的、满足同样规范的更简单实现。这些替换在行为上是正确的，不是投机取巧：实现更简单了，证明自然好写，但代价是效率可能下降。在这五对组合中，智能体关闭了全部250条规范，而针对固定参考实现的仅证明模式只能关闭201条——实现自由度确实能“绕开”证明难题。比如，一个参考实现可能使用了复杂的位运算技巧来提升性能，但智能体选择用简单的循环来实现同样的功能——虽然性能差一些，但证明起来容易得多。这种“用性能换可证明性”的权衡，在真实的形式化验证项目中也很常见。

但反过来，有17对组合在仅证明模式下通关，却在代码加证明模式下失败。为什么？因为实现和证明的协调出了问题：智能体修改了一个模块的实现，导致另一个模块的证明失效；或者引入的构建错误波及整个仓库。图6还揭示了一个行为模式：所有配置都在运行的前半段就锁定了实现方案，之后几乎不再改动实现，把所有剩余预算花在证明上。GPT-5.5（xhigh）中位情况下在第30分钟就确定了65行实现代码，然后在剩下60分钟里把证明从883行写到1077行。实现自由度成了一根“一次性杠杆”——用掉了就不能再用。这种“早期锁定实现”的策略，虽然避免了频繁修改实现带来的连锁反应，但也意味着智能体放弃了“通过重构实现来简化证明”的可能性。

这暴露了一个微妙的问题：智能体倾向于把实现当作固定脚手架，而不是可优化的对象。证明卡住了就死磕证明，而不回头重构实现以降低证明难度。这与人类形式化验证工程师的典型工作方式——在实现和证明之间反复调整——形成了鲜明对比。人类工程师在遇到证明困难时，经常会问自己：“是不是实现方式选得不好？换一种实现会不会更容易证明？”而当前的AI智能体似乎缺乏这种“元认知”——它不会主动反思实现选择对证明难度的影响，而是被动地接受初始实现，然后试图在证明上“硬啃”。

未来展望：迈向可扩展的自动化软件验证

Vero的意义不在于说“AI验证不行”，而在于第一次给出了一个可以用来量化进步速度的标尺。27/43这个数字是2026年8月这个时间点的成绩单。从RVBench到VeriSoftBench再到Vero，基准在变难，能力度量也越来越接近真实的软件工程需求。Vero上的10个所有模型都解不开的实例，就是下一个版本的GPT和Claude最值得瞄准的靶子。这些“硬骨头”实例代表了当前AI在形式化验证上的终极挑战，攻克它们将标志着AI验证能力的质的飞跃。

论文还提到了成本问题。表2报告了单次完整评估的成本——所有配置加起来的预算烧掉超过4万美元，这还只是单次运行。验证确实昂贵，但随着模型效率提升，这个成本正在以肉眼可见的速度下降。未来的方向很清晰：模型需要学会建立和维护可复用的引理库，学会在实现与证明之间反复权衡而不是一次性锁死，学会用全局视角组织证明——本质上，是学会像资深形式化验证工程师一样工作。这不仅仅是模型能力的问题，还涉及到智能体框架的设计：如何让智能体在证明过程中主动回顾和重构实现，如何让智能体在多个模块之间协调证明策略，这些都是未来研究的重要方向。

Vero把问题从“模型能不能写对代码”升级到了“模型能不能证明代码是对的”。这不仅是学术上的进步，更是把AI生成代码从“能跑”推向“可信”的关键一步。至少现在我们知道差距有多大、方向在哪里了。对于AI辅助软件工程这个领域来说，Vero提供了一个清晰的路线图：短期目标是让模型在更多实例上达到完整通关，中期目标是攻克那10个“硬骨头”实例，长期目标则是让模型能够在没有人工干预的情况下，自主完成整个软件仓库的形式化验证。这条路还很长，但Vero已经为我们标好了里程。

图7：运行结束时仍存在的失败情况。(a) 按仍失败规范占比分组的仓库。(b) 剩余规范按失败原因的分布。(c) GPT-5.5（xhigh）中失败规范不超过x条的仓库数量。

图7和图8进一步剖析了失败的模式：剩余失败规范主要集中在编码跨模块不变量、协议一致性和自定义数学理论的规范上。这些规范不是单个证明能解决的——它们需要智能体先发现共享不变量，把它组织成可复用的引理库，然后逐层推导到最终结论。比如，一个分布式共识协议的规范可能需要证明“所有节点最终会达成一致”，这个证明需要先建立关于消息传递、状态转换、故障模型等多个方面的引理，然后才能推导出最终结论。这种深层的、跨模块的推理，正是当前AI智能体最不擅长的。

龙迷三问

下面是龙哥对于大家可能的一些问题的解答：

这篇论文到底在解决什么问题？UC Berkeley联合多家机构推出Vero——首个仓库级形式化验证基准，要求AI智能体在Lean 4中同时实现代码并完成机器可检查证明。

这篇工作最值得看的点是什么？最强的GPT-5.5 (xhigh)配置在代码与证明模式下完全解决43个实例中的27个，在仅证明模式下解决25个；10个实例在所有配置和两种模式下都无法解决。最强的智能体在代码与证明模式下通过87.3%的规范，在仅证明模式下通过85.8%。

这篇工作的边界或风险在哪里？优点：(1) 首次提出仓库级别的形式化验证代码生成基准，填补了现有基准只关注单函数或仅证明生成的空白；(2) 设计了形式化审计机制，能够自动发现基准中的潜在错误；(3) 支持多种源语言（Python、Dafny、Verus、Coq）的翻译，具有可扩展性；(4) 提供了全面的反作弊机制，确保评估的公正性。缺点：(1) 仅支持Lean 4作为目标语言，限制了通用性；(2) 基准偏向于能干净翻译为Lean的代码，缺乏并发或时序协议的覆盖；(3) 审计机制只能证明形式化可满足性，无法确保规范的语义正确性和完整性。

如果你还有哪些想要了解的，欢迎在评论区留言或者讨论~

龙哥点评

论文创新性分数：★★★★☆

首次将“实现+证明联合生成”提升到仓库级，审计机制和防污染设计也颇具巧思，但单点技术并非全新。

实验合理度：★★★★☆

评估配置覆盖了主流前沿模型、两种任务模式、多角度结构分析，90分钟预算和“全解”评分标准都较合理；但模型种类还可再扩充。

学术研究价值：★★★★★

为“AI可信代码生成”提供了第一个可量化的仓库级标尺，明确了当前能力缺口和未来改进方向，后续研究很难绕开这个基准。

稳定性：★★★☆☆

最强的GPT-5.5（xhigh）有62.8%通关率，但第二名的Claude Opus 4.8只有18.6%——对模型配置高度敏感，稳定性一般。

适应性以及泛化能力：★★★★☆

横跨Python、Dafny、Verus、Coq四种来源语言，覆盖智能合约、分布式系统、密码学到基础算法，领域多样性做得不错。

硬件需求及成本：★★☆☆☆

一份完整的评估预算超过4万美元，GPT-5.5（xhigh）单配置跑完全部实例就要烧掉1万多美元，普通人玩不起。

复现难度：★★★★☆

数据、代码、评估流程全部开源，但完整复现需要数万美元的API调用预算，硬件门槛不高，经济门槛不低。

产品化成熟度：★★☆☆☆

当前是研究基准而非产品方案。代码加证明模式下只有最强模型能解六成实例，距离“AI自动产出可信软件仓库”还有明显差距。

可能的问题：论文对“完整解决”的标准偏严，只统计全解导致部分进步被低估；GPT-5.5（xhigh）的领先是否部分来自其训练数据与Vero的隐含关联，防污染论证尚未完全打消疑虑；43个实例规模仍偏小，统计功效有限。此外，人工审核的成本和可扩展性也是一个潜在瓶颈。

主要参考文献

[1] Vero: Can AI Agents Build Formally Verified Software Repositories? arXiv:2608.13522v1

[2] GitHub: https://github.com/sunblaze-ucb/vero

[3] Yang, K., et al. LeanDojo: Theorem proving with retrieval-augmented language models. NeurIPS 2023.

[4] First, E., et al. miniCodeProps: A minimal benchmark for proof assistant language models. 2024.

*本文仅代表个人理解及观点，不构成任何论文审核或者项目落地推荐意见，具体以相关组织评审结果为准。欢迎就论文内容交流探讨，理性发言哦～想了解更多原文细节的小伙伴，可以点击"阅读原文"，查看更多原论文细节哦！

AI写代码怕翻车？
仓库级验证正当时！
Vero一出，谁与争锋？
逻辑证明、规范校验、智能体实战，
欢迎加入龙哥读论文粉丝群，扫描下方二维码或者添加龙哥助手微信号加群：kangjinlonghelper。一定要备注：研究方向+地点+学校/公司+昵称（如图像处理+上海+清华+龙哥），根据格式备注，可更快被通过且邀请进群。
『龙哥读论文』微信群目前包含：图像处理、大模型及智能体、自动驾驶及机器人、AI医疗及AI金融5个群
wechat_helper