Vero：首个仓库级实现与证明联合合成基准，最强 Agent 仅解出 43 个实例中的 27 个

现有基准尚未衡量智能体能否在多模块仓库中同时生成实现与机器检查证明。

• 场景：作者认为编程智能体的正确性通常靠单元测试和人工审查。这些方法能抓住预期失败，但不能排除规格所覆盖的全部边界缺陷和安全漏洞；作者称这类问题在协议与基础设施软件中损害最大。形式验证用机器检查证明，对全部输入排除规格所刻画的缺陷类。
• 不足：作者称既有基准或只评单函数，或在固定实现上只评证明。仓库级任务不能靠放大函数级技术解决，因为一条证明可能依赖底层工具引理，改一处实现也可能使全库证明失效。
• 观察：作者认为智能体必须判断整个代码库的一致性，而不能只局部处理单个函数。作者还称，从操作系统内核到密码协议和分布式系统，真正的已验证软件存在于仓库中。
• 提出：作者提出 Vero，并称据其所知它是首个在仓库级评测联合实现与证明生成的 Lean 4 基准。它含 43 个多模块实例、proof-only 与 code-and-proof 两种模式，以及用形式反例审计规格和参考实现的机制。

论文第 2 节用四类限制组织既有基准，并据此定位 Vero。

函数级验证代码生成

• Lean 4 单题：miniCodeProps、FVAPPS、VERINA 和 CLEVER 评独立任务，题目来自 HumanEval、MBPP、APPS 等算法题集。
• SMT 验证器：DafnyBench、VerusBench、AlgoVeri、VeriCoding、VerifyThisBench 和 VeriEquivBench 针对 Dafny 或 Verus，对象是单个算法或方法。
• 论文的批评：作者称这些基准推动了孤立任务上的进展，但不能捕捉真实已验证代码库所需的跨模块依赖和长程推理。

仓库级、只评证明

• Verus 与 Lean：RVBench 含四个 Verus 项目上的 755 个证明补全任务；VeruSAGE-Bench 从八个 Verus 验证的 Rust 系统抽出 849 个证明任务；VeriSoftBench 打包开源形式化开发中的 500 个 Lean 4 证明义务。
• Coq：CoqStoq 提供仓库级定理语料用于证明合成；FSCQ 证明生成的案例研究针对已验证系统软件中的证明补全。
• 论文的批评：作者称这些基准都给出参考实现，只评能否完成证明义务，因而省略实现选择如何改变证明难度，以及两种制品必须在全库保持一致。

数学证明与污染

• Mathlib：LeanDojo、LeanAgent 和 APE-Bench 建立在 Mathlib 上。作者称它们推动了神经定理证明，但数学证明的结构与命令式软件验证差别很大，后者与可执行定义、数据类型和带效应的行为耦合。
• 预训练暴露：作者引用公开程序源的参考解可能进入预训练数据这一担忧，并称直接复用这类来源的基准会继承该暴露。Vero 的做法是跨语言取材并手工做成新的 Lean 4 形式化，使任一实例都没有可直接获得的 Lean 4 参考证明。

评测协议与基准自身错误

• 工具访问：作者称多数既有基准评的是单次或简单迭代下的原始 LLM 输出，没有部署中的编程智能体所使用的工具访问。Vero 评的是有完整工具访问的前沿编程智能体。
• 地面真值与作弊：作者引用形式验证基准中地面真值错误难以和智能体失败区分的问题，并称既有仓库级基准缺少反作弊，因而分不清报告结果是验证能力还是奖励黑客。Vero 用机器检查的反面证据做审计，并用公理白名单和限制定义编辑对付奖励黑客。

比较对象：实验没有引入另一套仓库级系统作外部基线，而是在 Vero 的两种模式上比较四种前沿编程智能体配置（Section 4）。作者称，据其所知 Vero 是首个在仓库级评测联合代码与证明生成的基准，并保留 proof-only 以便和只评证明的设置对照。

Vero 把真实仓库收成带固定接口和规格的多模块 Lean 4 项目，让编程智能体在 proof-only 或 code-and-proof 下补齐实现与机器检查证明，并用形式反例审计基准缺陷。

实例格式

策展者固定数据类型与辅助定义、API 签名和形式规格。实例包含共享定义、API 集合及其参考实现、汇集全部 API 的结构 RepoImpl、类型为 RepoImpl → Prop 的规格集合，以及 canonical。proof-only 用参考实现填充 canonical，code-and-proof 由智能体填充。规格不绑死单一实现，以便切换证明对象并支持审计（Section 3.1，Figure 2）。智能体在两种模式下都要填上标为 sorry 的证明义务；code-and-proof 还要填写 canonical 的函数体。

两种模式与反作弊

• proof-only：对每条规格 Si 证明 Si(canonical)，canonical 为参考实现。
• code-and-proof：为每个 API 提供函数体，并证明智能体自己的 canonical 满足全部规格。作者称实现可以改成更易证明的形式，但改动也会使跨模块证明失效。
• 完全求解：两种模式都要求全部规格被证明。作者认为未证明的规格会留下它本可抓住的缺陷，部分覆盖会被容易规格抬高；code-and-proof 中未证明也可能表示实现违反规格。
• 评分：评分器只抽取标记区域内的提交，叠到干净副本上再编译，从而恢复被改的规格、辅助定义、签名或被删的证明义务。公理白名单仅接受 Classical.choice、propext、Quot.sound；依赖 sorry 记为未填写，其他公理记为泄漏。规则与 LLM 评审再筛可使证明变平凡、或把逻辑语义与可执行行为拆开的声明，包括恶意 typeclass，以及 noncomputable 选择配合 @[implemented_by]。附录 D 说明这些机制。论文未写明该 LLM 评审是哪个模型。评测使用 Lean v4.29.1。

策展与语料

流水线分阶段由 LLM 智能体执行，每阶段经人工批准。Track 1 翻译 Dafny、Verus、Coq 中已有的类型、定义和规格；Track 2 翻译 Python 实现，并按上游文档与测试撰写规格，要求每个 API 受多条相互关联的规格约束。阶段包括 discover、select、plan、translate，Track 2 另有规格撰写，最后做结构、构建和语义审查。选择看真实来源、领域、规模与难度，以及能否忠实译成中等规模 Lean 脚手架。

43 个实例中 Track 1 为 13、Track 2 为 30，共 743 个计分 API、2,705 条规格。Table 1：Track 1 每实例 API 均值 36.0、最大 88，规格均值 92.8、最大 203，所选上游有效代码行均值 7,759、最大 56,887；Track 2 对应为 9.2/71、50.0/109、793/4,047。源码行数不含空行和注释。领域覆盖智能合约与区块链、分布式系统与共识、安全相关基础设施、形式化数学、数据结构、算法和数值工具。作者称没有公开的 Lean 4 参考证明。新增源语言只需新的 agent skill；目前覆盖 Python、Dafny、Verus、Coq。

形式审计

审计不把证不出来直接当成智能体失败，而接受三类机器检查反面证据：参考实现违反全部规格的合取；某条规格不存在任何实现满足；某个子集联合不一致，但各成员仍可单独满足。策展中该机制找出人工审查遗漏的错误，并用反例指导修正。附录 F：发布集上裁定 38 个规格缺陷（9 个实例）和 6 组联合不可满足，均已修复；第 4 节评测使用修复后的基准。38 例中 34 例依据智能体提交的干净证明，3 例为公理检查失败后作者重建，1 例为独立复现的 native 求值。附录 F 还称 Claude Opus 4.8 找到 33 例，Codex 找到 30 例，双方都找到 25 例。

实验设置

• 配置：Codex v0.140.0 配 GPT-5.5，推理力度为默认 medium（正文亦称 mid）和 xhigh；Claude Code v2.1.191 配 Claude Opus 4.8 与 Claude Sonnet 5，二者均为 xhigh。智能体可改文件、调用构建和 Lean 工具链，Lean 为 v4.29.1。
• 数据：Vero 的 43 个实例，743 个计分 API、2,705 条规格。两种模式都评。
• 指标：主要报告完全求解的实例数。作者采用完全求解而不是部分规格覆盖，因为容易规格会抬高部分覆盖，且 code-and-proof 中未证明的规格可能表示实现违反它。另分析规格通过率、失败原因和证明结构。
• 判定：独立评分器在干净状态重建，执行公理白名单和反作弊筛查。其中的 LLM 评审论文未说明模型。通过指机器检查证明且未被判为作弊或公理泄漏。
• 规模：每个配置、每种模式、每个实例一次最终提交，共 344 次运行，时间预算 90 分钟（Figure 3）。论文未报告重复次数或采样温度。附录 A 的 Table 2 给出合计费用；附录 E.4 称 344 个单元中 223 个因墙钟上限被中途终止、没有终端用量记录，其费用按已测运行的中位美元/分钟估计。

主结果

据 Figure 3(a,b) 与 Section 4.2，完全求解实例数为：

配置	code-and-proof	proof-only
GPT-5.5 (xhigh)	27/43	25/43
Claude Opus 4.8 (xhigh)	8/43	10/43
GPT-5.5 (mid)	2/43	6/43
Claude Sonnet 5 (xhigh)	2/43	2/43

• 作者称 Vero 对前沿配置仍然难：10 个实例在两种模式的全部八个配置下都未被完全求解。Figure 3(c) 按模式统计解出同一仓库的模型数：code-and-proof 为至少 3 个 n=3、2 个 n=5、1 个 n=20、0 个 n=15；proof-only 为 n=3、9、15、16。作者称多数被解出的实例只被一个配置解出。
• GPT-5.5 (xhigh) 在 45 分钟内达到 25 个和 23 个完全求解。作者认为瓶颈不是局部证明技巧：该配置规格通过率为 code-and-proof 87.3%、proof-only 85.8%，高规格覆盖并不等于仓库完成。
• 摘要称最强智能体在最难仓库上没有证明任何规格。Table 4 中 dedekind_reals 在八个单元均为 0/82。

实现自由度与证明工作量

• 172 个实例–智能体配对中，双模式都完全求解 26 个，仅 code-and-proof 13 个，仅 proof-only 17 个，都未解 116 个（Figure 4(a)）。作者检查后称，至少五个配对、三个仓库里，智能体用更简单、仍满足同一规格的实现替换难证的参考算法；这五对在 code-and-proof 证明全部 250 条规格，对固定参考实现只证明 201 条。作者称每处替换在行为上正确，而不是取巧，得到的是可证明性，放弃的是效率。
• 作者报告该效应并不对各模型对称：只在一种模式完全求解时，xhigh 为 code-and-proof 8 个、proof-only 6 个，较弱配置更常只在 proof-only 解出（附录 E.2）。规格粒度上，code-and-proof 使 xhigh 多通过 42 条、mid 多通过 130 条，但使 Opus 少通过 360 条。
• Figure 4(b–d) 中，完全求解与未完成运行的实现行数接近，证明文本大约为两倍，证明/实现比也更高。中位证明行数在 code-and-proof 为 1,181 对 626，proof-only 为 1,320 对 562（n=39/133 与 43/129）。附录 G 记 7/344 次运行因实现无法构建得 0 分。Table 4 中，Huffman 上 Opus 的 proof-only 为 116/127、code-and-proof 为 0/127；xhigh 的 unicode 为 0/46 与 36/46，正文未单独解释后一格。

失败位置与规格类型

• 82 次完全求解中，辅助定理占证明行数的中位数为 code-and-proof 73.6%、proof-only 71.6%（Figure 5(b)）。80/82 至少有一条辅助定理被两条及以上规格共用，65/82 被至少五条共用。作者认为完成的仓库围绕可复用引理库，而不是每条规格独立证明。
• 以 xhigh 的 proof-only 完全求解测量辅助链深度，再看其余七次运行（Figure 5(c)）：无需辅助定理时通过率为 83.9%（3,086/3,676，code-and-proof）和 80.1%（2,209/2,757，proof-only）；深度至少为 4 时为 50.6%（1,110/2,192）和 39.1%（643/1,644）。作者认为深层规格需要先为底层定义建立前置引理链。
• 按仓库均衡后，存在性与覆盖类失败率最高，为 47.1%，作者称在每种敏感性分析下仍最高；状态更新类为 20.9%（Figure 8(a)）。结构与成员类在 262 次未完成评测中出现 222 次（Figure 8(b)）。使用给定 helper 或重复调用同一计分 API，失败率高 14.9 和 11.7 个百分点，八个配置都更高；引用多个 API 或另一模块为 +5.0、+0.3 个百分点（Figure 8(c)）。作者认为难度来自展开给定定义和迭代行为，而不是跨越模块边界。xhigh 在 35/43 与 34/43 个仓库上至多四分之一规格仍失败；其 16 个未完成的 code-and-proof 仓库里，只有 6 个距完成不超过五条，9 个剩余超过十条（Figure 7）。作者称剩余失败不是差一点，而是共享少数缺失不变量的一簇规格。

其他消融与分析

• 正文称 xhigh 约三分之一剩余规格在构建时失败，另有 14% 被判作弊；Opus 与 Sonnet 约 78% 的剩余规格没有证明体（Figure 7(b)）。
• 八配置并集完全求解 33 个不同实例，与 xhigh 两模式并集相同；规格并集 2,486/2,705（91.9%），另有 219 条从未通过，全部落在那 10 个未完成实例（附录 E.3）。
• 这 219 条为：dedekind_reals 82、flocq 34、greenery 21、reedsolo 21、galoistools 18、ntheory 13、base58 11、verdict 7、unicode 6、piggybank 6（附录 E.3）。
• piggybank 上八个配置都通过 17/23 并失败同一 6 条；verdict 上 Opus 的 code-and-proof 为 112/119，其 7 条残余被全部八个配置失败（附录 E.1）。
• Figure 6：各配置在运行前半段达到最终实现规模中位数，证明文本增长到截止。xhigh 在第 30 分钟固定中位 65 行实现，证明文本从 883 行增至 1,077 行。图中另三个配置的实现中位数标为 48、49、49，正文未逐一对应。
• 附录 D：368 个规格结果在公理层被拒，集中于 base58（67）、verified_bitmasks（60）、reedsolo（53）、sortedcontainers（52）。

作者指出的局限与后续方向

• 只面向 Lean 4：Limitations 写明目前只以 Lean 4 为目标，原因是它是基于 LLM 的形式推理中特别活跃的生态。Track 1 翻译了 Dafny、Verus、Coq 的规格与不变量结构，流水线可扩展到其他目标语言（Section 3.3）。
• 语料偏向易译代码：作者写明语料偏向能干净译入 Lean 的代码，主要缺失类是上游形式化无法移植到中等规模 Lean 脚手架的并发或时序协议（Limitations）。
• 增量维护：作者把对增量维护任务做形式验证的评测称为有价值的未来方向（Limitations）。
• 审计边界：作者写明审计认证的是形式可满足性，不能保证规格在语义上正确或完备；因此全部规格经人工审查，Track 1 还对照源语言形式化做了交叉检查（Limitations）。
• 未写入规格的性质：附录 H.4 称，code-and-proof 的完全求解只认证实现满足已给出的规格，不认证规格未提及的性质；对数据结构库，复杂度就是会被换掉的这类性质。作者称形式化开销需要源仓库未提供的代价模型，因此只记下这一缺口。

实验覆盖范围

• 评测配置为 Codex v0.140.0 上的 GPT-5.5（medium 与 xhigh）和 Claude Code v2.1.191 上的 Claude Opus 4.8、Claude Sonnet 5（均为 xhigh），共四种，覆盖 proof-only 与 code-and-proof（Section 4.1、附录 A）。
• 实例 43 个：Track 1 为 13 个，源语言 Dafny、Verus、Coq；Track 2 为 30 个，源语言 Python（Section 3.4、Table 1）。计分 API 743，规格 2,705。
• 每个配置、模式、实例一次运行，合计 344 次，时间预算 90 分钟，Lean v4.29.1（Figure 3、附录 E.4）。论文未报告重复次数。
• 结果包含完全求解、规格通过、失败原因、语义类型和证明结构（Section 4、Figure 5–8）。反作弊中的 LLM 评审论文未说明具体模型（Section 3.2）。
• 附录 F 记录策展审计在发布集上裁定并修复了 38 个规格缺陷和 6 组联合不可满足；第 4 节结果针对修复后的基准。

Vero 评测编程智能体能否在真实多模块仓库中同时交出实现和机器检查证明。

• 问题：作者认为测试和人工审查排除不了规格所覆盖的全部边界缺陷，而既有基准停在单函数，或只在给定实现上评证明。
• 做法：从 Dafny、Verus、Coq 和 Python 整理 43 个 Lean 4 实例，固定接口与人工规格，共 743 个计分 API、2,705 条规格。proof-only 只证参考实现；code-and-proof 自写实现并证明。完全求解要求全部规格通过。形式审计接受规格不可满足或参考实现错误的机器检查证据；反作弊限制公理、标记区外修改，以及把证明目标与运行行为拆开的声明。
• 结果：在 90 分钟、四种前沿配置下，GPT-5.5 (xhigh) 的完全求解为 code-and-proof 27/43、proof-only 25/43；Opus 为 8/43 与 10/43，GPT-5.5 (mid) 为 2/43 与 6/43，Sonnet 两种模式均为 2/43（Figure 3）。10 个实例在八个配置下都未完全求解。xhigh 的规格通过率为 87.3% 与 85.8%，作者认为这不等于仓库完成。
• 作者的解读：未解实例集中在跨模块不变量、协议一致性和自定义数学理论。完成的求解把大部分证明行放进可复用引理。实现自由度既让智能体换上更易证明的算法，也会在更难实例上改坏已有证明或引入构建错误。作者认为差距在仓库级组织，并希望 Vero 成为衡量通向实用规模已验证软件合成的测试床。