endrazine/rocq-cve-poc-21682CVE-2026-72703 — Rocq Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
Proving 0 = 1 axiom-free via guard checker uniform parameter bypass.
The Rocq kernel's guard checker (fixpoint termination verifier) treats all
parameters of a nested mutual fixpoint as uniform without examining calls
between the fixpoint's bodies. The function find_uniform_parameters in
kernel/inductive.ml only inspects self-recursive calls; when no body calls
itself, every parameter is judged uniform. A parameter that grows through a
cross-call can then keep an incorrect subterm specification, and a recursive
call is accepted even though its argument is not structurally smaller.
This admits a non-terminating definition that proves False, from which any
proposition follows — including 0 = 1.
The proof requires no axioms, tactics, plugins, or unsafe flags. Print Assumptions reports it as closed under the global context.
docker build -t rocq-cve-poc-21682 .
docker run --rm rocq-cve-poc-21682
On a vulnerable version (Rocq 8.20 – <9.2.0), the output confirms the
proof of 0 = 1 with no axioms.
On a patched version (Rocq ≥9.2.0), the guard checker rejects the fixpoint.
Any system that relies on Rocq/Coq kernel-checked proofs may be affected if it runs on a vulnerable version without additional mitigation:
.v file in a dependency could
introduce unsound declarationsfind_uniform_parameters in kernel/inductive.ml only inspects
self-recursive calls within each body of a mutual fixpoint. When no body
contains a self-recursive call (all calls are cross-calls between bodies),
every parameter is marked as uniform. A parameter that actually varies across
cross-calls retains an incorrect subterm specification, allowing the guard
checker to accept a recursive call on a non-structurally-decreasing argument.
| Field | Value |
|---|---|
| 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 — Always-Incorrect Control Flow Implementation |
| Product | Affected | Fixed |
|---|---|---|
| Rocq Prover | 8.20 – <9.2.0 | 9.2.0 |
coqchk on compiled .vo files as a defense-in-depth measure.| Bug report | rocq-prover/rocq#21682 |
| Fix | rocq-prover/rocq#21684 |
| VulnCheck advisory | vulncheck.com |
| Date | Event |
|---|---|
| 2025 | Bug reported (rocq-prover/rocq#21682) |
| 2025 | Fix merged (PR #21684) in Rocq 9.2.0 |
| 2026-08-24 | CVE-2026-72703 published by VulnCheck |
| 2026-08-24 | Docker-reproducible PoC published |