Strix
65K

CVE-2026-72714

MEDIUMCVSS 6.3/10EPSS 0.12%

Last modified

CVE-2026-72714 is a medium-severity vulnerability rated 6.3/10 on the CVSS scale. 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. EPSS estimates a 0.12% chance of exploitation in the next 30 days.

Description

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.

Metrics

CVSS 3.1
6.3/10

CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N

CVSS 4.0
6.8/10

CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N/E:X/CR:X/IR:X/AR:X/MAV:X/MAC:X/MAT:X/MPR:X/MUI:X/MVC:X/MVI:X/MVA:X/MSC:X/MSI:X/MSA:X/S:X/AU:X/R:X/V:X/RE:X/U:X

EPSS Probability
0.12%

2.1th percentile

Probability of exploitation in the next 30 days. Learn more

Weakness Enumeration

Affected Software

Source: CNA advisory (CVE.org). NVD analysis pending.

VendorProductVersions
rocq-proverrocq<= 9.2.0

References

Timeline

Published
Last Modified
Status
Deferred

Frequently Asked Questions

What is CVE-2026-72714?
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.
How severe is CVE-2026-72714?
CVE-2026-72714 has a CVSS score of 6.3/10 (MEDIUM severity). The EPSS model estimates a 0.12% probability of exploitation in the next 30 days.
How do I fix CVE-2026-72714?
Check the vendor references and advisories linked above for patched versions and mitigation guidance. You can also run a Strix scan to test if your systems are affected.

How Strix Helps

Related CVEs from 2026

View all 2026CVEs →

Are you affected by CVE-2026-72714?

Run a free Strix scan to check your systems for this vulnerability.

Scan your code now

Source: NVD / NIST