BaselineWatch
Desk
Your fleet and your work Fleetyour releases and the hardware they run onTriagewhat needs a decisionWatchlistthe products and platforms you runSaved searchesthe lists you come back to
This instance Sourceswhat is read, how often, under what termsDigestthe daily or weekly summary, and alerts
How it is drawn Appearancethe look and the colour schemeBrandingthe mark this instance wears
Owner sign-in

CVE-2026-72705

6.8 medium exploit SSVC exploitation: poc Deferred
NVD · CVE.org

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.

Fix

Nothing published yet: no patch, vendor advisory or mitigation reference on NVD, no vendor advisory in the News for this CVE, not in CISA's KEV, no fixed package version. BaselineWatch does not guess at one.

Public exploits 1

Each line links to the index that lists it, never to exploit code. Exploit-DB's "verified" and a Metasploit rank of good or better count as verified; a PoC-in-GitHub entry is a repository's claim.

Change history 2

  1. References+1 references (now 6)NVD modified 2026-10-26 02:17
  2. First seenCVSS 6.8NVD modified 2026-10-12 15:10

Affected (CPE criteria) 0

NVD has not attached CPE configurations yet.

References 6