CVE-2026-72705: Rocq guard checker accepts fixpoint passed as higher-order argument (0 = 1 demonstrated)

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. The guard checker does not track recursive calls made through a fixpoint's own arguments.

Published 26-Oct-2026 00:59 UTC · First seen 26-Oct-2026 00:58 UTC

Sources

• Open Source Security · 26-Oct-2026