U.S. flag   An official website of the United States government
Dot gov

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Https

Secure .gov websites use HTTPS
A lock (Dot gov) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

National Vulnerability Database

National Vulnerability Database

NVD

National Vulnerability Database
  1. Vulnerabilities

CVE-2026-72714 Detail

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

 
NVD enrichment efforts reference publicly available information to associate vector strings. CVSS information contributed by other sources is also displayed.
CVSS 4.0 Severity and Vector Strings:

NIST CVSS score
NIST: NVD
N/A
NVD assessment not yet provided.

Nist CVSS score does not match with CNA score
CNA:  VulnCheck
CVSS-B 6.8 MEDIUM
Vector:  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

References to Advisories, Solutions, and Tools

By selecting these links, you will be leaving NIST webspace. We have provided these links to other web sites because they may have information that would be of interest to you. No inferences should be drawn on account of other sites being referenced, or not, from this page. There may be other web sites that are more appropriate for your purpose. NIST does not necessarily endorse the views expressed, or concur with the facts presented on these sites. Further, NIST does not endorse any commercial products that may be mentioned on these sites. Please address comments about this page to [email protected].

URL Source(s) Tag(s)
https://github.com/endrazine/rocq-cve-poc-22287 VulnCheck
https://github.com/rocq-prover/rocq VulnCheck
https://github.com/rocq-prover/rocq/issues/22287 VulnCheck
https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close VulnCheck

Weakness Enumeration

CWE-ID CWE Name Source
CWE-459 Incomplete Cleanup VulnCheck  

Change History

1 change records found show changes

Quick Info

CVE Dictionary Entry:
CVE-2026-72714
NVD Published Date:
08/24/2026
NVD Last Modified:
08/24/2026
Source:
VulnCheck