CVE-2026-72714 — Rocq Universe Checking State Desynchronised After Module Close

Proving 0 = 1 axiom-free via module-scoped universe checking flag desynchronization.

Field	Value
Bug report	rocq-prover/rocq#22287
Fix	None (issue open as of 2026-08-16)
Affected	Rocq ≤ 9.2.0 / Coq 8.x (all versions with Hurkens in stdlib)
CVSS 3.1	AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N — 7.1
CWE	CWE-488 (Exposure of Data Element to Wrong Session), CWE-20 (Improper Input Validation)
CVE	CVE-2026-72714

Vulnerability Summary

The Rocq Prover's module system fails to properly scope the Local Unset Universe Checking flag. When used inside a module, the flag should be restored to its previous state when the module closes. However, the universe graph (ugraph) maintains its own copy of the flag, which gets out of sync with the global state upon module closure.

After the desync:

• Test Universe Checking reports on (the global flag was restored)
• The ugraph still has universe checking off (its copy was not restored)
• The kernel therefore accepts universe-inconsistent terms without error

With universe checking effectively disabled, Hurkens' paradox applies: TypeNeqSmallType.paradox exploits the fact that Type@{u} and Type@{v} with u < v can be confused when universe constraints are not enforced, yielding a direct proof of False.

The exploit:

• Uses no axioms, plugins, or unsafe features
• Print Assumptions reports "Closed under the global context"
• Requires only Stdlib.Logic.Hurkens (part of the standard library)
• Is 6 lines of proof code

Usage

docker build -t rocq-cve-poc-22287 .
docker run --rm rocq-cve-poc-22287

Expected output on a vulnerable Rocq version:

[*] Compiling ZeroEqOne.v ...
Universe Checking is on.
bad is defined
Closed under the global context
zero_eq_one is defined
Closed under the global context

[!] VULNERABILITY CONFIRMED

    zero_eq_one : 0 = 1
    Depends on: no axioms (closed under the global context)

    Bug class:  Universe checking state desync (CWE-488)
    Root cause: ugraph retains stale Local Unset Universe Checking flag
    Bug report: https://github.com/rocq-prover/rocq/issues/22287

Impact

Any system that trusts Rocq's kernel-checked proofs is affected:

• Formally verified software: CompCert (verified C compiler), CertiKOS (verified OS kernel), Iris (concurrent separation logic framework), MathComp — any safety case built on a Rocq proof is invalid if the proof environment had this flag desync.
• Proof-carrying code: a malicious .v file in a dependency can silently introduce unsound declarations that downstream proofs rely on.
• Smart contracts: projects using Rocq for verified smart contract development (e.g., ConCert) could have their security guarantees voided.

Technical Details

Root Cause

The universe graph (ugraph) in the kernel contains its own copy of the Universe Checking flag. When a module uses Local Unset Universe Checking, the flag is modified in both the global state and the ugraph. When the module closes, the global state is restored from the module's saved state, but the ugraph's copy is not synchronized, leaving universe checking effectively disabled.

Attack Flow

┌─────────────────────────────────────────────────────┐
│ 1. Universes u v.  Constraint u < v.                │
│    → Declare universes with strict ordering          │
├─────────────────────────────────────────────────────┤
│ 2. Module Off.                                       │
│      Local Unset Universe Checking.                  │
│    End Off.                                          │
│    → ugraph flag stays OFF after module closes        │
├─────────────────────────────────────────────────────┤
│ 3. Test Universe Checking.  → reports "on" (LIE)     │
├─────────────────────────────────────────────────────┤
│ 4. eapply TypeNeqSmallType.paradox; reflexivity.     │
│    → Kernel accepts universe-inconsistent proof       │
│    → False proved with no axioms                     │
├─────────────────────────────────────────────────────┤
│ 5. zero_eq_one : 0 = 1                              │
│    → Derived via exfalso                             │
└─────────────────────────────────────────────────────┘

Comparison with Lean 4 Kernel Bugs

Aspect	Rocq #22287 (this bug)	Lean #14484	Lean #14576
Proof assistant	Rocq (Coq)	Lean 4	Lean 4
Bug class	State desync in module system	Inference cache poisoning	Type confusion via projections
Exploit complexity	6 lines	~20 lines	~50 lines
Universe/type system	Universe checking bypassed	Opaque FVar accepted	Phantom parameters escape
Fix status	Open	Fixed (PR #14498)	Fixed (PR #14577)

Credits

• Bug discovery: Gaëtan Gilbert (@SkySkimmer)
• PoC packaging: Jonathan Brossard (@endrazine)