CVE-2026-72714 (CVSS 6.3)

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.

Is your site exposed to CVE-2026-72714?

Run a free security scan — no signup, results in seconds.

CVSS v3.1 Score

6.3

MEDIUM

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

EPSS — Exploit Prediction

0.0012

Probability of exploitation

0.02%

Percentile rank

EPSS estimates the probability that this vulnerability will be exploited in the wild within the next 30 days. A higher score means more likely to be exploited.

Weakness Type (CWE)

CWE-459 CWE-459

References

Other References

https://github.com/endrazine/rocq-cve-poc-22287 https://github.com/rocq-prover/rocq https://github.com/rocq-prover/rocq/issues/22287 https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close https://github.com/rocq-prover/rocq/issues/22287

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. It has a CVSS v3.1 base score of 6.3 (MEDIUM).

How severe is CVE-2026-72714? +

CVE-2026-72714 has a CVSS v3.1 score of 6.3 out of 10, rated MEDIUM. This is a medium-severity vulnerability that should be remediated as part of regular maintenance. The EPSS score is 0.0012, placing it in the 0th percentile for exploitation probability.

How do I check if I'm vulnerable to CVE-2026-72714? +

You can use Secably's free Website Scanner to check your website for known vulnerabilities. For infrastructure scanning, use the Port Scanner to identify exposed services that may be affected. Check the vendor advisories linked above for specific patch and version information.

Related Vulnerabilities

CVE-2025-6338

There is an incomplete cleanup vulnerability in Qt Network's Schannel support on Windows which can lead to a Denial of …

CVE-2026-0427

Improper cleanup of shared register resources in GPU firmware could allow an admin-privileged attacker from a Guest Virtual machine (VM) …

CVE-2026-77761

A parser state isolation vulnerability in misp-stix could cause data from a previously processed STIX document to be retained and …

CVE-2026-34263 9.6

Due to improper Spring Security configuration, SAP Commerce Cloud allows an unauthenticated user to perform malicious input injection, resulting in …

CVE-2025-21609 9.1

SiYuan is self-hosted, open source personal knowledge management software. SiYuan Note version 3.1.18 has an arbitrary file deletion vulnerability. The …

CVE-2024-28265 9.1

IBOS v4.5.5 has an arbitrary file deletion vulnerability via \system\modules\dashboard\controllers\LoginController.php.

CVE-2026-72714