Threat Intelligence Database

CVE-2026-72714 is a vulnerability in rocq-prover where the universe graph's copy of the universe checking flag is not restored after a module that disables the check locally is closed. This causes a discrepancy between the test universe checking and the kernel state, allowing the kernel to accept universe-inconsistent terms. This flaw enables a proof of False without using axioms or unsafe features, potentially allowing any proposition to be proven. No fix is currently available.

CVE-2026-72705 is a vulnerability in Rocq Prover's guard checker that incorrectly handles recursive calls made through a fixpoint's own arguments. This flaw allows a fixpoint to pass itself as a higher-order argument to another fixpoint, enabling a type to be definitionally equal to its own negation. This leads to self-application producing False in purely definitional code without requiring tactics, axioms, plugins, or unsafe flags. The issue is fixed in Rocq version 9.2.0.

CVE-2026-72704 is a medium severity vulnerability in rocq-prover's rocq component affecting versions up to and including 9.2.0. The flaw involves the guard checker failing to revalidate the recursive tree representation of an inductive type parameter after it is modified by transport. This allows non-terminating definitions to be accepted as terminating, leading to logical contradictions within the system. A fix has been proposed but not yet merged, and no official patch is currently available.

CVE-2026-72703 is a vulnerability in Rocq Prover's guard checker that incorrectly treats parameters of nested mutual fixpoints as uniform without properly analyzing cross-calls. This flaw allows non-terminating definitions to be accepted as structurally decreasing, enabling the construction of a proof of False without requiring axioms or unsafe flags. The issue was introduced in Coq 8.20 and fixed in Rocq 9.2.0. It has a medium severity with a CVSS score of 6.8.