Guard Checker Vulnerability in Rocq Prover by Rocq Technologies
CVE-2026-72703

6.8MEDIUM

Key Information:

Vendor

Rocq-prover

Status
Rocq
Vendor
CVE Published:
24 August 2026

Badges

👾 Exploit Exists🟡 Public PoC

What is CVE-2026-72703?

The guard checker in Rocq Prover erroneously classifies a nested mutual fixpoint parameter as uniform without performing a thorough analysis of inter-body calls. The function find_uniform_parameters only evaluates self-recursive calls, leading to the risk of accepting a non-terminating definition as structurally decreasing. This oversight allows for the potential generation of terms that equate with their own successors, ultimately producing a proof of False. This vulnerability, present from Coq version 8.20 and resolved in Rocq version 9.2.0, demonstrates a significant flaw in parameter handling during fixpoint evaluations.

Affected Version(s)

rocq 8.20 < 9.2.0

Exploit Proof of Concept (PoC)

PoC code is written by security researchers to demonstrate the vulnerability can be exploited. PoC code is also a key component for weaponization which could lead to ransomware.

CVE-2026-72703 - Proof of Concept

References

https://github.com/rocq-prover/rocq
product
https://github.com/rocq-prover/rocq/issues/21682
issue-tracking
https://github.com/rocq-prover/rocq/pull/21684
issue-tracking

CVSS V4

Score:
6.8
Severity:
MEDIUM
Confidentiality:
None
Integrity:
High
Availability:
None
Attack Vector:
Local
Attack Complexity:
Low
Attack Required:
None
Privileges Required:
Undefined
User Interaction:
Unknown

Timeline

  • 🟡

    Public PoC available

  • 👾

    Exploit known to exist

  • Vulnerability published

  • Vulnerability Reserved

Credit

Tristan Stérin
Jonathan Brossard (MOABI)
.