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-72704

CVE-2026-72704MEDIUM

rocq-prover rocq — Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport

  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-72704 (rocq-prover rocq). Public exploit reference added.
  Aug 24  Published (CNA: VulnCheck)
  Aug 25  EXPLOIT PUBLISHED — CVE-2026-72704 (rocq-prover rocq). Public exploit reference added.
  Aug 29  EXPLOIT PUBLISHED — CVE-2026-72704 (rocq-prover rocq). Public exploit reference added.
  Sep 24  EXPLOIT PUBLISHED — CVE-2026-72704 (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 recheck the recursive tree representation of an inductive type parameter after that parameter has been changed by transport. A fixpoint may apply a rewrite along an equality between types to its recursive argument, which the guard checker accepts because the inductive type is preserved, while the recursive tree recorded for the parameter is altered. A second fixpoint that calls the first inherits the altered recursive tree without verification, so a call that is not structurally decreasing is accepted as terminating. The resulting non-terminating definition proves that a natural number equals its own successor and therefore False, from which any proposition follows. The demonstration uses two axioms that follow from univalence and are consistent with the calculus of inductive constructions, so the contradiction comes from the guard check rather than from the assumptions. A fix is proposed but not merged.

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-72704 (rocq-prover rocq). Public exploit reference added.
August 24, 2026	Published	Published (CNA: VulnCheck)
August 25, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72704 (rocq-prover rocq). Public exploit reference added.
August 29, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72704 (rocq-prover rocq). Public exploit reference added.
September 24, 2026	EXPLOIT PUBLISHED	EXPLOIT PUBLISHED — CVE-2026-72704 (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-22024 [exploit]
https://github.com/rocq-prover/rocq [product]
https://github.com/rocq-prover/rocq/issues/22024 [issue-tracking]
https://github.com/rocq-prover/rocq/pull/22027 [issue-tracking, patch]
https://www.vulncheck.com/advisories/rocq-prover-through-guard-checker-trusts-corrupted-recursive-tree-after-transport [third-party-advisory]

Authoritative record: CVE-2026-72704 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-72704 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.