CVE-2026-72705

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.