CVE-2026-72703
Description
A flaw was found in Rocq Prover. The guard checker incorrectly processes parameters of nested mutual fixpoints when cross-calls occur between different bodies of the fixpoint. This oversight allows the system to accept non-terminating definitions as structurally decreasing. This critical logical flaw enables an attacker to prove False, which in a proof assistant, means any arbitrary proposition can be proven, thereby undermining the integrity of the system.
Statement
Red Hat Product Security has determined that this vulnerability does not affect any currently supported Red Hat product. This assessment may evolve based on further analysis and discovery. For more information about this vulnerability and the products it affects, please see the linked references.
Mitigation
Mitigation for this issue is either not available or the currently available options do not meet the Red Hat Product Security criteria comprising ease of use and deployment, applicability to widespread installation base, or stability.
Understanding the Weakness (CWE)
Availability
Technical Impact: DoS: Resource Consumption (CPU); DoS: Resource Consumption (Memory); DoS: Amplification
An infinite loop will cause unexpected consumption of resources, such as CPU cycles or memory. The software's operation may slow down, or cause a long time to respond.
Frequently Asked Questions
Not sure what something means? Check out our Security Glossary.
Want to get errata notifications? Sign up here.
