Tristan Stérin

**Name of the Vulnerable Software and Affected Versions** Coq versions 8.20 through 9.1.x **Description** The guard checker incorrectly treats a parameter of a nested mutual fixpoint as uniform because the `find uniform parameters` function in `kernel/inductive.ml` only inspects self-recursive calls. When no body calls itself, the system concludes all parameters are uniform. Consequently, a parameter that increases through a cross-call between different bodies retains the subterm specification from the enclosing fixpoint. This allows a recursive call to be accepted even if the argument is not structurally smaller, permitting a non-terminating definition to be admitted as structurally decreasing. This can lead to a proof of False, allowing any proposition to be proven without requiring axioms, plugins, or unsafe flags. **Recommendations** Update to Rocq version 9.2.0.

**Name of the Vulnerable Software and Affected Versions** Rocq Prover versions prior to 9.2.0 **Description** The guard checker fails to track recursive calls made through a fixpoint's own arguments. This occurs when a fixpoint passes itself as a higher-order argument to another fixpoint, which then applies it to a value that is not a subterm of the structural argument. While passing a recursive function to a plain definition is rejected because the checker unfolds the definition, passing it to a fixpoint is accepted. This flaw allows for a type that is definitionally equal to its own negation, enabling self-application to produce False in purely definitional code without the use of tactics, axioms, plugins, or unsafe flags. **Recommendations** Update Rocq Prover to version 9.2.0.