---
id: CVE-2026-72705
title: >-
  The guard checker in Rocq Prover does not follow recursive calls made through
  a fixpoint's own arguments
summary: >-
  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 …
severity: medium
cvss: 6.3
cvssVector: 'CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N'
cwe:
  - CWE-670
published: '2026-08-24'
updated: '2026-09-08'
sourceUpdated: '2026-09-08T20:23:49.880'
source: NVD
sourceUrl: 'https://nvd.nist.gov/vuln/detail/CVE-2026-72705'
references:
  - url: 'https://github.com/endrazine/rocq-cve-poc-21683'
    label: disclosure@vulncheck.com
  - url: 'https://github.com/rocq-prover/rocq'
    label: disclosure@vulncheck.com
  - url: 'https://github.com/rocq-prover/rocq/issues/21683'
    label: disclosure@vulncheck.com
  - url: 'https://github.com/rocq-prover/rocq/pull/21684'
    label: disclosure@vulncheck.com
  - url: >-
      https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument
    label: disclosure@vulncheck.com
tags:
  - nvd
  - cve.org
  - exploit-available
epss: 0.00176
epssPercentile: 0.06331
ingestedAt: '2026-09-08T21:11:12.285Z'
vendor: rocq-prover
product: rocq
affected:
  - rocq < 9.2.0
exploitAvailable: true
ssvc:
  exploitation: poc
  automatable: 'no'
  technicalImpact: partial
  timestamp: '2026-08-26T15:46:51.503814Z'
---

## Overview

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

Refer to the linked advisories for vendor-supplied fixes and affected version ranges.