CVE-2026-72704: Rocq guard checker trusts corrupted recursive tree after transport (0 = 1 demonstrated) — 0-day
// AI summary
Rocq guard checker has a soundness bug allowing construction of a checked proof of False, demonstrated by 0 = 1, because it does not recheck the recursive tree after transport.
// from the source
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. A fixpoint applies a rewrite along a type equality to its recursive argument; the...