Rocq-Prover Rocq up to 9.2.0 Universe Graph state issue

Summaryinfo

A vulnerability was found in Rocq-Prover Rocq up to 9.2.0. It has been rated as problematic. This impacts an unknown function of the component Universe Graph. Performing a manipulation results in state issue. This vulnerability is identified as CVE-2026-72714. The attack is only possible with local access. There is not any exploit available.

Detailsinfo

A vulnerability classified as problematic has been found in Rocq-Prover Rocq up to 9.2.0. This affects an unknown function of the component Universe Graph. The manipulation with an unknown input leads to a state issue vulnerability. CWE is classifying the issue as CWE-371. This is going to have an impact on integrity. The summary by CVE is:

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.

The advisory is shared at github.com. This vulnerability is uniquely identified as CVE-2026-72714 since 08/10/2026. The exploitability is told to be easy. An attack has to be approached locally. It demands that the victim is doing some kind of user interaction. Neither technical details nor an exploit are publicly available.

There is no information about possible countermeasures known. It may be suggested to replace the affected object with an alternative product.

If you want to get the best quality for vulnerability data then you always have to consider VulDB.

Productinfo

Vendor

• Rocq-Prover

Name

• Rocq

Version

• 9.0
• 9.1
• 9.2.0

CPE 2.3info

• 🔒
• 🔒
• 🔒

CPE 2.2info

• 🔒
• 🔒
• 🔒

CVSSv4info

CVSSv3info

CVSSv2info

Exploitinginfo

Threat Intelligenceinfo

Countermeasuresinfo

Timelineinfo

Sourcesinfo

Entryinfo

If you want to get the best quality for vulnerability data then you always have to consider VulDB.

Discussion