Rocq guard checker trusts rewritten recursive tree (CVE-2026-72704)
Original title: CVE-2026-72704: Rocq guard checker trusts corrupted recursive tree after transport (0 = 1 demonstrated) — 0-day
After eq_rect or rew changes an inductive parameter, the checker does not recheck the recursive tree.
Jonathan Brossard reported a Rocq kernel soundness bug, labeled a 0-day in the post title. A fixpoint rewrites its recursive argument along a type equality, and the guard checker then trusts the recursive tree for that inductive parameter without rechecking it. The report says this produces a checked proof of False, including 0 = 1. Versions and a patch are not in the snippet.
Unconfirmed: The 0-day label is the poster's; exploitation by attackers is not stated.
- The transport uses eq_rect or rew on an inductive type parameter.
- The post title calls the issue a 0-day.
- A checked proof of 0 = 1 is described as demonstrated.
- No fixed version appears in the available text.
Impact: checked proof of False after a type transport
| Product | Affected |
|---|---|
| Rocq | — |
Vulnerabilities mentioned
All| CVE | Vulnerability | CVSS | EPSS | Signals | Published |
|---|---|---|---|---|---|
| CVE-2026-72704 | 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… | 6.8 | <1% |
From the original article
Posted by Jonathan Brossard on Oct 25 1. Summary ========== A soundness bug in the Rocq (formerly Coq) kernel's guard checker allows construction of a checked proof of False — and by extension, any proposition, including 0 = 1. The guard checker does not recheck the recursive tree (rectree) for an inductive type parameter after a transport (rewrite via eq_rect/rew) changes that parameter.
seclists.org
A short excerpt; the article and its images belong to the publisher. Summary, key facts and assessment above are AI-written from the article and can be wrong.