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 进程内运行的元程序可以注册一个类型不良的嵌套归纳类型，其构造函数会将一个属于不相关类型 W 的值通过 投影进行访问。内核通过标准的 路径（该路径在最大程度的内核检查下运行）接受此声明，整个过程无需使用 、 、 、 、FFI，也不需要修改 文件。 该漏洞导致类型混淆，进而生成一个无需引入公理（axioms）即可证明 的
Possible ATT&CK Techniques 1 AI
T1195 · Supply Chain CompromiseAffected Version Matrix 3
| Vendor | Product | Version Range | Status |
|---|---|---|---|
| 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
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 POCIII. 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 weakness: CWE-843
V. Comments for CVE-2026-72844
No comments yet