Dawn Song 团队发布首个代码库级形式化验证基准 Vero
Dawn Song 团队（UC Berkeley 等高校联合）发布 Vero，首个面向代码库级联合实现与证明合成的形式化验证基准，用于评估 AI 构建经形式验证软件的能力。结果显示前沿模型远未达标：90 分钟预算下最佳配置 GPT-5.5（xhigh 推理档，code-and-proof 模式）仅完全验证 43 个仓库中的 27 个，proof-only 模式为 25 个，另有 10 个仓库在所有配置下均告失败，说明「完全验证的 AI 生成软件」仍处于早期。
已确认
- Vero 由 43 个多模块 Lean 4 实例组成，从 Python、Dafny、Verus、Coq 等真实仓库策划而来，涵盖密码学与分布式系统等领域；每个实例含固定的数据类型与 API 签名（共 743 个打分 API）及人工策划的形式化规范（共 2705 条）。
- 设两种任务模式：proof-only（对给定参考实现证明全部规约）与 code-and-proof（先实现每个 API，再对自己的代码证明全部规约）；两者均要求全覆盖，任何未证明的规约都可能放过它本应捕获的漏洞。
- 内置形式化审计机制：agent 可提交机器检查的证明，指出某规约不可满足或参考实现本身有错；该机制在数据策划阶段已发现潜在错误。
- 能力差距定位：最强 agent 能通过 87% 的单条规约，但留下 16 个仓库未完成——剩余规约编码了跨模块不变式，需要可复用的引理库，而 agent 很少主动构建；在 82 次完整求解中约 74% 的证明行依赖辅助引理。
为什么重要
团队指出，现有基准要么只针对单函数，要么只在固定实现上评测证明生成，而真正的验证软件（OS 内核、密码协议、分布式系统）以多模块仓库形态存在，代码、规约、证明相互交织。Vero 为研究者提供了衡量「完全验证的 AI 生成软件」进展的标尺，并明确指出可复用引理库构建是下一步的关键瓶颈。
2026-08-23 ~ 2026-08-23 · 8 条相关
一手来源
- 首个代码库级形式化验证基准 Vero 发布 — dawnsongtweets ·
- GPT-5.5 仅完全验证 27/43 仓库，10 仓库所有配置全军覆没 — dawnsongtweets ·
- Vero 揭差距：agent 不建可复用引理库，74% 证明行靠辅助引理 — dawnsongtweets ·
- 【源头】首个代码库级形式化验证基准 Vero 发布 — dawnsongtweets · 2026-08-23
- 为何需要仓库级验证：单函数 benchmark 无法覆盖真实软件 — dawnsongtweets · 2026-08-23
- Vero 构成：43 个 Lean 4 仓库、743 个 API、2705 条规约 — dawnsongtweets · 2026-08-23
- Vero 两种任务模式：proof-only 与 code-and-proof 全覆盖要求 — dawnsongtweets · 2026-08-23
- 【源头】GPT-5.5 仅完全验证 27/43 仓库，10 仓库所有配置全军覆没 — dawnsongtweets · 2026-08-23
- 【源头】Vero 揭差距：agent 不建可复用引理库，74% 证明行靠辅助引理 — dawnsongtweets · 2026-08-23
- Dawn Song 团队推 Vero 基准，测评 AI 生成正式验证代码库能力 — dawnsongtweets · 2026-08-23
- Vero 附形式化审计机制：可机器检查规约不可满足性 — dawnsongtweets · 2026-08-23