Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument (CVE-2026-72705) | HOL Guard CVE

Unknown severity · Source severity not reportedCVE-2026-72705

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

Answer in brief

CVE-2026-72705 records a Unknown severity vulnerability in Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument. The current sources do not mark it as known exploited. The current feed maps rocq-prover/rocq (generic). Check affected ranges and fixed versions before updating.

Analysis pending evidence review

HOL Guard separates source facts from reviewed analysis. See the methodology.

Published Aug 24, 2026Updated Aug 24, 2026Source checked Aug 24, 2026First seen by HOL Aug 24, 2026Material review Aug 24, 2026

Upstream Advisory

Key facts

Risk: Unknown severitySource severity not reported
Exploitation: Not marked as known exploited
Affected software: 1 mapped package or product
Fix availability: Available

Why this deserves its current priority

A CVSS score is not reported in the current record. The current sources do not mark it as known exploited. Treat this as a source-backed prioritization signal, not a statement about your environment.

Analysis status

Analysis pending evidence review

Factual feed record only; HOL analysis is not approved for indexing. Read the methodology.

Affected scope and exposure questions

The current feed maps rocq-prover/rocq (generic). Check affected ranges and fixed versions before updating.

Mapped affected packages and fixed versions
Package	Affected range	Fixed version
rocq-prover/rocqgeneric	>=0 <9.2.0	9.2.0

Recommended response

Check inventory. Check lockfiles and deployed manifests for rocq-prover/rocq.
Review the reported fix. Update rocq-prover/rocq to 9.2.0 if you use the affected versions. Test the change in a non-production environment first.

Evidence timeline and material changes

Published upstream
Aug 24, 2026
Evidence: source:cvelist:source_dates:source-dates:record
Source modified
Aug 24, 2026
Evidence: source:cvelist:source_dates:source-dates:record
First seen by HOL
Aug 24, 2026

Sources and claim methodology

Upstream source 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.

Quoted source text, attributed separately from HOL analysis.