Executive brief
Rocq Prover, an interactive theorem prover used for formal verification and mathematical proof development, contains a flaw in its guard checker that incorrectly validates recursive function definitions. An attacker can craft a non-terminating function definition that the prover accepts as valid, allowing them to prove false statements and derive contradictions that undermine the soundness of the proof system.
Technical details
The vulnerability is a logical inconsistency in the guard checker mechanism (kernel/inductive.ml) that validates recursive function definitions. The find_uniform_parameters function inspects only self-recursive calls within nested mutual fixpoints and incorrectly marks parameters as uniform when no body calls itself, failing to examine cross-calls between different fixpoint bodies. When a parameter grows through such cross-calls, it retains an inherited subterm specification that allows recursive calls to be accepted even though their arguments are not structurally smaller. This permits non-terminating definitions to be admitted as structurally decreasing, enabling construction of a term whose value equals its own successor, yielding a proof of False without requiring axioms or unsafe flags. The vulnerability was introduced in Coq 8.20 and is patched in Rocq 9.2.0.
Affected products
- Rocq Rocq Prover 8.20 through 9.1.x
Timeline
- 2026-08-24: disclosed
- 2026: patched: Fixed in Rocq 9.2.0