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.
Published: 2026-08-24
Score: 6.8 Medium
EPSS: < 1% Very Low
KEV: No
Impact: Unrestricted logical deduction leading to arbitrary proof production
Action: Immediate Patch
AI Analysis

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.

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

Remediation

No vendor fix or workaround currently provided.

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

Sign in to view the affected projects.

Advisories

No advisories yet.

History

Fri, 28 Aug 2026 21:00:00 +0000

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

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

Subscriptions

Rocq-prover Rocq
cve-icon MITRE

Status: PUBLISHED

Assigner: VulnCheck

Published:

Updated: 2026-08-29T11:47:43.005Z

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 : Deferred

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

Modified: 2026-09-08T20:23:49.880

Link: CVE-2026-72703

cve-icon Redhat

No data.

cve-icon OpenCVE Enrichment

Updated: 2026-08-28T20:38:48Z

Weaknesses
  • CWE-670

    Always-Incorrect Control Flow Implementation