CVE-2026-72705

CVE-2026-72705 is a soundness flaw in the guard checker of Rocq Prover (before 9.2.0). The checker fails to track recursive calls when a fixpoint passes itself as a higher-order argument to another fixpoint, which then applies it to a non-subterm value. This admits a type definitionally equal to ...