Rocq guard checker misses recursive calls via higher-order arguments (CVE-2026-72705)
Original title: CVE-2026-72705: Rocq guard checker accepts fixpoint passed as higher-order argument (0 = 1 demonstrated)
A checked proof of False, including 0 = 1, needs no axioms, tactics, plugins, or unsafe flags.
Jonathan Brossard reported a soundness bug in the Rocq kernel guard checker, formerly Coq. The checker does not track recursive calls made when a fixpoint passes itself through its own arguments. Print Assumptions reports the resulting proof as closed under the global context. The snippet does not name affected versions or a fix.
Unconfirmed: Affected versions, a fix, and any real-world use are not stated.
- Posted to oss-security on October 25 by Jonathan Brossard.
- The bug yields a checked proof of any proposition, including 0 = 1.
- Print Assumptions treats the proof as closed under the global context.
- No affected release or patched version is stated in the snippet.
Impact: checked proof of any proposition, including False
| Product | Affected |
|---|---|
| Rocq | — |
Vulnerabilities mentioned
All| CVE | Vulnerability | CVSS | EPSS | Signals | Published |
|---|---|---|---|---|---|
| CVE-2026-72705 | The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments | 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.