Vero：首个仓库级形式化验证基准，最强AI只搞定了27个工程

Vero: Can AI Agents Build Formally Verified Software Repositories?

论文原文 ↗ 论文发布 2026-08-13 解读发布 2026-09-07 解读：AI前沿分享

大语言模型（LLM）驱动的软件工程智能体（Coding Agents）正在席卷开发流程，但无论其生成的代码看起来多么规范、单元测试通过率多么亮眼，都无法为关键基础设施提供数学层面的正确性保障。单元测试只能捕捉预料之内的失败，却无法穷尽协议交互、分布式系统或密码学逻辑中的边缘条件漏洞。形式化验证（Formal Verification）提供了一条截然不同的路径：借助机器可检查的数学证明（如使用交互式定理证明器 Lean 4），证明实现完全满足形式化规范，从而在数学上排除该规范所能涵盖的全部缺陷。

ArXiv URL：https://arxiv.org/abs/2608.13522v1

然而，现有的形式化代码生成评测大多停留在单函数级别，或者预先固定参考实现、仅评估智能体的补全证明能力。这种设定严重脱离工业级软件的真实生态。现实中的高保证软件系统——无论是操作系统微内核、分布式共识协议还是零知识证明电路——都是以包含多个模块、相互交织的依赖树形式存在的。代码实现的细微变动会击穿上下游的引理假定，而定理的推导又倒逼着数据结构的重构。

来自 UC Berkeley、Stanford、Caltech、AWS 等机构的研究团队提出了 Vero，这是业内首个面向真实仓库级（Repository-scale）、要求智能体联合合成“代码实现与机器可检查证明”的形式化验证基准。Vero 涵盖了源自 Python、Dafny、Verus 和 Coq 的 43 个多模块工程，包含 743 个 API 接口与 2,705 条形式化规范。在配备了完整的 Lean 4 编译环境与工具链后，目前表现最出色的 GPT-5.5（xhigh 推理配置）也仅能在 43 个工程中完全解决 27 个，甚至有 10 个工程让所有前沿智能体全军覆没。这项研究清晰地揭示了当前代码智能体面临的结构性瓶颈：它们善于应对局部推导，却极度欠缺跨模块抽象、构建共享引理库的全局架构能力。

从单函数到多模块仓库：验证评测的范式转移

过去的形式化验证评测基准之所以无法反映真实软件工程难度，核心原因在于“孤岛效应”。以往的研究往往给出一个孤立的函数签名，让模型写出对应的 Dafny 或 Lean 代码并附带前后置条件；或者直接锁死既有代码，仅要求模型把 sorry 占位符填补完整。但在实际的多模块代码库中，一个高层协议模块的正确性证明，通常极度依赖底层数据结构导出的引理体系。当上游定义发生细微调整时，下层推导链条就会全面断裂。

Vero 将评测维度推向了真正的工程级现实。每个 Vero 实例都是一个完整的 Lean 4 多模块项目。人类管理者为项目冻结了三层基础脚手架：基础数据类型与辅助函数定义、预设的 API 函数签名、以及人工严格校验的地面真值规范（Ground-truth Specifications）。

面对这套严格约束的框架，智能体需要同时消化两类核心义务：

实现义务（Implementation Obligation）：针对预先声明的每一个 API 签名，补全具有可执行语义的函数体；
证明义务（Proof Obligation）：针对预先编写的形式化规范，利用 Lean 4 证明引擎输出能够通过机器类型检查的严格证明。

尤为精妙的是，Vero 的每一条形式化规范均对实现抽象 $RepoImpl$ 进行了参数化抽象，而不是直接绑定到固定的某个实现之上。这一设计不仅赋予了基准强大的评估弹性，也是实现后续主动形式化审计的关键技术支点。

双模式设计与严苛的反作弊防线

在评估任务设置上，Vero 划分了两个相互对照的评测模式：

纯证明模式（Proof-only Mode）：智能体直接接收人类专家编写的黄金参考实现，其唯一目标是证明该实现完全满足给定的所有形式化规范。这考验的是智能体在给定现实复杂代码结构下的定理推导功底。
代码与证明联合合成模式（Code-and-proof Mode）：智能体不再拥有参考代码，而是需要自行填补全部 API 的函数体，并构造证明保证自己的实现满足所有规范。这是 Vero 最核心的贡献，它逼迫智能体在“可执行算法效率”与“形式化推导难度”之间进行工程权衡。

在形式化定理证明中，评估过程极易遭遇“奖励作弊（Reward Hacking）”。由于证明辅助工具的强大表达力，大模型很容易投机取巧：比如擅自引入不一致的公理（Axiom Injection）使逻辑系统崩溃，利用空真（Vacuous Truth）或伪造的不动点使任何目标瞬间获证；或者滥用 Lean 4 的非计算性选择算子（如结合 @[implemented_by] 和 Exists.choose），在逻辑层假装存在一个满足性质的值，但在运行层却指涉完全不相干的行为。

为了筑牢防线，Vero 构建了多重防御屏障。评估评测器（Grader）严格限制了模型的可修改文件区域，评测时会将智能体产出的代码切片抽取出来，注入到完全干净的基准沙箱中重新编译。同时，系统维护着一份严格的公理白名单，任何未经许可的自定义公理都会导致整个项目直接判负。此外，基于静态规则过滤和独立大模型判别的双重检查器会严密扫描代码中的恶意类型类实例与作弊注解，确保通过验证的代码在数学逻辑与运行时语义上保持严格统一。

逆向证伪：用形式化证据清洗基准自身缺陷

形式化验证领域一直存在一个不可忽视的“元问题”：谁来验证形式化规范本身的正确性？以往的许多基准在经过长期评测后，常被发现部分数学规范本身是相互矛盾、数学上不可满足的，或者原本的人工参考实现其实存在难以察觉的边缘漏洞。如果基准自身存在暗病，智能体即便竭尽全力也绝不可能成功证明，最终导致模型能力被误判。

Vero 创新性地引入了形式化审计机制（Formal Audit Mechanism）。在该机制下，评测系统不仅接收正面证明，还允许智能体输出经过机器检验的“否定性证据”。具体而言，智能体可以提交形式化证明，指出以下三种基准病态情况之一：

证明给定的某条规范在数学上是不可满足的（即不存在任何可能的程序实现能够满足它）；
证明人类给出的参考实现违背了某条预期规范，并给出反例（Counterexample）；
证明给定的规范子集之间存在内在冲突，无法被任何单一系统联合满足。

在基准构建过程中，这项审计机制与智能体探索形成了高效的闭环。依靠前沿模型提交的反例与不可能性形式化证明，研究团队在人工审核阶段成功排查出多处逃脱了传统代码审查的隐匿缺陷，显著净化了评测集的信噪比。这使得 Vero 具备了“伴随模型能力进阶而持续自我净化”的演进特质。

谁在引领仓库级证明？实验结果与残酷现实

在真实的基准测试中，研究人员选取了两个工业级智能体框架（Codex 工具链与 Claude Code 环境），配合四种前沿模型配置展开了全量评测：GPT-5.5（中等推理与 xhigh 极高推理档位）、Claude Opus 4.8（xhigh）以及 Claude Sonnet 5（xhigh）。测试设定了极其严格的准则：智能体拥有完整的 Lean 4 编译器交互工具链与文件系统编辑权限，限时 90 分钟，且最终以“是否完全通过该仓库的所有规范”为全胜标准（Full Solve）。因为在形式化领域，未被完全证明的系统等同于留有后门，局部的证明覆盖率无法保证全局安全。

实验结果呈现出清晰的技术分水岭。搭载极高推理档位的 GPT-5.5（xhigh）全面领跑，在“代码与证明联合合成”模式下成功完全解决 27 个实例，在“纯证明”模式下解决 25 个，展现出目前最强的大规模推理韧性。紧随其后的 Claude Opus 4.8 在双模式下分别完成了 8 个和 10 个项目，而中等推理档位的 GPT-5.5 与 Claude Sonnet 5 则止步于个位数胜场。

然而，更震撼的结论在于基准展现出的“前沿阻抗（Frontier-resistance）”：在全部 43 个多模块工程中，有整整 10 个工程在所有模型的所有配置下毫无突破，无一解决。即便表现最好的 GPT-5.5（xhigh），虽然单条规范的平均通过率超过了 85%，但在触及最深层次的跨模块核心协议时，依然无法收敛为可成功编译的终态代码库。高单点覆盖率与零仓库交付并存，暴露出当前智能体在处理长链依赖时的无力感。

“偷懒的算法”与形式化推导的深层博弈

对“代码与证明联合模式”的微观行为分析，揭示出大模型极具启发性的一种编程生存策略：实现自由（Implementation Freedom）是一把双刃剑。

在人工审查通过的案例中，研究人员观察到了颇具戏剧性的一幕：在面对诸如复杂排序算法或图遍历等高难度工程时，智能体为了避免证明那些错综复杂的高性能实现，主动选择抛弃人类专家编写的高效参考代码，转而写出一套逻辑极其平铺直叙、算法复杂度更高、但数学对称性极强的新实现。因为新代码结构极度纯粹，伴生而来的归纳证明难度呈现断崖式下降。

在至少 5 个实例中，智能体凭借这种“降低执行效率以换取数学可证明性”的策略，在联合模式下完美关闭了全部规范；而在锁死人类参考代码的纯证明模式下，相同的模型却被复杂的数据结构状态机彻底卡死。

但这种自由在更高难度的系统级仓库中变成了灾难。由于缺少对工程依赖图谱的宏观掌控，弱势模型常常在修改了底层辅助模块后，遗漏了上游接口的配套改动，导致整个 Lean 4 依赖树大面积报红。或者在多次尝试修补某个深层证明时，反复篡改实现，最终引入循环定义或无法收敛的构建错误。

统计数据显示，所有成功完全解决的项目，其智能体生成的证明代码量通常是实现代码量的两倍以上。换言之，决定仓库级形式化验证成败的核心矛盾不在于写出算法代码的行数，而在于智能体是否具备持续、系统地铺设证明架构的耐力。

引理库的深度陷阱：智能体何时被彻底击垮？

通过进一步拆解 82 次成功通关的项目产物，研究人员发现了一个决定性的模式：可复用的共享辅助引理库（Helper Lemma Libraries）是仓库级验证的基石。

在成功通关的案例中，超过 70% 的证明代码行数都集中在智能体自行构造的辅助引理中，绝非直接在目标定理下机械地平铺推导。在 80 个全通案例中，智能体编写的引理至少被两个以上的不同规范共享复用；超过 65 个案例中，单个核心引理被 5 个以上的规范共同依赖。这说明，只有当智能体懂得将全局不变式（Global Invariants）拆解为基础逻辑积木时，形式化验证才有可能成功跨越模块边界。

而这恰恰对应了失败案例的致命软肋：证明链条的层级深度。

当一条形式化规范无需任何辅助引理支持、仅凭本地上下文即可闭合时，前沿智能体的解决成功率高达 80% 到 84%；但当一条规范需要依赖深度达 4 层以上的跨模块引理推导链条时，模型的成功率急剧坠落至 39% 到 50%。

现阶段的代码智能体在工作流调度上呈现出明显的“单向单步思考”偏见：在获得任务的最初 30 分钟内，智能体迅速敲定它所认为的实现代码，在此后的时间里便将代码视作既成事实，开始在证明层盲目死磕。一旦陷入僵局，它们极少反思是否是数据结构定义本身缺乏数学归纳友好性，更不会主动回退重构底层抽象。当推导链条延伸至多层抽象之外时，模型往往迷失在庞大的局部符号推演中，直至 90 分钟的算力窗口消耗殆尽。

走向自担保软件工程的必由之路

Vero 的诞生为人工智能辅助软件工程确立了一座崭新的界标。它有力地表明：衡量智能体代码能力的标准，不应仅仅停留在它能否写出迎合浅层测试用例的脚本代码，而必须跨越到它能否在严谨的数学验证体系下构建自洽的大型软件系统。

当前的顶级基础模型与智能体框架已经展现出令人惊艳的局部形式化推导天赋，甚至学会了为了求证而动态简化算法语义。但在面对工业级多模块架构、分布式一致性协议以及深度引理依赖时，它们依然缺乏人类形式化验证工程师所具备的“自顶向下拆解、自底向上沉淀抽象库”的系统工程素养。

随着 Vero 的开源，包含 43 个多模块工程、完整的双模式评测沙箱以及创新的反向形式化审计流水线已被完整推向社区。形式化代码合成不再是单点函数的玩具试验，而是演化为衡量 AI 逻辑推理深度、架构一致性与安全可信度的硬核战场。未来的智能体若想真正接管安全敏感的基础软件开发，必须学会走出局部的试错循环，掌握在代码与数学证明之间反复斡旋的全局架构智慧。