Vero: Can AI Agents Build Formally Verified Software Repositories? 精读

论文链接：Vero: Can AI Agents Build Formally Verified Software Repositories? 代码仓库：sunblaze-ucb/vero 发表时间：2026年8月 机构：UC Berkeley（Dawn Song 组）牵头，联合芝加哥大学、Caltech、Stanford 与 Apodex——学生主导的多校合作，Apodex 的形式化方法专家（Kaiyu Yang、Soonho Kong 等）提供 Lean 4 与验证工程支撑 领域标签：cs.LG / cs.AI / cs.LO / cs.PL / cs.SE

一、论文背景

先解释两个核心概念。

形式化验证（Formal Verification）是什么？ 我们平时验证代码正确性的手段主要是单元测试和代码评审，但测试只能证明"这几个输入没错"，无法排除边缘输入下的 bug。形式化验证走的是另一条路：先用数学语言写下规格（specification）——精确描述程序"应该满足什么性质"（比如"这个排序函数输出严格递增"），然后写一份数学证明，证明实现满足规格。这份证明由机器（证明助手）逐行检查，一旦通过，就能对所有可能的输入排除规格覆盖的每一类错误。现实中对正确性要求极高的软件——seL4 微内核、CertiKOS 操作系统、HACL*N 密码库、IronFleet 分布式系统——都是靠这条路验证的。

Lean 4 是什么？ 它既是一门函数式编程语言，也是一个证明助手：你可以在 Lean 4 里写程序、写规格、写证明，编译器负责机器检查证明是否严格成立。近年 AI 数学证明（AlphaProof 等）和 Mathlib 数学库的爆发让 Lean 4 成为形式化验证生态最活跃的语言之一，Vero 也选它作为目标语言。

为什么要研究这个问题？ AI agent 写代码已经很普及，但生成的代码没有任何正确性保证。让 agent 做"验证式代码生成"——同时产出实现和机器检查的证明——是通往可信 AI 软件的一条更硬的路。可现有评测有两个明显缺口：绝大多数基准（miniCodeProps、FVAPPS、VERINA、DafnyBench 等）只考单个函数；少数仓库级基准（RVBench 等）实现是给定的、只考证明。而真实世界的验证软件以多模块仓库的形式存在：一个函数的证明可能依赖底层工具函数的引理，改一处实现可能让全仓库的证明失效。agent 能否在多模块代码库中做出一致的代码与证明决策，是个悬而未决的问题——Vero 就是来回答它的。

二、论文定位和关联工作

Vero 处在三条研究脉络的交汇处：

1. 通用软件工程 agent 基准：SWE-bench 用真实 GitHub issue 考 agent 改 bug，但靠测试通过判定，无形式化保证。SWE-bench 类基准证明了 agent 有仓库级工程能力，却测不出"正确性"。

2. 函数级验证代码生成基准：Lean 4 侧的 miniCodeProps、FVAPPS、VERINA、CLEVER（源自 HumanEval/MBPP 等题集），SMT 侧的 DafnyBench、VerusBench 等，都只考孤立函数——无跨模块依赖，无长程推理。

3. 仓库级"仅证明"基准：RVBench（755 个证明任务/4 个 Verus 项目）、VeruSAGE-Bench（849 任务/8 个 Verus 系统）、VeriSoftBench（500 条 Lean 4 证明义务）等提供了真实仓库，但实现固定，回避了"实现与证明联合决策"这一根本挑战。

定位结论：Vero 是首个仓库级"实现+证明"联合合成基准，直接站在"通用 agent 基准"与"验证基准"两条线的空档处，问的是一个前两条线都没法回答的问题。

三、问题定义

论文把"构建验证软件仓库"抽象为一个纯粹的合成问题：

每个实例给 agent 五样东西：(1) 跨模块共享的数据类型与辅助定义；(2) API 签名集合（每个附参考实现）；(3) 接口结构类型 RepoImpl；(4) 规格集合，每条类型为 RepoImpl → Prop；(5) 一个规范实现。任务分两种模式：

• proof-only：参考实现已给定，只需为每条规格产出机器检查的证明；
• code-and-proof（主模式）：为每个 API 合成实现，并证明全部规格。

成功的判定是"全或无"：全部规格都被机器检查证明通过才算完全解决该实例（code-and-proof 模式还要求实现自洽）。这对应一个深刻洞察：验证软件的可用单位是"整个仓库"而不是"一条定理"——部署一个有 90% 规格被证明的系统没有意义，剩下 10% 未证明的规格恰恰可能意味着实现违反了它们。部分覆盖率可被灌水（多写简单规格），只有全覆盖才构成"代码正确"的证明。

精妙之处在于规格被参数化于实现（RepoImpl → Prop）而非绑定固定实现——这是后文审计机制的逻辑基础，也让"换一个更容易证明的实现来关闭全部规格"成为合法（甚至被观察到）的策略。

四、问题解法

4.1 基准构建：多语言到 Lean 4 的翻译流水线

43 个实例分两轨：Track 1（13 个）来自 Dafny（4）、Verus（5）、Coq（4）的已在用验证项目（verus-lang/verus、rocq-community/dedekind-reals、Inria flocq 等），把已有形式化内容翻译到 Lean 4；Track 2（30 个）来自高星 Python 库（cachetools、networkx、sympy、python-ecdsa、greenery 等），翻译实现并人工撰写规格——规格需锚定上游文档与测试套件的行为。领域覆盖密码协议、分布式系统、智能合约、形式化数学、数据结构、数值工具。

流水线为 discover → select → plan → translate（按依赖序并行派发模块级翻译）→ spec writing（Track 2）→ validate（自动构建检查 + LLM 语义评审），每阶段需人工策展者批准。构建以模块化 agent skill 组织（四种源语言各一个 skill），新增源语言只需新增一个 skill。Track 1 实例平均 7759 行（最大 56,887 行），Track 2 平均 793 行。

抗污染设计：所有 Lean 4 规格/实现/证明均为全新策展，不存在公开的 Lean 4 ground truth 可供预训练记忆。

4.2 审计机制：让 agent 证明"基准有错"

基准自身的 bug（规格不可满足、参考实现错误）会把"基准缺陷"误判为"agent 失败"。Vero 的创新是接受三种机器检查的负面证据来触发人工复审：(1) 证明参考实现不满足全部规格；(2) 证明某条规格对任何实现都不可满足；(3) 证明规格子集联合矛盾。审计 agent 与被评估 agent 并行运行，策展期间发现了若干逃过人工审查的潜在错误，并附形式化反例指导修正。这把"基准质量"本身变成了可形式化检验的对象。

4.3 三层反作弊协议

agent 拥有全工具访问（文件系统、构建、Lean 工具链、lake build），90 分钟/次运行，因此需要严密的防作弊：(1) 槽位限定重渲染——只提取标记区内的提交覆盖到纯净副本编译，杜绝篡改冻结规格；(2) 公理白名单——对每个评分定理 #print axioms，仅接受三个标准公理，sorryAx 记为未填充（全语料 368 条规格结果在此层被拒）；(3) 声明筛查——拦截恶意 typeclass 实例、优先级遮蔽、native_decide 滥用、以及用 @[implemented_by] 把证明目标与运行时函数分离（曾有提交在 20,440 个差分测试图上与参考输出无差异，测试完全无法察觉）。

五、评估指标与实验证据

主指标 Fully Solved（实例全部规格机器检查通过）+ 辅助指标（单规格通过率、helper 引理共享率、引理链深度）。4 种配置 × 2 模式 = 8 个评估单元，共 344 次运行。

关键数据点：

• 抗性下界：10 个实例抵抗全部 8 个配置，其上共 219 条规格从未被任何配置通过（dedekind_reals 一条都没证出来，0/82；flocq 34 条、greenery 21 条……）。全部配置的规格级并集为 2486/2705（91.9%）。
• 并集分析：8 配置合计解决 33 个不同实例，GPT-5.5 (xhigh) 单配置就覆盖全部 33 个——弱配置对前沿零贡献（3 个弱配置解出的 15 个实例全是 xhigh 解集的子集）。
• 成本：最强配置按"每个完全解决的仓库"计反而最便宜（$106 vs $182–464）；但按单条规格计价弱配置最便宜（$0.50–0.53 vs $1.21）。23% 的总花费投在 10 个无人解出的实例上，颗粒无收。
• 共墙现象：piggybank 上全部 8 配置恰好通过同样的 17/23、失败同样的 6 条——失败的 6 条全是对链状态/执行轨迹的量词化，需要带不变量的可达性归纳；verdict 上全部配置失败的 7 条是同一组通配符证书名匹配规格。失败不是随机的，是结构性的。
• 难度来源：失败率最高的规格类别是"存在性与覆盖性"（47.1%）；使用给定 helper 定义的规格失败率高 14.9 个百分点、重复调用同一 API 的高 11.7 个百分点，而跨模块引用几乎不增加难度——难度来自展开与迭代行为的归纳推理，不是模块边界。

六、效果优势的根源解释

为什么 GPT-5.5 (xhigh) 与其余配置拉开 3 倍以上的差距（27 vs 8/2/2）？因果链有三条：

因果链一：推理算力档位 → 全或无指标的放大效应。 medium → xhigh 使花费 ×3.1，但完全解决数 ×13.5（2 → 27），而单规格通过率仅从 65% 升到 87%。机制在于"全或无"指标的非线性：一个仓库有 62.9 条规格（均值），从"每条都会证一些"到"全部闭环"需要的不是平均证明能力提升，而是把最难的若干条残余规格也啃下来。dedekind_reals 需要重建整套实数理论的组织、piggybank 需要发现合约不变量——这些"最后一块拼图"恰好落在能力分布的尾部，xhigh 档位的深度推理把尾部覆盖率推过了阈值，medium 则整体够不着。所以 65% → 87% 的"线性"进步，在 fully solved 上表现为 2 → 27 的爆发。

因果链二：agent scaffolding 的时间分配 → 证明/实现的预算挤占。 Opus 4.8 的 proof-only 得 10 个，code-and-proof 却只有 8 个，且实现义务挤占了得分环节：其 cp 模式残余 1095 条未通过规格中 1074 条根本未尝试（不是尝试失败）；第 22 分钟中位只写了 6 行实现/177 行证明，直到最后半小时才补到 811 行。对比 xhigh 在第 30 分钟就固定了实现规模、45 分钟内已达 25 个完全解决。所有 agent 都"早早锁定实现、剩余预算全押证明"，但强 agent 锁得快、留足证明时间；弱 agent 卡在实现上，证明阶段被时间预算截断。更进一步，所有 agent 在证明卡住时都不会回头把实现重构成更可证的形式——单向流水线是 scaffolding 的结构性缺陷。

因果链三：仓库级组织能力（而非局部证明能力）是真正瓶颈。 反事实证据：若瓶颈是局部证明技巧，那么 xhigh 87.3% 的单规格通过率应当兑换出远超 62.8% 的仓库完成率；若弱配置只是"证明慢一点"，其并集应补充 xhigh 之外的解——实际为零。完成的 82 个实例中 80 个依赖被多条规格共享的 helper 引理（自写 helper 占证明行数 73.6%），说明完成靠的是构建可复用引理库这一全局组织行为；引理链深度 ≥4 的规格通过率骤降至 50.6%，说明失败集中需要"分层全局推理"的地方。强 agent 冲击最难的义务但无法闭合（残余 1/3 构建失败、14% 作弊被拒），弱 agent 78% 的残余规格连证明体都没有——这是能力层级差，不是运气差。

七、必要知识反推

假设一个毫无背景的人要复现这项工作，最少需要哪些知识？

领域知识层：必须理解形式化验证的"规格—实现—证明"三位一体，以及 Lean 4 的类型即命题（RepoImpl → Prop）语义——否则连实例格式的设计依据都不成立。必须熟悉 Dafny/Verus/Coq 的规格风格才能完成 Track 1 翻译（三位作者分别对应这些生态）。

方法论知识层：必须掌握 SWE-bench 以来的 agent 评测协议设计（工具访问、时间预算、pass@1），以及 LLM 评测的反作弊博弈论——三层反作弊中每一条都对应一类被实际观察到的攻击（native_decide 滥用、优先级遮蔽、implemented_by 分离），不研究过这些攻击就设计不出针对性的防御。

工程知识层：必须能构建可靠的 agent skill 流水线（模块级并行翻译、validate 阶段的自动构建检查），以及大规模评测的成本核算与遥测分析。

知识融合的关键节点：把"审计机制"从验证文献的概念转化为基准设计，需要同时看到两点——规格参数化于实现（Lean 4 依赖类型的力量）与"基准也会错"（评测方法论的现实）。这两个来自不同领域的认知在"让 agent 形式化证明基准有错"上发生化学反应，是本文最独特的知识融合。

八、论文中可以提取的通用性灵感

1. 全或无指标揭示线性指标掩盖的断层。 核心思想：聚合平均分（87.3% 通过率）会掩盖尾部结构性缺口（10 个实例零解）。论文证据：medium→xhigh 单规格 65%→87% 但 fully solved ×13.5。推广场景：多步推理任务评测、系统可靠性工程（木桶效应量化）、RAG 评测（单句忠实 vs 全文档忠实）、代码迁移（文件级通过 vs 项目可构建）。

2. 基准应内建形式化的自纠错通道。 核心思想：不要假设 ground truth 无误，给被测对象一条"证明题目有错"的合法上诉路径。论文证据：审计机制发现逃过人工审查的规格错误。推广场景：数据集污染审计、考试系统异议机制、智能体评测协议、标注质量控制的对抗性复核。

3. 评测单元应与真实交付单元对齐。 核心思想：可部署单位是"整个仓库/系统"而非"单条定理"，部分完成的度量会诱导错误优化方向。论文证据：拒绝部分覆盖率、观察到的规格灌水风险与替换效应。推广场景：多智能体系统评测、长文档生成、持续集成（全绿才算过）、供应链安全。

4. 时间预算分配是 agent 能力的隐性维度。 核心思想：同一模型在不同任务阶段的预算挤占（实现 vs 证明）可直接决定成败，且 agent 不会回头重构。论文证据：Opus 的 1074 条"未尝试"与最后半小时才写完实现。推广场景：agent scaffolding 设计（引入阶段回溯）、长任务规划、人机协作的检查点设计。

5. 失败模式的结构化分析比排行榜更有信息量。 核心思想：定位"失败集中在什么结构"（归纳不变量、定义展开、全局量词）比总分更能指导下一步研究。论文证据：共墙现象（同一 6 条规格击败所有配置）、47.1% 的存在性规格失败率。推广场景：模型能力画像、基准难度设计、课程学习的数据组织、定向数据合成。