CVE-2026-72705

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

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.

Remediation

No solution or workaround provided in the CVE record

Tracking

Sign in to view the affected projects.

Advisories

No advisories available
History
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

Sources

Status
PUBLISHED
Assigner
VulnCheck
Published
Updated
Oct 26, 2026, 1:23 AM
Reserved
Aug 10, 2026, 1:02 PM
Status
Deferred
Published
Aug 24, 2026, 8:17 PM
Modified
Oct 26, 2026, 2:17 AM