通过守卫检查器统一参数绕过，无公理地证明 0 = 1。
Rocq 内核的守卫检查器（不动点终止性验证器）将所有嵌套互递归不动点的参数视为统一的，而不检查不动点各函数体之间的调用。kernel/inductive.ml 中的函数 find_uniform_parameters 仅检查自递归调用；当没有任何函数体调用自身时，每个参数都被判定为统一的。一个通过交叉调用增长的参数因此可以保留错误的子项规范，使得递归调用即使其参数并非结构上更小也会被接受。
这允许一个非终止的定义证明 False，由此可推出任何命题——包括 0 = 1。
该证明不需要公理、策略、插件或不安全标志。Print Assumptions 报告其在全局上下文中是封闭的。
docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682
在存在漏洞的版本（Rocq 8.20 – <9.2.0）上，输出确认了 0 = 1 的无公理证明。
在已修补的版本（Rocq ≥9.2.0）上，守卫检查器会拒绝该不动点。
任何依赖 Rocq/Coq 内核检查证明的系统，如果在没有额外缓解措施的情况下运行存在漏洞的版本，都可能受到影响：
.v 文件可能引入不可靠的声明kernel/inductive.ml 中的 find_uniform_parameters 仅检查互递归不动点每个函数体内的自递归调用。当没有任何函数体包含自递归调用（所有调用都是函数体之间的交叉调用）时，每个参数都被标记为统一的。一个在交叉调用中实际发生变化的参数保留了错误的子项规范，使得守卫检查器接受对非结构递减参数的递归调用。
| 字段 | 值 |
|---|---|
| CVE | CVE-2026-72703 |
| CVSS 3.1 | AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1 (High) |
| CVSS 4.0 | AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N — 6.8 (Medium) |
| CWE | CWE-670 — 始终错误的控制流实现 |
| 产品 | 受影响 | 已修复 |
|---|---|---|
| Rocq Prover | 8.20 – <9.2.0 | 9.2.0 |
.vo 文件运行 coqchk 作为纵深防御措施。| 缺陷报告 | rocq-prover/rocq#21682 |
| 修复 | rocq-prover/rocq#21684 |
| VulnCheck 公告 | vulncheck.com |
| 日期 | 事件 |
|---|---|
| 2025 | 报告缺陷（rocq-prover/rocq#21682） |
| 2025 | 修复合并（PR #21684）至 Rocq 9.2.0 |
| 2026-08-24 | VulnCheck 发布 CVE-2026-72703 |
| 2026-08-24 | 发布可通过 Docker 复现的 PoC |