Reference page — cumulative record through Saturday, October 3, 2026 UTC. Reference pages update as the archive grows; only dated daily editions are immutable pages of record.

CVE-2026-72705

CVE-2026-72705MEDIUM

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

  AV  AC  AT  PR  UI  VC  VI  VA   CVSS    EPSS   %ile   KEV
   L   L   N   N   P   N   H   N    6.8   .0018    6.5     —

AFFECTED
  Product  Versions     Fixed
  rocq     unspecified  —

TIMELINE
  Aug 10  Reserved by VulnCheck
  Aug 24  EXPLOIT PUBLISHED — CVE-2026-72705 (rocq-prover rocq). Public exploit reference added.
  Aug 24  Published (CNA: VulnCheck)
  Aug 26  EXPLOIT PUBLISHED — CVE-2026-72705 (rocq-prover rocq). Public exploit reference added.
  Aug 29  EXPLOIT PUBLISHED — CVE-2026-72705 (rocq-prover rocq). Public exploit reference added.
  Sep 24  EXPLOIT PUBLISHED — CVE-2026-72705 (rocq-prover rocq). Public exploit reference added.

CWE-670 · CNA: VulnCheck · CVSS v4.0 · 5 references · NVD status: Deferred

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.

Lifecycle

Complete event history — 6 events, chronological
Date	Event	Detail
August 10, 2026	Reserved	Reserved by VulnCheck
August 24, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72705 (rocq-prover rocq). Public exploit reference added.
August 24, 2026	Published	Published (CNA: VulnCheck)
August 26, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72705 (rocq-prover rocq). Public exploit reference added.
August 29, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72705 (rocq-prover rocq). Public exploit reference added.
September 24, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72705 (rocq-prover rocq). Public exploit reference added.

Affected

Affected products and packages — 1 row
Vendor	Product / Package	Ecosystem	Version introduced	Fixed
rocq-prover	rocq	—	—	—

Weaknesses

CWE-670

References (5)

https://github.com/endrazine/rocq-cve-poc-21683 [exploit]
https://github.com/rocq-prover/rocq [product]
https://github.com/rocq-prover/rocq/issues/21683 [issue-tracking]
https://github.com/rocq-prover/rocq/pull/21684 [issue-tracking, patch]
https://www.vulncheck.com/advisories/rocq-prover-before-guard-checker-accepts-fixpoint-passed-as-a-higher-order-argument [third-party-advisory]

Authoritative record: CVE-2026-72705 at cve.org

Vendors: rocq-prover

Weaknesses: CWE-670

About this page

This is a reference page, not a dated page of record. It assembles the complete lifecycle of CVE-2026-72705 from the CVE Program record, NVD enrichment, the CISA KEV catalog, EPSS, and OSV advisories. The box score's numbers (CVSS, EPSS, KEV status) are current as of Saturday, October 3, 2026 UTC and are re-derived as the archive grows; only dated daily editions are immutable pages of record. The authoritative source for this identifier is cve.org.