在评估 LLM 生成代码的“验证”意义时，常见的做法是给出一个单一的验证率。我们认为这会把三种本质不同的属性混为一谈，这三种属性在一次条件审计序列中分别对应：
- 表面 A：验证器接受率，即生成的代码能否通过形式化验证器的检查；
- 表面 B：语法规格绑定，指证明义务是否真正绑定到规格定义的谓词或函数上；
- 表面 C：语义规格忠实度，指规格本身是否完整捕获了非形式化的需求。
实验一（A ≠ B）：使用 Li@Opus（在 Claude Opus 4.7 上复现 \citet{li2025dafny} 的 Dafny‑IR 流水线）对三个 Python 基准进行测试。HumanEval 上的验证器接受率达到 99.1%，但仅有 1.9% 的样本能够得到绑定到规格谓词的证书，说明高接受率并不等同于规格绑定。
实验二（B ≠ C）：在 Rust 基准上使用我们内部实现的 VCG（同样基于 Dafny‑IR）进行评估。Rust 目标能够强制每个组件以 Dafny 证书形式输出，保证结构上通过绑定门。即便如此，结构上通过验证的样本中仍有 11.48%（MBPP‑Rust）和 14.82%（VeriContest LC slice）在隐藏测试中失败，表明规格本身未能完整捕获需求。
在 VeriContest 的 LC 切片上，VCG 报告的端到端成功率为 7.79%（535/6870），而外部报告的 GPT‑5.5 为 5.51%，单次 Opus 4.7 为 1.88%。两者之间的差异分别为 2.3 个百分点和 $4.14\times$，但任务预算、修复策略和评测框架的差异阻止了直接的性能对比。
点评：这三层失效面提醒我们，在追求 LLM 生成代码的形式化验证时，不能仅关注验证器的通过率，而必须同步检查规格绑定和规格的语义完整性，否则所谓的“验证”可能只是表面的合规。