Skip to content

CVEs Search About

synced 43 MIN AGOT-43M

01 RecordSTATE: —

02 Description

SRC: CNA

03 Metadata

SCHEMA: CVE JSON 5

04 Affected products

PAIRS: —

05 References

REFS: —

CVE content courtesy of the CVE Program (cve.org). exploit.cc is not an official CVE Program property. CVE data sourced from github.com/CVEProject/cvelistV5.

SRC: CVELISTV5 / SYNC: T-43M / LAG: 49M / REC: 381,617 / REV: C6-1C / V4

01 RecordSTATE: PUBLISHED

CVE-2026-72844

Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

MediumPUBLISHEDCNA: VulnCheck

Base score6.8 CVSS v4.0CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N

View raw JSON CVE Program record

02 Description

CNA: VulnCheck

Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

03 Metadata

SCHEMA: 5.2

Published

2026-08-20 17:19Z1 DAY AGO

Last updated

2026-08-21 21:46Z3 HR AGO

Reserved

2026-08-10

Assigning CNA

VulnCheck

Record state

PUBLISHED

Severity

Medium (CVSS 6.8)

CVSS vector

CVSS:4.0/AV:L/AC:L/AT:N/PR:N/UI:P/VC:N/VI:H/VA:N/SC:N/SI:N/SA:N

Weaknesses

CWE-843Access of Resource Using Incompatible Type ('Type Confusion')Base

SSVC decision

ExploitationpocAutomatablenoTechnical Impactpartial

Data version

5.2

Document digest

95c6fc222c2a11b033c61a9d3df1b4d69434a6ff3240abcc4cc3cd2d30007943

04 Affected products

PAIRS: 1

VendorProductVersionsPlatforms

leanproverlean40 to < 4.32.2, 4.33.0-rc1—

05 References

REFS: 8

github.comGitHub Issue #14576https://github.com/leanprover/lean4/issues/14576issue-tracking
github.comfix: missing check at kernel inductive declarationhttps://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808patch
github.comGitHub Pull Request #14577https://github.com/leanprover/lean4/pull/14577issue-tracking
github.comlean-cve-pochttps://github.com/endrazine/lean-cve-pocexploit
github.comCollatzLeanhttps://github.com/xrchz/CollatzLeanexploit
www.openwall.comoss-security: Lean 4 kernel soundness bughttps://www.openwall.com/lists/oss-security/2026/08/02/1third-party-advisory
github.comhttps://github.com/leanprover/lean4product
www.vulncheck.comVulnCheck Advisory: Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projectionshttps://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projectionsthird-party-advisory