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.

Attack Vector Local

Attack Complexity Low

Privileges Required None

Attack Requirements None

User Interaction Passive

Vulnerable System Confidentiality Impact None

Vulnerable System Integrity Impact High

Vulnerable System Availability Impact None

Subsequent System Confidentiality Impact None

Subsequent System Integrity Impact None

Subsequent System Availability Impact None

Attack Vector Local

Attack Complexity Low

Privileges Required None

Scope Changed

Confidentiality Impact None

Integrity Impact High

Availability Impact None

User Interaction Required

No CVSS v3.0

No CVSS v2

This CVE is not in the KEV list.

The EPSS score is 0.0012.

Exploitation poc

Automatable no

Technical Impact partial

Default status is the baseline for the product, each version can override it (e.g. patched versions marked unaffected).

Vendor Product Default status Versions
rocq-prover rocq unaffected
Version Status Constraints
0 affected ≤ 9.2.0

No data.

No data.

OpenCVE Enrichment is a feature of OpenCVE that uses AI to automatically link vendors and products to CVEs. Learn more on GitHub.

No data.

Project Subscriptions

No data.

Advisories

No advisories yet.

Fixes

Solution

No solution given by the vendor.

Workaround

No workaround given by the vendor.

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

Tue, 25 Aug 2026 18:30:00 +0000

Type Values Removed Values Added
Metrics ssvc

{'options': {'Automatable': 'no', 'Exploitation': 'poc', 'Technical Impact': 'partial'}, 'version': '2.0.3'}

Mon, 24 Aug 2026 20:15:00 +0000

Type Values Removed Values Added
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.
Title Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
Weaknesses CWE-459
References
Metrics cvssV3_1

{'score': 6.3, 'vector': 'CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N'}

cvssV4_0

{'score': 6.8, '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'}

Projects

Sign in to view the affected projects.

cve-icon MITRE

Status: PUBLISHED

Assigner: VulnCheck

Published:

Updated: 2026-08-25T17:41:24.594Z

Reserved: 2026-08-10T13:02:52.001Z

Link: CVE-2026-72714

cve-icon Vulnrichment

Updated: 2026-08-25T17:41:00.810Z

cve-icon NVD

Status : Received

Published: 2026-08-24T20:17:18.810

Modified: 2026-08-25T18:18:02.633

Link: CVE-2026-72714

cve-icon Redhat

No data.

cve-icon OpenCVE Enrichment

Updated: 2026-08-24T22:45:03Z

Weaknesses