Description
The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0.
Published: 2026-08-24
Score: 6.8 Medium
EPSS: < 1% Very Low
KEV: No
Impact: Unsound Proofs
Action: Patch
AI Analysis

Impact

The guard checker omitted tracking recursive calls that flow through fixpoint arguments, allowing a self-referential type that is definitionally identical to its own negation. The exploit can produce a proof of False without requiring tactics or unsafe flags. This results in the prover accepting unsound proofs, compromising the integrity of verified code and undermining trust in formally proven properties.

Affected Systems

The vulnerability is present in the Rocq Prover before version 9.2.0. Developers and users employing older Rocq releases in any downstream projects that depend on the guard checker are affected. The issue is specific to the Rocq repository under the vendor "rocq", impacting all builds using the affected compiler.

Risk and Exploitability

The CVSS score of 6.8 rates the issue as moderate severity. EPSS data is unavailable, so the likelihood of exploitation is unclear, but the flaw exists in the core compiler logic and could be exercised by any code written in the prover's language. The vulnerability is not listed in CISA's KEV catalog, indicating no public exploitation reports have yet surfaced. Until the official patch in Rocq 9.2.0 is applied, the risk remains that an attacker can craft unsound proofs that circumvent program verification.

Generated by OpenCVE AI on August 24, 2026 at 22:31 UTC.

Remediation

No vendor fix or workaround currently provided.

OpenCVE Recommended Actions

  • Upgrade Rocq to version 9.2.0 or later
  • Recompile all dependent libraries and codebases that rely on the guard checker with the patched compiler
  • Audit existing proofs for unsoundness and regenerate any that rely on risky definitions

Generated by OpenCVE AI on August 24, 2026 at 22:31 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

Fri, 28 Aug 2026 19: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 does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0.
Title Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
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:44.348Z

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

Link: CVE-2026-72705

cve-icon Vulnrichment

Updated: 2026-08-26T15:46:55.891Z

cve-icon NVD

Status : Deferred

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

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

Link: CVE-2026-72705

cve-icon Redhat

No data.

cve-icon OpenCVE Enrichment

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

Weaknesses
  • CWE-670

    Always-Incorrect Control Flow Implementation