CVE-2026-72703

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.