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

Goal: 1000 CNY · Raised: 1359 CNY

100%
Buy Us a Coffee

CVE-2026-72711— Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable

Quick assessment

Affected
leanprover lean4
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.

leanprover lean4是leanprover个人开发者的一款交互式定理证明器。 leanprover lean4 4.32.2之前版本存在输入验证错误漏洞，该漏洞源于未正确检查不透明声明的主体是否闭合（缺少闭包检查），可能导致攻击者利用类型检查器推断缓存绕过局部上下文检查，创建类型为False的不透明常量，从而推导出任意命题。

CVSS 6.3 · Medium EPSS 0.18% · P7

Affected Version Matrix 1

VendorProduct Version RangeStatus
leanprover lean4 < 4.32.2 affected
Get alerts for future matching vulnerabilities Log in to subscribe

I. Basic Information for CVE-2026-72711

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
Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable
Source: CVE Program / CVE List V5
Vulnerability Description
The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.
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
Vulnerability Title
leanprover lean4 输入验证错误漏洞
Source: CNNVD (China National Vulnerability Database)
Vulnerability Description
leanprover lean4是leanprover个人开发者的一款交互式定理证明器。 leanprover lean4 4.32.2之前版本存在输入验证错误漏洞，该漏洞源于未正确检查不透明声明的主体是否闭合（缺少闭包检查），可能导致攻击者利用类型检查器推断缓存绕过局部上下文检查，创建类型为False的不透明常量，从而推导出任意命题。
Source: CNNVD (China National Vulnerability Database)
CVSS Information
N/A
Source: CNNVD (China National Vulnerability Database)
Vulnerability Type
N/A
Source: CNNVD (China National Vulnerability Database)

Affected Products

Vendor Product Affected Versions CPE Subscribe
leanprover lean4 0 ~ 4.32.2 -

II. Public POCs for CVE-2026-72711

# 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-72711

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

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

Vendor Advisories for CVE-2026-72711 (1)

Proof of Concept for CVE-2026-72711 (2)

IV. Related Vulnerabilities

Same product: lean4
Same vendor: leanprover
Same weakness: CWE-20

V. Comments for CVE-2026-72711

No comments yet

Leave a comment