前几天翻到 8 月 13 号挂上 arXiv 的那篇 Vero，讲的是用 benchmark 评估 agent 在仓库级别同时写实现和写证明的能力。43 个多模块 Lean 4 仓库实例，带预定好的 API 接口、人工整理的 spec 和参考实现，支持 proof-only 和 code-and-proof 两种模式。整篇论文里我最想记下来的是一个小东西：它的 audit 机制——允许 agent 形式化地证明“你给的 spec 不可满足”或者“你的参考实现是错的”，证明通过了算通过，不算失败。
为什么这个东西值得单独记一笔，是因为它对应一个我实际遇到过的尴尬局面。之前让 agent 对着一个 spec 写实现加证明，它跑了几轮之后开始原地打转，我当时的第一反应是 prompt 不够好，拆开看看才发现是 spec 本身自相矛盾——两个约束放在一起，任何实现都满足不了。可是在大多数评测设定里，agent 没有渠道把这个发现表达出来，它只能一直失败，评测方只能一直记零分。错误被记成了能力不足。
Vero 的做法是给 agent 一个正式的出口。用玩具例子演示一下这个机制在验证什么。假设一个模块的 spec 长这样（示意，不是 Vero 里的原题）：
-- spec: 查找函数必须满足的两条性质
theorem find_returns_match (h : ∃ i, i < a.length ∧ a[i] = x) :
find a x < a.length ∧ a[find a x] = x
theorem find_returns_none_iff (h : ¬ ∃ i, i < a.length ∧ a[i] = x) :
find a x = a.length
这两条单看都合理。但如果接口里另外规定了这个函数只允许返回 Nat 且调用方约定返回值必须落在数组下标范围内，第二条就让整个 spec 变成不可满足的——没有任何 find 能同时满足全部约束。传统评测里 agent 只能硬写，写不出来就是零分；audit 模式下它可以交一份这样的东西：
theorem spec_unsat : ∀ f : Array Nat → Nat → Nat,
¬ (satisfies_match f ∧ satisfies_none_iff f ∧ satisfies_range f) := by
intro f ⟨h1, h2, h3⟩
-- 从三条约束推出 False
exact absurd (h1 ...) (by simp [h3])
Lean 的 kernel 检查这份证明，通过就说明题目本身有问题。注意这里的关键：这不是 agent 嘴上说“我觉得 spec 有问题”——那种抱怨没法采信——而是一份被形式化验证过的指控，机器说了算。这跟我之前记的另一篇笔记里“生成和执行分开、中间留人工介入窗口”是同一个思路：把争议交给可验证的凭证，不交给对话。
顺手记一下评测结果，因为它反过来印证了 audit 为什么必要。给了 Lean 工具链的前沿 agent 里，最强的那个在 43 个实例里完整解掉 27 个，但在最难的几个仓库上没有关掉任何一条 spec——密码协议、分布式系统这些领域。也就是说有相当一部分实例是 agent 完全啃不动的，那么这里面有多少是能力问题、有多少是 spec 或参考实现本身的问题，没有 audit 机制就分不开。作者说 benchmark、curation pipeline 和 evaluation harness 都会放出来，我打算等能跑的时候亲手验证一遍 audit 这条路，光看论文里的描述我没法确认它的判定边界在哪。
这里也有我没完全搞懂的地方：agent 提交的“参考实现有错”的证明，具体要证明到什么程度才算数，论文里的表述我读得半懂，得看到 harness 里的实际判定代码才能确认。这条先留一个坑。
划重点：第一，audit 机制的本质是给被评测方一个形式化验证过的申诉渠道，把“题目错了”和“我不会”区分开；第二，这个思路完全可以搬到自己的工作流里——让 agent 对着 spec 卡死的时候，先问一句“这个 spec 是不是本身不可满足，给我证明”，比反复改 prompt 便宜；第三，Vero 那些没被关掉的最难实例，正是最需要这种区分的地方。你可以拿手头任何一个“agent 一直失败”的任务试一遍这个问法，说不定会发现题目本身有问题。