Executive brief
Rocq Prover is a formal verification tool used to create machine-checked mathematical proofs for critical software systems, including formally verified compilers and cryptocurrency infrastructure. A flaw in its type-checking system allows malicious or crafted proof code to bypass safety guarantees and prove false statements, undermining the trustworthiness of any proofs verified by vulnerable versions.
Technical details
The vulnerability is a logic error in the guard checker, a component that enforces structural recursion constraints on fixpoint definitions. 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 arguments that are not subterms of the original structural argument. This permits construction of a Russell's paradox variant, creating a type definitionally equal to its own negation (russell 1 ≡ russell 1 → False), which can be self-applied to derive False in purely definitional code. The exploit requires no axioms, tactics, unsafe features, or plugins, and is detectable only by analyzing the proof structure. Fixed in Rocq 9.2.0 (PR #21684).
Affected products
- Rocq Rocq Prover ≤ 9.1.0
Timeline
- 2026-08-24: disclosed
- 2026: patched: Fixed in Rocq 9.2.0