Rocq and Lean 4 kernel bugs let checked proofs of False through

Four disclosures posted the same day on oss-security describe kernel and audit failures in Rocq (formerly Coq) and Lean 4 that allow construction of checked proofs of False, and thus any proposition including 0 = 1, without axioms or unsafe flags. The findings matter because both systems sit at the trust root for formally verified compilers, OS kernels, separation-logic frameworks, math libraries, and proof-carrying dependencies. A bypass at that layer undermines assurance chains that rely on the checker, including workflows tied to Common Criteria or airborne-software standards.

The Lean 4 report, tracked as CVE-2026-72844, is a kernel soundness bug. The kernel failed to ensure that a structure named in a projection matched the value being projected, and nested inductive applications were not fully type-checked when registered. A metaprogram could introduce an ill-typed nested inductive and obtain a proof of False even under maximum kernel checking. Independent recheckers that replay the same kernel rules are equally exposed. Affected builds could treat forged theorems as kernel-valid, including safety claims about compilers, kernels, and crypto code, or unsound declarations slipped in through a dependency.

Two fresh Rocq issues hit the guard checker, the component that enforces termination of recursive definitions. CVE-2026-72703 covers acceptance of a non-terminating mutual fixpoint: the checker treated nested mutual-fixpoint parameters as uniform without examining cross-calls, so a parameter that grew through a cross-call kept a wrong subterm specification and a non-decreasing recursive call was allowed. From that definition, False follows in a closed proof. CVE-2026-72705 is a related guard gap: the checker did not track recursive calls made through a fixpoint’s own arguments, so a fixpoint could pass itself to another fixpoint and be applied to a non-structural value. That admits a type definitionally equal to its own negation; self-application yields False in purely definitional code. One of the Rocq guard findings was surfaced during a fuzzing campaign. Both are described as fixed in Rocq 9.2.0 and later; older lines accepted the demonstrations.

A fourth item, CVE-2020-37268, is older and still open as of Rocq 9.2.0. It is an audit bypass rather than a raw kernel acceptance hole. When a module type uses Parameter Inline and functor application inlines the body, metadata that the original definition ran under unset universe checking is dropped. Print Assumptions then reports the proof as closed with no axioms visible, while the universe graph silently holds inconsistent constraints, enabling a paradox proof of False. The separate coqchk path on compiled objects can still reject the result, but in-process Print Assumptions, the check most projects and CI pipelines actually run, does not. The issue has been on the project’s critical-bugs list since 2020 without a merged fix.

Taken together, the batch is a reminder that proof-assistant kernels and the thin audit tools around them remain high-value targets. Projects that pin Rocq below 9.2.0, run Lean 4 on affected kernels, or treat Print Assumptions as a sole integrity gate should reassess trust in previously accepted developments and dependency graphs until patches and stricter checkers are in place. Jonathan Brossard filed the public reports.