Rocq guard checker accepts non-terminating cross-calls (CVE-2026-72703)
Original title: CVE-2026-72703: Rocq guard checker accepts non-terminating fixpoint via unchecked cross-calls (0 = 1 demonstrated)
Nested mutual fixpoint parameters are treated as uniform without examining cross-calls between them.
Jonathan Brossard reported a soundness bug in the Rocq kernel guard checker, formerly Coq. All parameters of a nested mutual fixpoint are treated as uniform, and cross-calls between those fixpoints are not examined. The report says this accepts a non-terminating fixpoint and yields a checked proof of False, including 0 = 1, with no axioms, tactics, plugins, or unsafe flags. Print Assumptions reports the proof as closed.
Unconfirmed: The snippet does not state versions, a patch, or attacker exploitation.
- Posted to oss-security on October 25.
- The flaw concerns unchecked cross-calls in a nested mutual fixpoint.
- No axioms, tactics, plugins, or unsafe flags are required.
- Affected and fixed versions are not given in the snippet.
Impact: checked proof of False from a non-terminating fixpoint
| Product | Affected |
|---|---|
| Rocq | — |
Vulnerabilities mentioned
All| CVE | Vulnerability | CVSS | EPSS | Signals | Published |
|---|---|---|---|---|---|
| CVE-2026-72703 | The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint | 6.8 | <1% |
From the original article
Posted by Jonathan Brossard on Oct 25 1. Summary ========== A soundness bug in the Rocq (formerly Coq) kernel's guard checker allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1 — without axioms, tactics, plugins, or unsafe flags. Print Assumptions reports the proof as closed under the global context.
seclists.org
A short excerpt; the article and its images belong to the publisher. Summary, key facts and assessment above are AI-written from the article and can be wrong.