Reference page — cumulative record through Saturday, October 3, 2026 UTC. Reference pages update as the archive grows; only dated daily editions are immutable pages of record.

CVE-2026-72714

CVE-2026-72714MEDIUM

rocq-prover rocq — Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close

  AV  AC  AT  PR  UI  VC  VI  VA   CVSS    EPSS   %ile   KEV
   L   L   N   N   P   N   H   N    6.8   .0018    6.5     —

AFFECTED
  Product  Versions     Fixed
  rocq     unspecified  —

TIMELINE
  Aug 10  Reserved by VulnCheck
  Aug 24  EXPLOIT PUBLISHED — CVE-2026-72714 (rocq-prover rocq). Public exploit reference added.
  Aug 24  Published (CNA: VulnCheck)
  Aug 25  EXPLOIT PUBLISHED — CVE-2026-72714 (rocq-prover rocq). Public exploit reference added.
  Sep 24  EXPLOIT PUBLISHED — CVE-2026-72714 (rocq-prover rocq). Public exploit reference added.

CWE-459 · CNA: VulnCheck · CVSS v4.0 · 4 references · NVD status: Deferred

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.

Lifecycle

Complete event history — 5 events, chronological
Date	Event	Detail
August 10, 2026	Reserved	Reserved by VulnCheck
August 24, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72714 (rocq-prover rocq). Public exploit reference added.
August 24, 2026	Published	Published (CNA: VulnCheck)
August 25, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72714 (rocq-prover rocq). Public exploit reference added.
September 24, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72714 (rocq-prover rocq). Public exploit reference added.

Affected

Affected products and packages — 1 row
Vendor	Product / Package	Ecosystem	Version introduced	Fixed
rocq-prover	rocq	—	—	—

Weaknesses

CWE-459

References (4)

https://github.com/endrazine/rocq-cve-poc-22287 [exploit]
https://github.com/rocq-prover/rocq [product]
https://github.com/rocq-prover/rocq/issues/22287 [issue-tracking]
https://www.vulncheck.com/advisories/rocq-prover-through-universe-checking-state-desynchronised-after-module-close [third-party-advisory]

Authoritative record: CVE-2026-72714 at cve.org

Vendors: rocq-prover

Weaknesses: CWE-459

About this page

This is a reference page, not a dated page of record. It assembles the complete lifecycle of CVE-2026-72714 from the CVE Program record, NVD enrichment, the CISA KEV catalog, EPSS, and OSV advisories. The box score's numbers (CVSS, EPSS, KEV status) are current as of Saturday, October 3, 2026 UTC and are re-derived as the archive grows; only dated daily editions are immutable pages of record. The authoritative source for this identifier is cve.org.