CVE-2026-72703

Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls

Published Aug 24, 2026 CVSS 4.0 · 6.8 Medium EPSS < 1% KEV · Not listed

Description

The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.

Analysis

Technical impact

This flaw in Rocq’s guard checker causes it to incorrectly treat a parameter of a nested mutual fixpoint as uniform when cross‑call interactions are present. As a result, a definition that does not structurally decrease is still accepted, leading to a term whose value equals its own successor. The consequence is a proof of False with no extra axioms or unsafe flags, allowing an attacker to derive any proposition within a Rocq session.

Affected Systems

Rocq Prover developers ship this vulnerability in versions 8.20 through 9.1.x. The fix is released in release 9.2.0. Users running any earlier or 9.x minor releases are susceptible. The product is the open‑source Rocq theorem prover available from the upstream project.

Risk and Exploitability

The CVSS score is 6.8, indicating a medium severity impact. No EPSS data is available, and the vulnerability is not listed in CISA KEV. Attackers can exploit the flaw locally by executing arbitrary Coq code that defines a non‑terminating mutual fixpoint. Once triggered, the guard checker accepts it and a proof of False is produced, effectively undermining soundness and enabling any subsequent logical consequence. The exploit requires no special privileges beyond the ability to run user code in Rocq.

Affected Products

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
`8.20`	affected	< 9.2.0

No data.

Vendor Product Versions

Rocq-prover

Rocq

Version	Status	Scheme	Platform
`[8.20,9.2.0)`	affected	generic	—

Remediation

No solution or workaround provided in the CVE record.

OpenCVE Recommended Actions

Upgrade Rocq Prover to version 9.2.0 or later to apply the guard checker patch.
If an upgrade is infeasible, avoid using nested mutual fixpoints that involve cross‑calls until a patch becomes available; review existing proofs for such patterns.
Use an alternative verification pipeline that does not rely on Rocq’s guard checker or manually validate that all fixpoints terminate by checking structural decrease arguments before acceptance.

Generated by OpenCVE AI on August 24, 2026 at 21:45 UTC.

Tracking

Advisories

No advisories available

Metrics

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.

Exploit prediction score: < 1% (0.176% probability within 30 days)

Exploitation poc

Automatable no

Technical Impact partial

References

Link	Providers
http://www.openwall.com/lists/oss-security/2026/10/26/4
https://github.com/endrazine/rocq-cve-poc-21682
https://github.com/rocq-prover/rocq
https://github.com/rocq-prover/rocq/issues/21682
https://github.com/rocq-prover/rocq/pull/21684
https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls

History

Oct 26, 2026 2:30 AM Added references View changes

Type	Values Removed	Values Added
References		http://www.openwall.com/lists/oss-security/2026/10/26/4

Aug 28, 2026 9:00 PM First appearance in the feed. Affected vendors updated View changes

Type	Values Removed	Values Added
First Time appeared		Rocq-prover Rocq-prover rocq
Vendors & Products		Rocq-prover Rocq-prover rocq

Aug 27, 2026 3:30 PM Scoring metrics updated View changes

Type	Values Removed	Values Added
Metrics		ssvc `{'options': {'Automatable': 'no', 'Exploitation': 'poc', 'Technical Impact': 'partial'}, 'version': '2.0.3'}`

Aug 24, 2026 8:15 PM Description updated. Title updated. Weaknesses updated. Added references. Scoring metrics updated View changes

Type	Values Removed	Values Added
Description		The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
Title		Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
Weaknesses		CWE-670
References		https://github.com/endrazine/rocq-cve-poc-21682 https://github.com/rocq-prover/rocq https://github.com/rocq-prover/rocq/issues/21682 https://github.com/rocq-prover/rocq/pull/21684 https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls
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'}`