CVE-2026-72844

See a problem?
Please try reporting it to the source first.
Source
https://cve.org/CVERecord?id=CVE-2026-72844
Import Source
https://storage.googleapis.com/cve-osv-conversion/osv-output/CVE-2026-72844.json
JSON Data
https://api.osv.dev/v1/vulns/CVE-2026-72844
Published
2026-08-20T17:19:34Z
Modified
2026-08-24T03:59:16Z
Severity
  • 6.8 (Medium) CVSS_V4 - 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 CVSS Calculator
Summary
Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections
Details

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.

Database specific 
{
    "cna_assigner": "VulnCheck",
    "cwe_ids": [
        "CWE-843"
    ],
    "osv_generated_from": "https://github.com/CVEProject/cvelistV5/tree/main/cves/2026/72xxx/CVE-2026-72844.json"
}
References

Affected packages

Git / github.com/leanprover/lean4

Affected ranges

Type
GIT
Repo
https://github.com/leanprover/lean4
Events
Introduced
0 Unknown introduced commit / All previous commits are affected
Introduced
62eed1db4d67327ec8120be05f1a1b0847d74561
Fixed
a39eab69e1eee9ad38f4efe507907b1026a77808
Database specific
Show details 
{
    "extracted_events": [
        {
            "introduced": "0"
        },
        {
            "fixed": "4.32.2"
        },
        {
            "introduced": "4.33.0-rc1"
        },
        {
            "last_affected": "4.33.0-rc1"
        }
    ],
    "source": [
        "AFFECTED_FIELD",
        "REFERENCES"
    ]
}

Affected versions

4.*
4.33.0-rc1
Other
CADE25
ICFP19
ICFP20
IFL
IFL19
IJCAR20
IJCAR20-LMCS
NFM2022
cade2021
cade21
nightly-2018-03-19
nightly-2018-03-26
nightly-2018-03-27
nightly-2018-03-29
nightly-2018-03-30
nightly-2018-04-02
nightly-2018-04-06
nightly-2018-04-10
popl_17
popl_2017
popl_paris_2017
test1
test2
v3.*
v3.0.0
v3.1.0
v3.2.0
v3.3.0
v4.*
v4.0.0-M1
v4.0.0-m1
v4.0.0-m2
v4.0.0-m3
v4.0.0-m4
v4.0.0-m5
v4.0.0-rc1
v4.0.0-rc2
v4.0.0-rc3
v4.0.0-rc4
v4.12.0-rc1

Database specific

source 
"https://storage.googleapis.com/cve-osv-conversion/osv-output/CVE-2026-72844.json"
vanir_signatures 
[
    {
        "deprecated": false,
        "digest": {
            "function_hash": "151061590017594300886269883507905875713",
            "length": 2440
        },
        "id": "CVE-2026-72844-6edad654",
        "signature_type": "Function",
        "signature_version": "v1",
        "source": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808",
        "target": {
            "file": "src/kernel/inductive.cpp",
            "function": "environment::add_inductive"
        }
    },
    {
        "deprecated": false,
        "digest": {
            "line_hashes": [
                "87228126211685352155538230884846912068",
                "63381581372863484823848030229876762206",
                "256305726175152380745516568565018862995",
                "87430265600039924126696631875317834597",
                "142720749022433809561586080289880991884",
                "271475237214433260452254562801380272735",
                "156059277533398028813518540897118091183",
                "155886352923744264237991165021505617941",
                "278747475749210048556795106875370179763",
                "281431326285065435009321797089092381050",
                "232322387652805797400282485226993914693",
                "224511068663990502764521758495207921646",
                "47019820594276833920491886486814361908",
                "220465816523729496372338387361707987361",
                "335069605500433213827959151101847209819",
                "311055000491514373802279163259657339261"
            ],
            "threshold": 0.9
        },
        "id": "CVE-2026-72844-f6fa7294",
        "signature_type": "Line",
        "signature_version": "v1",
        "source": "https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808",
        "target": {
            "file": "src/kernel/inductive.cpp"
        }
    }
]
vanir_signatures_modified 
"2026-08-24T03:59:16Z"