Goal Reached Thanks to every supporter — we hit 100%!

Goal: 1000 CNY · Raised: 1336 CNY

100%
Buy Us a Coffee

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

Quick assessment

Affected
rocq-prover rocq
Exploitation
No confirmed in-the-wild exploitation; assess based on exposure
Recommended action
Check the vendor advisory and references for a fixed version. If immediate upgrade is impossible, restrict exposure and increase monitoring.

在 Coq 定理证明器中，当关闭一个局部禁用宇宙检查的模块时，宇宙检查标志在宇宙图的副本中未能被正确恢复。理论上，模块内部通过 禁用的宇宙检查行为应仅在该模块作用域内有效，并在模块结束时恢复全局标志；然而，宇宙图（universe graph）维护着自己的宇宙检查标志副本，该副本在模块关闭后仍保持禁用状态。 由此导致两种视图出现不一致： 显示宇宙检查处于启用状态，但内核（kernel）实际上仍接受违背宇宙一致性的项（terms）。由于两个宇宙之间的约束不再被强制执行，Hurkens 悖论可被触发，从而构造出对逻辑假

CVSS 6.3 · Medium EPSS 0.12% · P2

Possible ATT&CK Techniques 1 AI

T1195 · Supply Chain Compromise

Affected Version Matrix 1

VendorProduct Version RangeStatus
rocq-prover rocq ≤ 9.2.0 affected
Get alerts for future matching vulnerabilities Log in to subscribe

I. Basic Information for CVE-2026-72714

Vulnerability Information
Have questions about the vulnerability? See if Shenlong's analysis helps!
View Shenlong Deep Dive ↗

Although we use advanced large model technology, its output may still contain inaccurate or outdated information.Shenlong tries to ensure data accuracy, but please verify and judge based on the actual situation.

Vulnerability Title
Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
Source: CVE Program / CVE List V5
Vulnerability 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.
Source: CVE Program / CVE List V5
CVSS Information
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
Source: CVE Program / CVE List V5
Vulnerability Type
清理环节不完整
Source: CVE Program / CVE List V5

Affected Products

Vendor Product Affected Versions CPE Subscribe
rocq-prover rocq 0 ~ 9.2.0 -

II. Public POCs for CVE-2026-72714

# POC Description Source Link Shenlong Link
AI-Generated POC Premium

No public POC found.

Login to generate AI POC

III. Intelligence Information for CVE-2026-72714

请登录查看更多情报信息。

Vendor Advisories for CVE-2026-72714 (1)

Proof of Concept for CVE-2026-72714 (1)

Other References for CVE-2026-72714 (2)

Same Patch Batch · rocq-prover · 2026-08-24 · 5 CVEs total

CVE-2026-72705 6.3 MEDIUM Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
CVE-2026-72703 6.3 MEDIUM Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked
CVE-2026-72704 6.3 MEDIUM Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
CVE-2020-37268 6.3 MEDIUM Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Param

IV. Related Vulnerabilities

Same product: rocq
Same vendor: rocq-prover
Same weakness: CWE-459

V. Comments for CVE-2026-72714

No comments yet

Leave a comment