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.

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.

The EPSS score is 0.0012.

Exploitation poc

Automatable no

Technical Impact partial

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.

No data.

OpenCVE Enrichment is a feature of OpenCVE that uses AI to automatically link vendors and products to CVEs. Learn more on GitHub.

No data.

Project Subscriptions

No data.

Advisories

No advisories yet.

Fixes

Solution

No solution given by the vendor.

Workaround

No workaround given by the vendor.

References
Link Providers
https://github.com/endrazine/rocq-cve-poc-21682 cve-icon cve-icon
https://github.com/rocq-prover/rocq cve-icon cve-icon
https://github.com/rocq-prover/rocq/issues/21682 cve-icon cve-icon
https://github.com/rocq-prover/rocq/pull/21684 cve-icon cve-icon
https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-non-terminating-fixpoint-via-unchecked-cross-calls cve-icon cve-icon
History

Thu, 27 Aug 2026 15:30:00 +0000

Type Values Removed Values Added
Metrics ssvc

{'options': {'Automatable': 'no', 'Exploitation': 'poc', 'Technical Impact': 'partial'}, 'version': '2.0.3'}

Mon, 24 Aug 2026 20:15:00 +0000

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
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'}

Projects

Sign in to view the affected projects.

cve-icon MITRE

Status: PUBLISHED

Assigner: VulnCheck

Published:

Updated: 2026-08-27T14:12:34.453Z

Reserved: 2026-08-10T13:02:20.829Z

Link: CVE-2026-72703

cve-icon Vulnrichment

Updated: 2026-08-27T14:12:30.905Z

cve-icon NVD

Status : Received

Published: 2026-08-24T20:17:18.240

Modified: 2026-08-27T17:19:51.313

Link: CVE-2026-72703

cve-icon Redhat

No data.

cve-icon OpenCVE Enrichment

Updated: 2026-08-24T22:00:04Z

Weaknesses