CVE-2026-72703: Rocq guard checker accepts non-terminating fixpoint via unchecked cross-calls (0 = 1 demonstrated)

// from the source

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 treats all parameters of a nested mutual fixpoint as uniform without examining cross-calls between the...