CVE-2026-72714Medium· 6.3▾ TwilightPoC availableRocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, a…
▾ Twilight zone — High severity, or a signal on a lesser flaw
impact 34.7 · likelihood 0 · exploitation 12
A public proof-of-concept already exists for this vulnerability — see Exploit availability below.
Public exploit / PoC code seen in 1 source. Availability, not in-the-wild use.
Stakeholder-Specific Vulnerability Categorization from CISA's ADP record at CVE.org: whether exploitation is observed, whether an attack can be automated, and how much of the system is at stake.
Exploit-prediction probability, daily snapshots since Sep 8.
Disclosure to exploitation, from the record and what we observed since indexing it.
Disclosed via NVD
0.1%
1 GitHub repo
0.1% → 0.2%
Last analysed / modified upstream
Rocq Prover does not restore the universe graph's copy of the universe checking flag when a module that locally disabled the check is closed. Local Unset Universe Checking inside a module is expected to last only until the module ends, and the global flag is restored, but the universe graph keeps its own copy which is left disabled. The two views then disagree: Test Universe Checking reports the check as enabled while the kernel continues to accept universe-inconsistent terms. With the constraint between two universes no longer enforced, Hurkens' paradox applies and yields a proof of False, from which any proposition follows. The proof uses no axioms, plugins or unsafe features once the module has closed, and Print Assumptions reports it as closed under the global context, so neither the assumption audit nor the flag query reflects the actual kernel state. No fix is available.
Refer to the linked advisories for vendor-supplied fixes and affected version ranges.
Field changes observed since this record was first indexed.
Connected by shared product, vendor, weakness, or advisory.
CVE-2020-37268Medium· 6.3Print Assumptions does not report that a definition was produced while universe checking was disabled when that definition reaches the caller through Parameter Inline in a module type
CVE-2026-72703Medium· 6.3The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint
CVE-2026-72704Medium· 6.3The guard checker in Rocq Prover does not recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport
CVE-2026-72705Medium· 6.3The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments
CVE-2026-113658High· 7.5ApostropheCMS: Unauthenticated CSV import requests leave rejected uploads in the system temporary directory
CVE-2023-35945High· 7.5Envoy is a cloud-native high-performance edge/middle/service proxy