当 Agent 写完代码还不够，Vero 把验证也变成了仓库级任务

发表于2026-09-02|更新于2026-09-07|视界AI研究

|浏览量:

一个 Agent 跑完 CI，回了一句 all tests pass。你会把它的 PR 直接合进去吗？

大多数工程团队的真实答案是，不会。有人会看 diff，有人会补测试，有人会盯着那几个改动很小却足够把数据删光的 SQL。可一旦 Agent 把改动范围拉到一个多模块仓库，靠人眼补上这层信任会变得很贵。你不是只在验一段代码，你在验它有没有理解整个系统。

Berkeley RDI 9 月发布的 Vero 很有意思。它不再问 Agent 能不能填出某一个 Lean 4 证明，也不满足于某个函数的单元测试。它把问题推到了更不舒服、也更接近工程现场的位置，能不能让 Agent 在一个完整仓库里同时写实现和证明，并且让整个项目从干净环境重新构建通过。

这不是给 Agent 再加一道考试题。

它是在追问，代码生成走到今天，真正稀缺的能力到底是什么。

测试通过，不等于你获得了可以托付的代码

测试的价值当然不需要怀疑。对 Java 和 Spring 服务来说，单测、集成测试、契约测试、压测，已经是非常实用的防线。我们每天都靠它们把回归拦在上线前。

问题是测试只覆盖了你想到要写下来的输入和路径。一个订单状态机可能有一百个合法与非法的状态组合，测试挑十几个典型路径就已经不少了。那条在重试、超时和并发同时发生时才出现的路径，往往不在断言里。

形式化验证的野心更大。它不是拿一批样例去碰碰运气，而是把行为写成 specification，再由一个小型可信内核检查证明。只要前提和模型没有写错，证明的是规范涵盖范围内的所有输入，而不是测试作者挑到的那些例子。

这话听起来很美，但落在仓库里就很别扭。

因为实现、类型、模块依赖、辅助定理、构建脚本，会互相牵连。你改了一个数据结构定义，后面一串 proof obligation 都可能跟着失效。一个函数本身不复杂，真正难的地方可能是你在三小时前写下的那个不变量，已经让后面所有证明走进了死胡同。

我自己也踩过类似的坑。写 Agent 工作流时，最开始总会把失败归因为模型没有把某一步做好。复盘日志后才发现，很多失败不是单点能力差，而是早期约束没有被显式保存，后面每一步都在错误的前提上认真工作。代码仓库里的 proof dependency，和 Agent 的状态、工具输出、任务分解，其实是同一种麻烦。

Vero 测的就是这件事。

Vero 没把仓库问题拆回函数题

Vero 收录了 43 个多模块 Lean 4 实例，横跨智能合约与区块链协议、分布式系统与共识、安全关键基础设施、数据结构、算法和数值工具。数据来源并不全是 Lean 项目，13 个实例来自 Dafny、Verus 或 Coq 的验证项目，另有 30 个从 Python 项目迁移并补齐了形式化规范。

规模也不是摆设。整个套件有 743 个计分 API 和 2705 条形式化规格。

这两个数字放在一起看，才能明白它为什么比一般 benchmark 更像工程。一个 Agent 没法只挑最容易的 theorem 做掉，再拿局部通过率讲故事。Vero 把 full solve 作为主要指标，只有整个仓库的所有义务都关闭、从干净源重新构建也通过，才算完成。

它提供两种模式。

Proof-only 模式给出参考实现，Agent 只需要补完证明。这已经保留了跨模块依赖和仓库级构建的问题。

Code-and-proof 模式则把实现体也藏起来。Agent 要自己决定 API 怎么实现，再证明自己的实现满足每条规格。后者才是 Vero 真正想看的场景，因为实现和证明不是两份独立作业。

一个很直觉的例子是排序。你可以写一个性能很好、但循环不变量很难表达的实现，也可以选一个朴素得多、却天然容易归纳证明的实现。两者都可能满足排序正确性，却会把后续证明的难度拉开一大截。

不是说生产系统都应该换成最容易证明的算法。性能、内存、可维护性、已有行为兼容，都不会因为 proof 成立就消失。Vero 自己也报告，有些 Agent 用更简单的实现换来了可证明性，却牺牲了渐进效率。

但这正是它有价值的地方。它没有把这种 trade-off 藏在榜单背后。

当前最强的 Agent，仍然会在仓库组织上卡住

在每次 90 分钟的预算内，Vero 评估了四种前沿 Agent 配置。公开结果里，GPT-5.5 xhigh 配合 Codex 在 code-and-proof 模式完成了 27 个实例，在 proof-only 模式完成了 25 个。按单条规格统计，覆盖率分别达到 87.3% 和 85.8%。

这个成绩已经很高了。过去我们讨论 AI 编程，大多还停在能否修改文件、能否读懂报错、能否让测试绿起来。现在一个 Agent 已经可以为相当一部分多模块项目搭起实现和证明库，并让它们一起工作。

但别把 87.3% 当成 87.3% 的放心。

在有严格正确性要求的系统里，缺掉的一条规格未必是一个无关紧要的角落。它可能恰好是转账不凭空增发、锁不会永久占住、权限不会绕过的那条边界。因而 Vero 坚持以全仓库完成作为主指标，我觉得很对。局部覆盖率适合诊断，不适合替代交付标准。

更刺眼的数据是，所有配置和两种模式加起来，仍有 10 个实例无人完成。并且很多成功实例只被一种配置拿下。这说明它还不是一个已经稳定商品化的能力，更像是某些路线能幸运走通的前沿探索。

如果你正在给团队采购 Agent，这句话可能有点扫兴，但需要说出来。今天把 Agent 接进 CI，可以明显提速。把它当成能独立承诺关键性质的工程师，还太早。

难点不是证明某一句，而是维护一张会生长的依赖网

Vero 的结果里有一组细节特别值得做 Agent 的人看。

在 82 次全仓库完成的运行中，辅助定理占了 code-and-proof 证明行数的中位数 73.6%，proof-only 中也是 71.6%。80 次运行里，一个 helper theorem 支撑了至少两条规格，65 次里支撑了至少五条。

这就很不像刷题了。

真正完成一个仓库级验证，主角不是最后那句一键自动化 tactic，而是一批被设计、复用和维护的中间结论。它们像 Spring 项目里的领域模型和边界接口。你如果一开始把边界切对，后面的业务实现会自然收敛。切错了，后面每加一个功能都在还债。

研究者还统计了 helper 链深度和通过率。没有 helper 的规格，在 code-and-proof 中通过率是 83.9%，proof-only 中是 80.1%。当依赖链深度达到四层以上，通过率分别掉到 50.6% 和 39.1%。

这几乎是一个很具体的 Agent 架构提示。

现在不少 Coding Agent 的工作方式仍是，看到报错，局部修一下，再跑一遍。这种反应式循环在短任务里很好用。一旦仓库存在长依赖链，它会把错误的早期设计不断固化。Vero 的轨迹分析也观察到，Agent 常常很早就承诺某种实现，即使证明计划反复受阻，也继续堆 proof 直到超时，而不是回头改定义。

这很像一个写错了 LangGraph state schema 的工作流。节点再聪明，也只是在错误的字段和路由上加更多补丁。

所以，面向长任务的 Agent 不该只有 planner 和 executor。它还需要一个能触发重新建模的机制。不是「再试一次」，而是能明确判断，当前不变量、模块接口或实现策略已经让后续搜索空间坏掉了，应该退回哪一层重做。

这听着像项目经理的话，但其实非常工程化。它需要可追溯的决策记录、依赖图、失败分类，以及一个不把历史 token 当成真理的回退策略。

代码可运行和代码可证明，给了 Agent 不同的自由度

Vero 里有个现象很有启发性。研究者找到 5 组实例与 Agent 的配对，分布在 3 个仓库中。Agent 换掉了参考实现里较难验证的算法，改用更简单但仍满足规格的实现。这样一来，code-and-proof 把 250 条规格全部关闭，而固定参考实现的 proof-only 只关闭了 201 条。

这不是 code-and-proof 比 proof-only 多做一步却反而更轻松的悖论。它提示了一件常被忽略的事，代码生成的自由度，有时也是验证的自由度。

传统开发会优先问，这个算法快不快、可读不可读、跟旧系统兼不兼容。形式化开发还多一个问题，这个设计的关键性质能否被模块化地表达和复用。

你如果做 Java 服务，未必会在下个迭代引入 Lean 4。但可以把这种思路迁移回来。比如对幂等、状态迁移、资金守恒、权限边界，先写出可以被测试、监控和审计共同使用的明确不变量。它们不一定是机器证明，却会强迫设计在代码前变得具体。

反正我觉得，很多所谓「Agent 写代码不可靠」，并不是因为模型少会了几门语言。更深的原因是我们把可运行当成了完成，把关键约束留在了人的脑子里。