CVE-2026-72714
Received Received - Intake

Universe Checking Bypass in Rocq Prover via Module Closure

Publication date: 2026-08-24

Last updated on: 2026-08-24

Assigner: VulnCheck

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.

CVSS Scores

EPSS Scores

Probability:
Percentile:

Meta Information

Published
2026-08-24
Last Modified
2026-08-24
Generated
2026-08-25
AI Q&A
2026-08-24
EPSS Evaluated
N/A
NVD
CVE-2026-72714
EUVD
EUVD-2026-65143

Affected Vendors & Products

Showing 2 associated CPEs
Vendor Product Version / Range
rocq rocq_prover 9.2.0
coq coq 8.*

Helpful Resources

Exploitability

CWE
CWE Icon
KEV
KEV Icon
CWE ID Description
CWE-459 The product does not properly "clean up" and remove temporary or supporting resources after they have been used.

Attack-Flow Graph

AI Quick Actions

Instant insights powered by AI
Executive Summary

This vulnerability affects the Rocq Prover (formerly Coq), a proof assistant used for formal verification. It occurs when the universe checking flag is locally disabled within a module but not properly restored globally after the module closes. The universe graph retains a stale disabled state, causing a mismatch between the reported and actual kernel state. This allows invalid proofs, including a proof of False via Hurkens' paradox, to pass verification without using unsafe features.

Detection Guidance

This vulnerability is specific to the Rocq Prover (Coq) and cannot be detected via standard network or system commands. It requires checking the version of Rocq Prover installed and verifying if universe checking state desynchronization occurs after module operations. Use commands like 'coqc --version' to check the installed version and review proof scripts for 'Local Unset Universe Checking' usage.

Impact Analysis

This vulnerability allows attackers to prove false statements like 0 = 1 in Rocq Prover versions up to 9.2.0. It undermines the soundness of all formally verified systems built on Rocq, including CompCert, CertiKOS, Iris, MathComp, and proof-carrying code systems. Exploits require only standard library components and minimal code, making it a high-impact threat to systems relying on Rocq for correctness.

Compliance Impact

This vulnerability could compromise compliance with standards requiring formal verification, such as those in critical infrastructure or healthcare systems. Since it allows proving false statements, systems relying on Rocq for correctness may fail to meet regulatory requirements for data integrity, security, or safety. No specific compliance frameworks are mentioned in the provided context.

Mitigation Strategies

No official fix is available for this vulnerability. Immediate steps include avoiding the use of 'Local Unset Universe Checking' in modules, especially when working with universe constraints. Users should review and update proof scripts to prevent reliance on this feature. Monitor the Rocq Prover GitHub repository for updates and potential patches.

Chat Assistant

Ask questions about this CVE
Hi! I’m here to help you understand CVE-2026-72714. Ask me anything about the vulnerability, its impact, or mitigation strategies.
0/70

EPSS Chart