CVE Intelligence
Medium Memory corruption exploit reference

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

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.

Published Aug 20, 2026 · Updated Oct 15, 2026 · Sources: NIST National Vulnerability Database, CVE Program (cve.org) e CISA ADP · CNA: VulnCheck

Who exploits it and how urgent it is

A 0–100 score combining confirmed exploitation, ransomware and APT use, public exploits, EPSS and severity.

No exploitation signal in the sources consulted so far.
How the score was calculated
  • Technical severity (medium)+3
  • CISA SSVC: exploitation "poc"+5

The score orders the patch queue; it does not replace your asset context (internet exposure, criticality, compensating controls).

Triage

Is it exploited, how likely is exploitation, what does it touch, and how severe do the sources call it.

Exploitation
Not confirmed
Not in CISA KEV — an absence of record, not proof it is unexploited.
EPSS FIRST
—
No EPSS score.
Affects
Leanprover
Lean4
CVSS base
6.3
Medium · 2 source(s)

CISA SSVC assessment CISA

Three decision points CISA publishes for the CVEs it assesses (SSVC 2.0.3). A stakeholder decision, not a severity score.

Exploitation
Proof of concept
none · proof-of-concept · active
Automatable
No
can an attacker script the kill-chain steps
Technical impact
Partial
partial · total control of the vulnerable component

Remediation

Fixes and mitigations documented by the sources — linked to the original advisory.

No fix documented by the sources we poll. That does not mean none exists: check the vendor advisory.

First 24 hours

Ordered from the record’s own fields — exposure first, because you cannot patch what you have not found. A rule-generated starting point.

  1. Identify exposed assets running the affected vendor/product/version combinations (Leanprover Lean4).
  2. No fix documented in the sources: reduce exposure and monitor the vendor advisory.
  3. Exploitation requires user interaction: tighten email/web filtering and warn affected users.
  4. Search available logs for exploit probes matching the vulnerability class (memory corruption), errors and authentication anomalies.

Affected scope

Vendor, product and versions as the sources word them.

VendorProductVersionsStatusSource
Leanprover Lean4 < 4.32.2version 4.33.0-rc1 Vulnerable CVE Program (cve.org) e CISA ADP

Attack characteristics

The CVSS vector, decoded. It describes the attack, not your exposure to it.

Attack vector
Local
Attack complexity
Low
Privileges required
None
User interaction
Required
Scope
Changed
Confidentiality
None
Integrity
High
Availability
None

Every base score collected

Sources score independently and may disagree; each row says who scored it and under which version.

ScoreVersionSeverityExpl.ImpactScored by
6.8 CVSS 4.0 Medium — — disclosure@vulncheck.com via NIST National Vulnerability Database
6.8 CVSS 4.0 Medium — — VulnCheck via CVE Program (cve.org) e CISA ADP
6.3 CVSS 3.1 Medium 1.8 4.0 disclosure@vulncheck.com via NIST National Vulnerability Database
6.3 CVSS 3.1 Medium — — VulnCheck via CVE Program (cve.org) e CISA ADP
CVSS:3.1/AV:L/AC:L/PR:N/UI:R/S:C/C:N/I:H/A:N (score shown at the top: disclosure@vulncheck.com)

Weakness MITRE

Weakness class according to MITRE’s CWE catalog.

CWE-843 · Type Confusion

Other CVEs with this weakness →

Detection

Read off the CVSS vector and the weakness class. Starting points, not tested rules.

  • Local/physical vector: focus on endpoint telemetry (EDR) from affected hosts.
  • Correlate service crashes/restarts with inbound traffic; repeated crashes may indicate attempts.
endpoint telemetry (EDR)crash dumps

Timeline

What happened to this CVE, newest first.

  • 2026
  • Affected products added · leanprover/lean4
    Oct 15, 2026 · CVE Program (cve.org) e CISA ADP
  • SSVC assessment updated
    Oct 15, 2026 · CVE Program (cve.org) e CISA ADP
  • Record published
    Oct 15, 2026
  • CVSS changed · 6.3
    Oct 15, 2026 · NIST National Vulnerability Database
  • Source status changed · → Deferred
    Oct 15, 2026 · NIST National Vulnerability Database
  • Record created in this database
    Oct 15, 2026 · NIST National Vulnerability Database
  • CVE published
    Aug 20, 2026 · VulnCheck

Source activity

Repeated readings are counted rather than listed.

  • 1× Official description updated · Oct 15, 2026 – Oct 15, 2026

References

8 on the record

Elsewhere on this site

Leanprover
every CVE for this vendor
Memory corruption
same class
CWE-843
other pages naming this weakness

Related CVEs (same products)

  • CVE-2026-72711 Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable Aug 24, 2026

Not in any source we poll

Listed rather than left blank: an empty field and an unmeasured one look identical on screen, and only one is a reason to look elsewhere.

  • No FIRST EPSS score.
  • No fixed version, patch or mitigation documented.
  • No confirmed IOCs, IP addresses, domains, file hashes, or malware artifacts supplied.
  • No organization-specific asset inventory, compensating-control status, or patch deployment evidence supplied.
  • No exploit packet captures, log samples, or incident case IDs supplied.

Answered from this record

Text assembled only from the fields above — no additional claims.

What should defenders know first?

CVE-2026-72844 is "Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections", rated Medium. It affects Lean4 (Leanprover); versions are in the scope table. It is not in CISA KEV, which does not rule out exploitation. CVSS 6.3 describes technical severity. First verify whether exposed or business-critical assets run the affected versions, apply vendor fixes or mitigations, and preserve logs for review.

Comments

Moderated technical discussion. Read the community guidelines.

No comments yet.

Sign in or create an account to comment and suggest corrections.