Recursive Call Vulnerability in Rocq Prover by Endrazine
CVE-2026-72705

6.8MEDIUM

Key Information:

Vendor

Rocq-prover

Status
Rocq
Vendor
CVE Published:
24 August 2026

Badges

👾 Exploit Exists🟡 Public PoC

What is CVE-2026-72705?

The guard checker in Rocq Prover is susceptible to a type safety violation where recursive calls using fixpoint arguments are inadequately tracked. This could lead to scenarios where a type becomes definitionally equal to its negation. Consequently, self-application can produce false results within purely definitional contexts, potentially leading to misinterpretations in the code. This vulnerability has been addressed in the Rocq Prover version 9.2.0.

Affected Version(s)

rocq 0 < 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-72705 - Proof of Concept

References

https://github.com/rocq-prover/rocq
product
https://github.com/rocq-prover/rocq/issues/21683
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)
.