Goal Reached Thanks to every supporter — we hit 100%!

Goal: 1000 CNY · Raised: 1336 CNY

100%
Buy Us a Coffee

CVE-2026-72703— Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls

Quick assessment

Affected
rocq-prover rocq
Exploitation
No confirmed in-the-wild exploitation; assess based on exposure
Recommended action
Check the vendor advisory and references for a fixed version. If immediate upgrade is impossible, restrict exposure and increase monitoring.

在 Rocq Prover 中，守卫检查器（guard checker）将嵌套相互固定点（nested mutual fixpoint）的参数视为一致的（uniform），而未检查该固定点不同主体（body）之间的调用关系。 中的 函数仅检查自递归调用（self-recursive calls）；因此，当没有任何主体调用自身时，该函数会错误地得出结论认为所有参数都是一致的。 若某一参数通过从一个主体到另一个主体的交叉调用（cross-call）而不断增大，则该参数仍保留其从外层固定点继承而来的子项规范（subter

CVSS 6.3 · Medium

Possible ATT&CK Techniques 1 AI

T1588.001 · Malware
Get alerts for future matching vulnerabilities Log in to subscribe

I. Basic Information for CVE-2026-72703

Vulnerability Information
Have questions about the vulnerability? See if Shenlong's analysis helps!
View Shenlong Deep Dive ↗

Although we use advanced large model technology, its output may still contain inaccurate or outdated information.Shenlong tries to ensure data accuracy, but please verify and judge based on the actual situation.

Vulnerability Title
Rocq Prover 8.20 before 9.2.0 Guard Checker Accepts Non-Terminating Fixpoint via Unchecked Cross-Calls
Source: CVE Program / CVE List V5
Vulnerability Description
The guard checker in Rocq Prover treats a parameter of a nested mutual fixpoint as uniform without examining calls between the different bodies of that fixpoint. find_uniform_parameters in kernel/inductive.ml inspects only self-recursive calls, so when no body calls itself the function concludes that every parameter is uniform. A parameter that grows through a cross-call from one body to another therefore keeps the subterm specification it inherited from the enclosing fixpoint, and a recursive call guarded by that specification is accepted although the argument is not structurally smaller. A non-terminating definition is admitted as structurally decreasing, which yields a term whose value equals its own successor and so a proof of False, from which any proposition follows. The proof requires no axioms, plugins or unsafe flags and Print Assumptions reports it as closed under the global context. Introduced in Coq 8.20 and fixed in Rocq 9.2.0.
Source: CVE Program / CVE List V5
CVSS Information
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N
Source: CVE Program / CVE List V5
Vulnerability Type
控制流实现总是不正确
Source: CVE Program / CVE List V5

Affected Products

Vendor Product Affected Versions CPE Subscribe
rocq-prover rocq 8.20 ~ 9.2.0 -

II. Public POCs for CVE-2026-72703

# POC Description Source Link Shenlong Link
AI-Generated POC Premium

No public POC found.

Login to generate AI POC

III. Intelligence Information for CVE-2026-72703

请登录查看更多情报信息。

Patches & Fixes for CVE-2026-72703 (1)

Vendor Advisories for CVE-2026-72703 (1)

News Coverage for CVE-2026-72703 (1)

Other References for CVE-2026-72703 (1)

Same Patch Batch · rocq-prover · 2026-08-24 · 5 CVEs total

CVE-2026-72705 6.3 MEDIUM Rocq Prover before 9.2.0 Guard Checker Accepts Fixpoint Passed as a Higher-Order Argument
CVE-2026-72714 6.3 MEDIUM Rocq Prover through 9.2.0 Universe Checking State Desynchronised After Module Close
CVE-2026-72704 6.3 MEDIUM Rocq Prover through 9.2.0 Guard Checker Trusts Corrupted Recursive Tree After Transport
CVE-2020-37268 6.3 MEDIUM Coq and Rocq Prover Print Assumptions Omits Unsafe Universe Checking Inlined Through Param

IV. Related Vulnerabilities

Same product: rocq
Same vendor: rocq-prover
Same weakness: CWE-670

V. Comments for CVE-2026-72703

No comments yet

Leave a comment