验证器说 pass，这个 pass 到底是什么形状？99.1% 的验证器接受率和 1.9% 的规范绑定率来自同一个流水线，中间隔着三层审计。这篇我们直接把这三层搭成一个最小可运行的程序，跑完你就知道，那些报告里最亮眼的数字，只报了第一层。
事情起因是一篇刚上 arXiv 的论文（arXiv:2611.05590）。它在 HumanEval 上复现了以 Dafny 为中间表示的流水线：Claude Opus 4.7 生成代码，用 Dafny 做形式化验证。验证器接受率 99.1%。追问一句：那些“通过验证”的样本里，有多少真的把生成的证明义务绑到了规范定义的谓词或函数上？只有 1.9%。
这两个数不是同一个维度的波动。验证器接受是一台机器在判断逻辑蕴含，而绑定到规范是另一层的事——你的 ensures 到底引用没引用规范里那个谓词。
验证器在“接受”什么？
先看验证器的内部动作。Dafny 验证一个带 ensures 的方法时，把后置条件翻译成一个 SMT 查询，问的是：给定前置条件，执行完函数体之后，后置条件是否必然成立。成立就接受，不成立就拒绝。这个机制不判断语义，只判断逻辑蕴含。
所以后置条件可以窄到什么都不承诺：
function Add(x: int, y: int): int
ensures true
{
x + y
}
验证器对这一个字都不会多说。ensures true 恒真，任何函数体都能让它成立，你写不写函数体没有区别。恒真命题不是错的，但它什么都没承诺。
接受率度量的就是这个 pass 字符流，而 pass 可以是对着一句 true 说出来的。99.1% 不稀奇——每一道题都能用恒真后置条件糊过去。真正稀奇的是那 1.9%，那些样本真的写了跟需求同源的谓词。
“绑定”不是“出现”
我一开始以为，绑定到规范嘛，生成几行 ensures 不就行了吗，怎么只有这么点。后来翻论文的审计定义才明白：证书不是指代码里随便出现了谓词，而是证明义务真的引用了规范里定义的谓词或函数，而不是引用了 true，也不是引用了实现里随手写的局部断言。
模型在采样高概率 token，它倾向于输出一个看起来像正确的后置条件，而不是真的去捕获需求。它写出来的经常是：
ensures x > 0
这类过程性断言在你眼里像是有逻辑约束，但它没有指向任何规范谓词。验证器不管这个——它只负责检查 x > 0 是不是由函数体推出来。你有没有定义 IsPositive(x)、有没有让 ensures IsPositive(x) 去引用它、有没有在规范里赋予它应有的含义，全都不在验证器的职责之内。
到这一步，审计分层可以写成代码了：
class VerificationSample:
def __init__(self, exit_code, ensures_refs_pred, pred_captures):
self.exit_code = exit_code # 第一层：验证器是否接受
self.ensures_refs_pred = ensures_refs_pred # 第二层：ensures 是否引用规范谓词
self.pred_captures = pred_captures # 第三层：谓词是否真的捕捉需求
def audit(sample):
# 三次检查，不是一次检查的三个说法
return (sample.exit_code == 0,
sample.ensures_refs_pred,
sample.pred_captures)
跑一次追踪：
s1 = VerificationSample(0, False, False) # 第一层过，后两层没戏
s2 = VerificationSample(0, True, False) # 前两层过，第三层漏了
s3 = VerificationSample(0, True, True) # 端到端能跑的真样本，只有这种才算数
s1 就是那 99.1% 的形状——验证器点头了，但 ensures true 没指向任何规范谓词，更别说这个谓词能不能捕捉真实需求。s2 前两层干净，但它绑定上去的谓词是偏的，还是会被隐藏测试打死。s3 才是那 535/6870。
把第二层焊死会怎样
你自然会问：那是不是补上第二层绑定检查，数字就实在了？论文第二项实验干的就是这件事。他们用 VCG——团队自己那套 Dafny 中间表示流水线，在 Rust 上强制每个组件都带 Dafny 证书，按构造通过 ensures 绑定检查。相当于把 Surface B 焊死，不绑定的样本根本漏不过去。
结果呢？隐藏测试没给面子。MBPP-Rust 有 11.48% 的结构化验证样本没过隐藏测试，VeriContest 的 LC 切片上失败率 14.82%。这批样本前两层审计都是干净的——验证器说 pass，证明义务也绑上了规范谓词。但它们还是挂了，而且挂得很有代表性。
死在第三层。规范谓词本身没有捕捉到非形式需求。你用 Sorted(a) 当规范，代码证明自己排好序了，隐藏测试要的是稳定排序。验证器再严肃也只证明“你写了什么”，证明不了“用户想要什么”。第二层能把 ensures true 挡住，但挡不住 ensures Sorted(a) 里那个 Sorted 的定义跟真实需求脱节。
99.1% 到 7.79% 之间
这篇论文里真正该看的，不是它跟外部结果的对比——GPT-5.5 的 5.51%、单次 Opus 4.7 的 1.88%。最扎眼的两个数都在它自己身上：99.1% 和 7.79%。后者是 VeriContest LC 切片上的端到端真实解决率，对应 535/6870 个样本，前者是第一层通过率。
同一个流水线，一个数字看着像成了，另一个数字告诉你离能接手真实任务还远着。差的不在实现质量，在审计层数。99.1% 走到第一层就停了，7.79% 是走完三层之后剩下的现实。
作者说跟外部结果的差异只有 2.3 个百分点、4.14 倍，也不敢据此声称性能匹配——任务预算、修复流程、测试框架都不一样。但克制背后藏着一个最要紧的观察：所有端到端数字都低得可怜，所有验证通过率数字都高得离谱。中间的裂缝就是第二层到第三层那段——你绑定了规范，但规范没抓住需求；你证明了谓词，但谓词本身是错的。
这跟模型能力没有直接关系，是结构性的。自回归模型在采样，不在推理。它写 ensures 的时候是补全一串最像规范文本的东西，不是在句法上把非形式需求翻译成形式规范。补全出来的东西恰好撞上绑定条件的概率已经很低，撞上之后还能恰好捕捉真实需求的概率更低。两层概率乘起来，才是你真正能跑端到端测试的那一小撮样本。
下回看见哪个模型报告说“验证通过率 99%”，先别激动，问一句：它绑定规范了吗？绑定上去的那个规范，跟人说的需求是一条路吗？这俩答不上来，那个 99% 跟你没关系——它只是对着 true 说了句“接受”。
想再深一层，自己去翻 Dafny 的 verification engine 如何把 ensures 编码成 SMT 查询。等你看清后置条件在求解器里被展开成什么形状，对“接受”这个词的信任会再降一档。