通过守卫检查器的 fixpoint 绕过，借助罗素悖论无公理地证明 0 = 1。
由 Claude Opus 4.6（Anthropic）自主发现。
| 字段 | 值 |
|---|---|
| 缺陷报告 | rocq-prover/rocq#21683 |
| 修复 | PR #21684 |
| 受影响 | Rocq ≤ 9.1.0 / 所有带守卫检查器的 Coq 版本 |
| 修复于 | 9.2.0 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 |
| CWE | CWE-670（始终错误的控制流实现） |
| CVE | CVE-2026-72705 |
守卫检查器接受这样的 fixpoint：它们将自身作为高阶参数传递给另一个 fixpoint，而后者随后在结构参数的非子项上调用它们。将递归函数传递给 Definition（非 fixpoint 常量）会被正确拒绝——守卫检查器会展开它并看到有问题的调用。但将其传递给 Fixpoint 则会被错误地接受。
这就在 4 行代码中制造了一个罗素式悖论：
Definition delta (x : russell 1) : False := x x.
Definition omega : False := delta delta.
其中 russell 1 在定义上等于 russell 1 -> False——一个类型是其自身的否定。自应用直接得到 False。
该漏洞利用：
Print Assumptions 报告 “Closed under the global context”False 的整个证明仅需 4 行函数式代码Qed——纯定义式docker build -t rocq-cve-poc-21683 .
docker run --rm rocq-cve-poc-21683
任何信任 Rocq 内核检查证明的系统都会受到影响：
iterate_to_neg f n seed :=
match n with
| 0 => f seed -> False (* negate after n steps *)
| S m => iterate_to_neg f m seed
end
russell n :=
match n with
| 0 => True
| S m => iterate_to_neg russell 1 (S m) (* passes ITSELF *)
end
守卫检查器应当拒绝 russell，因为它将自身作为高阶参数传递给 iterate_to_neg，而后者随后会在 S m（不是 n 的子项）上调用它。但该检查器只跟踪直接递归调用，而不跟踪通过高阶不动点参数进行的调用。
russell 1 = iterate_to_neg russell 1 1
= iterate_to_neg russell 0 1
= russell 1 -> False
因此 russell 1 ≡ russell 1 -> False。这就是经典的罗素集：所有不包含自身的集合所构成的集合。自应用得到：
delta : russell 1 -> False (* russell 1 = russell 1 -> False *)
delta x := x x (* x : russell 1 = russell 1 -> False *)
omega : False
omega := delta delta (* delta : russell 1 -> False = russell 1 *)
该漏洞是由 Claude Opus 4.6 在一次夜间模糊测试运行中自主发现的，该测试由 Tristan Stérin（@tcosmo）搭建，基于 Yannick Forster（@yforster）关于守卫检查器的提示。该 AI 识别出了高阶不动点绕过模式，并构造了最小的 iterate_to_neg/russell 漏洞利用。
参见：Zulip 讨论串