CVE-2026-72705 — MEDIUM (6.3)

Vulnerability Description

The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies it to a value that is not a subterm of the structural argument. Passing the recursive function to a plain definition is rejected because the checker unfolds the definition and observes the call, but passing it to a fixpoint is accepted because higher-order recursive calls through fixpoint arguments are not tracked. This admits a type that is definitionally equal to its own negation, so self-application produces False in purely definitional code, without tactics, axioms, plugins or unsafe flags, and Print Assumptions reports the result as closed under the global context. Fixed in Rocq 9.2.0.

CVSS Score

6.3

MEDIUM

CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N

Attack Vector

LOCAL

Attack Complexity

LOW

Privileges Required

NONE

User Interaction

REQUIRED

Scope

CHANGED

Confidentiality

NONE

Integrity

HIGH

Availability

NONE

Related Weaknesses (CWE)

CWE-670

References

FAQ

What is CVE-2026-72705?

CVE-2026-72705 is a vulnerability with a CVSS score of 6.3 (MEDIUM). The guard checker in Rocq Prover does not follow recursive calls made through a fixpoint's own arguments. A fixpoint may pass itself as a higher-order argument to a second fixpoint, which then applies...

How severe is CVE-2026-72705?

CVE-2026-72705 has been rated MEDIUM with a CVSS base score of 6.3/10. Review the CVSS metrics above for detailed severity breakdown.

Is there a patch for CVE-2026-72705?

Check the references section above for vendor advisories and patch information. Review vendor security bulletins for remediation guidance.