CVE-2026-72705

Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument

View on CVE.org
Published Aug 24, 2026 CVSS 4.0 · 6.8 Medium EPSS < 1% KEV · Not listed
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.

Analysis

AI-generated

Technical 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.

Remediation

No solution or workaround provided in the CVE record.

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 available
History
Type Values Removed Values Added
References
Type Values Removed Values Added
First Time appeared Rocq-prover
Rocq-prover rocq
Vendors & Products Rocq-prover
Rocq-prover rocq
Type Values Removed Values Added
Metrics ssvc

{'options': {'Automatable': 'no', 'Exploitation': 'poc', 'Technical Impact': 'partial'}, 'version': '2.0.3'}
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'}
Weaknesses
  • CWE-670

    Always-Incorrect Control Flow Implementation

Sources

Status
PUBLISHED
Assigner
VulnCheck
Published
Updated
Oct 26, 2026, 1:23 AM
Reserved
Aug 10, 2026, 1:02 PM

View source JSON

Updated
Oct 26, 2026, 1:23 AM

JSON

Status
Deferred
Published
Aug 24, 2026, 8:17 PM
Modified
Oct 26, 2026, 2:17 AM

View source JSON

No data.

Updated
Aug 28, 2026, 8:38 PM

JSON