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

Goal: 1000 CNY · Raised: 1359 CNY

100%
Buy Us a Coffee

CVE-2026-72844— Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

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.

Lean 4是Lean组织的一个交互式定理证明与函数式编程框架。 Lean 4 4.32.2之前版本和4.33.0-rc1版本存在缓冲区错误漏洞，该漏洞源于内核未验证投影表达式中的结构类型与值类型匹配，且environment::add_inductive未对嵌套归纳应用进行类型检查，可能导致类型混淆，进而产生无公理False证明并推导出任意命题。

CVSS 6.3 · Medium EPSS 0.18% · P7

Possible ATT&CK Techniques 1 AI

T1195 · Supply Chain Compromise

Affected Version Matrix 3

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

I. Basic Information for CVE-2026-72844

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 Kernel Type Checking Bypass via Mismatched Structure Projections
Source: CVE Program / CVE List V5
Vulnerability Description
The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.
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
Lean 4 缓冲区错误漏洞
Source: CNNVD (China National Vulnerability Database)
Vulnerability Description
Lean 4是Lean组织的一个交互式定理证明与函数式编程框架。 Lean 4 4.32.2之前版本和4.33.0-rc1版本存在缓冲区错误漏洞，该漏洞源于内核未验证投影表达式中的结构类型与值类型匹配，且environment::add_inductive未对嵌套归纳应用进行类型检查，可能导致类型混淆，进而产生无公理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-72844

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

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

Patches & Fixes for CVE-2026-72844 (2)

Vendor Advisories for CVE-2026-72844 (1)

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

Mailing List Discussions for CVE-2026-72844 (1)

Other References for CVE-2026-72844 (1)

IV. Related Vulnerabilities

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

V. Comments for CVE-2026-72844

No comments yet

Leave a comment