伯克利 RDI 实验室放出了一个叫 Vero 的基准。它要求 AI 智能体在整个代码库的尺度上同时干两件事：把每个必需的 API 实现出来，并且证明每条给定的规范成立，同时保证代码、证明和构建三者始终一致。此前的形式化验证基准基本停在单个定理或单个函数上，仓库级别的还是头一个。
题面是 43 个多模块 Lean 4 项目，从 Python、Dafny、Verus 和 Coq 的现有代码移植而来，一共覆盖 743 个 API 和 2705 条形式规范。评测跑两种模式：仅证明模式给出参考实现，智能体只负责证明；代码与证明模式则要求智能体自己写实现，再证明它满足规范。
分数表
90 分钟预算下的完全解决数（满分 43）：
| 配置 | 代码与证明 | 仅证明 |
|---|---|---|
| GPT-5.5（xhigh）+ Codex | 27 | 25 |
| Claude Opus 4.8 + Claude Code | 8 | 10 |
| GPT-5.5（medium）+ Codex | 2 | 6 |
| Claude Sonnet 5 + Claude Code | 2 | 2 |
第一行和第三行之间那道沟需要看清楚：同一个 GPT-5.5、同一个 Codex，仅仅把推理档位从 medium 调到 xhigh，代码与证明模式的成绩从 2 跳到 27。在这类任务上，思考预算的边际收益远远没有饱和。
难的地方不在单条证明
榜首那一行还有另一组数字。GPT-5.5（xhigh）在代码与证明模式下通过了 87.3% 的单条规范，仅证明模式下 85.8%，但落到”整个实例完全做完”这个口径，只剩 27/43 和 25/43。研究者给的判断很直接：证明每一条规范已经不算难点，难的是让整个证明仓库保持一致。
这两个数字的落差是有工程含义的。八成七的单条通过率，换算到一个有几十条规范的项目上，意味着几乎每个项目都会剩下几条卡住。而形式化验证是全有全无的——剩一条没证出来，整个仓库就构建不过，前面证对的那些拿不到任何部分分。这跟单元测试通过 87% 的项目还能上线是完全两回事。
另一处细节是证明代码的构成。在那些完全解决的运行里，辅助定理占了证明代码的中位数 73.6%。也就是说智能体写出来的东西，四分之三是为了支撑主证明而临时搭的脚手架。这个比例暗示当前的模型走的是宽度优先的路子，靠堆引理硬推，而非找到简洁的证明结构。
自己挑算法，五次帮忙十七次坏事
代码与证明模式给了智能体一个自由度：实现可以自己写，那就可以挑一个更好证的算法。研究者统计了这个自由度的净效果，配对比较下来，5 组因为换了算法而做成，17 组反倒因此失败。
这个 5 比 17 挺说明问题。理论上，能自选实现应该只增不减——大不了照抄参考实现。实际结果是模型经常挑了一个自认为聪明、证起来却更麻烦的写法，然后在 90 分钟里陷进去出不来。会写代码和知道哪种代码好证明，是两种能力，眼下的智能体只有前一种。
榜单最后还留了一条：43 个实例里有 10 个，在所有配置、两种模式下都没有任何一次被解决。这批题目构成了当前方法的硬上限，也是下一轮工作最该盯的地方。
对做 AI 编程工具的人来说，Vero 的参考价值不在排名，而在它把”仓库级一致性”这个此前只能靠经验感受的东西拆成了可测的指标。SWE-bench 那类基准测的是能不能改对一个 bug，Vero 测的是能不能扛住一个工程的完整约束，两者难度不在一个量级。
参考来源：伯克利 RDI 实验室公开博客、CocoLoop；基准规模、两种模式的完全解决数、单条规范通过率、辅助定理占比与配对统计均按公开报告口径核对。