证明通过仍会出错：用编译器检查契约漏洞

AI 写出的程序通过了形式化验证，就能放心合并吗？作者此前让小模型生成 Dafny 程序，发现 8 份契约中有 5 份只限制了长度、格式或形状，其中一个方法写错了，证明依然通过。问题出在验收条件太宽。

作者为此做了一门小语言 Quod：编译器先检查，同一输入能否得到两个都符合契约的不同结果。能找到，就拒绝程序。这个尝试值得看，但它检查的是规格是否充分，离确认业务需求正确还有距离。

证明通过，为什么还能答错

契约（contract）可以理解为函数的验收条件：前置条件规定什么输入合法，后置条件规定输出必须满足什么。验证器只负责证明代码符合这些条件。

如果代码和契约都由同一个 AI 编写，它可能只写自己容易证明的要求。下面这个 clamp 实现负责把输入限制在区间内，但契约只要求结果落在区间内：

fn clamp(x: int, lo: int, hi: int) -> int
  requires lo <= hi
  ensures lo <= result && result <= hi
{
  if x < lo { lo } else if x > hi { hi } else { x }
}

要看的是 ensures 那一行：它没有规定输入已经在区间内时，结果应该保持不变。

执行 quod check clamp_weak.quod，编译器会给出反例：x = 0, lo = 0, hi = 1, result_a = 1, result_b = 0。对同一输入，正确答案 0 和错误答案 1 都过得了验收。

补齐后的契约需要说明三个分支各自应该返回什么：

  ensures lo <= result && result <= hi
  ensures lo <= x && x <= hi ==> result == x
  ensures x < lo ==> result == lo
  ensures x > hi ==> result == hi

其中后三行才把输入与结果对应起来。作者给出的检查结果是：4 个证明义务通过，1/1 份契约能确定结果，契约风格归为 properties。

证明是否通过，和验收条件是否足够，是两个问题。

编译器怎样识别契约里的空话

Quod 把这件事转成 Z3 的可满足性问题：满足前置条件时，是否存在两个不同结果，同时满足后置条件？找到这样的组合，就说明契约留有歧义。

但拒绝有边界。求解器无法判定时，检查只会警告。因此，标题里的「拒绝」应理解为：能够确认约束不足时拒绝。

作者还堵了两条容易绕过检查的路。

第一条是把函数再实现一遍，塞进契约。这样的规格确实可以唯一确定结果，却可能只是重复同一个错误。作者早期实验中，6 份 AI 契约里有 4 份用了第二套实现。编译器因此区分 properties、model、restated、missing，对单纯复述代码的契约发出警告。这是辅助审阅，不能当作独立正确性证明。

第二条涉及合理的多解。例如二分查找遇到重复元素，多个索引可能都能接受。Quod 允许用 loose (a, b) => ... 声明两个结果必须具有什么共同性质，并展示示例。如果声明对任意两个结果都成立，编译器会指出它没有证明任何东西，也可以直接拒绝。

唯一确定结果也不等于符合需求。作者遇到过 ensures len(result) == 0 配合 return []：结果确定、证明成立，但业务上可能完全错误。

它能接进工程，但实验没有证明更强

Quod 目前面向纯函数，支持契约、引理、循环不变量、终止性证明，以及模块、字符串、i32、i64、structs、enums、match 和 generics。它没有输入输出，也没有 maps、sets；这些在路线图中。输入输出计划通过 capability 显式授权。作者不计划加入 classes。

生成目标是 Python 和 C#。C# 后端使用 C# 7.3，可面向 .NET Framework 4.7.2；int 以 long 承载并在 checked 中计算，溢出会抛异常，i32、i64 则证明取值边界。作者没有测生成代码的速度。

工程入口包括 MCP 服务 quod mcp，以及构建时生成 C# 的 NuGet 包。后者附在 release 中，没有发布到 nuget.org；Z3 随发行包提供。原文没有提供 JavaScript 或 Node 后端。

效果需要分开看：

• 两个模型仅凭语言参考，写出了约 300 行、跨三个模块的计费引擎。24 次运行全部通过验证，并与参考判定程序一致。但规则、参考程序和编译器都由作者一人编写，任务难度缺少独立检验。
• 对能力较强的模型，新增规则没有增加完整契约的数量，作者没有测到收益。
• 与 Dafny 比较时，在四种设置、六个任务、共 72 次留出运行中，作者使用的健全性指标未能区分两者。
• 一个本地 14B 模型在 18 次尝试中没有一次被接受，主要卡在沿用 Dafny 语法。错误提示没有教会它写好契约。

工具自身也有可信度成本。对抗审查曾发现过强的长度公理、遗漏前置条件的循环辅助调用，以及 Z3 中断后对可满足问题错误返回 unsat。最后一类在某组文件中约每 300 次出现一次错误拒绝构建，作者没有找到由此造成的错误证明。

另有 Python 变量遮蔽类、C# 模块 a_b 与 aB 合并成同一类的问题，造成生成代码与证明不一致。作者称这些问题都已修复；针对 0.4.0 默认构建的最后一次审查没有发现同类问题，但不保证没有遗漏。使用 --budget 时，机器速度还可能影响哪些证明义务被截断。

我的判断

我认可把「契约有没有说够」提前到编译阶段。它给审阅者一个具体反例，比泛泛提醒「补全边界条件」更容易处理。

但它适合做审查护栏，现有证据不足以证明它能提升模型能力，或比 Dafny 更健全。强模型没测到收益，弱模型也没有靠提示过关，这些结果不能略过。

它也不能替代需求审查和测试。测试能拿具体业务案例核对输出，属性测试能检验广泛输入下的不变量；Quod 增加的检查是：你写下的条件，是否还容得下另一个答案。三者回答的问题不同。

相关研究也不是空白。Lahiri（2024）用能否拒绝变异输出评价 LLM 生成的 Dafny 后置条件；VeriEquivBench（2025）研究规格与代码的等价性。作者只读过后者的一部分。Quod 的尝试在于把反馈放进编译循环，目前还缺少外部用户和独立任务验证。

能拿来做什么

• 审查 AI 写的纯计算函数时，可以直接追问：同一输入下，能否举出另一个满足现有条件、却不符合需求的输出？区间限制只检查范围，就应该继续追问输入与结果的关系。
• 让 AI 同时写实现和契约时，单独检查契约有没有复制实现，并用明确的业务输入输出核对需求。唯一结果也可能是唯一的错误结果。
• 如果项目能调用 Python 或 C#，可以按作者提供的约 30 分钟路径试一个小函数：检查示例、阅读弱契约错误、生成两种代码，再写自己的函数。作者表示目前几乎只有他自己使用，接入前应检查生成代码，并记录实际卡点。