Executive brief
Rocq Prover is an interactive theorem prover used for formal verification of mathematical proofs and software correctness. A flaw in its guard checker (which validates that recursive functions terminate) allows attackers to prove false statements by corrupting the internal recursion tracking mechanism. An exploit can demonstrate that 0 equals 1, undermining the logical soundness of any formal proof that relies on this component.
Technical details
The guard checker in Rocq Prover fails to recheck the rectree (recursion tree representation) of inductive type parameters after they are modified through transport operations (type rewrites). A fixpoint can silently corrupt the rectree by applying a rewrite to its recursive argument; when a second fixpoint calls the first, it inherits the corrupted rectree without re-verification, leading the guard checker to incorrectly accept non-terminating definitions as structurally decreasing. The exploit uses two axioms consistent with univalence and the calculus of inductive constructions, then constructs a non-terminating function that produces the contradiction 0=1. The root cause is CWE-670 (control flow implementation error), and no public patch has been merged as of the advisory date.
Affected products
- Rocq Prover Project Rocq Prover ≤ 9.2.0
Timeline
- 2026-08-24: disclosed
- 2026-08-24: advisory