CVE-2026-72844

MEDIUMPre-NVD 6.36.3—
EchelonGraph scoreMEDIUM confidence

Score 6.3 from GitHub Security Advisory published 2026-08-20. A secondary CVSS source baseline 6.3; sources differ by 0.0.

Triggered by: GitHub Security Advisory CVSS
Sources: epss, ghsa, secondary
Trending — 3 sources updated this weekElevated
6.3EG
EchelonGraph verdictMonitorLow exploitation likelihood right now — keep watching.
  • Lower severity and no public exploit yet
CISA-KEV: Not listedEPSS PROB: 0.2%CVSS: 6.3Exploit: Elevated riskExposed services: Not assessed

An upstream fix is merged but not yet released — mitigate (WAF / firewall / segmentation) until the release ships, then apply it.

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.

CVSS v3
6.3
EG Score
6.3MEDIUMmedium confidence
EG Risk
44
EG Risk 44/100CISA SSVC

EG Risk is EchelonGraph's 0–100 priority score: it fuses intrinsic severity with real-world exploitation and automatability so you can rank equal-severity CVEs and fix the most dangerous first. Higher = act sooner. Distinct from the 0–10 EG Score (severity).

How it’s computed
Severity63% × 45%
Exploitation40% × 40%
Automatability0% × 15%
CISA SSVC: Track at low or medium mission impact; Track* at high (mission-essential systems).
Action: An upstream fix is merged but not yet in a tagged release. Restrict network exposure of the affected system or apply the vendor's mitigation within your standard update timelines until it ships, then apply the release.
EPSS PROB
0.2%
EPSS %ILE
6th
KEV
Not listed

CISA SSVCTrack at low or medium mission impact; Track* at high (mission-essential systems).

An upstream fix is merged but not yet in a tagged release. Restrict network exposure of the affected system or apply the vendor's mitigation within your standard update timelines until it ships, then apply the release.

Exploitation public PoC (CISA Vulnrichment) · Automatable no (CISA Vulnrichment) · Technical impact partial (CISA Vulnrichment). Mission impact is CISA's Mission & Well-being decision point, and only you can judge it: high means the affected system is essential to your organisation's mission, or its compromise could cause irreversible harm to people. CISA's decision table

Published

August 20, 2026

Last Modified

September 24, 2026

Advisory Details (8)

Auto-updated Aug 20, 2026
🔬 Proof of concept available. Upstream fix merged — awaiting tagged release. Sources: github_commit, github_pr.
generic🟡 PoC Available

Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections | Advisories | VulnCheck

https://www.vulncheck.com/advisories/lean-4-kernel-type-checking-bypass-via-mismatched-structure-projections
generic

GitHub - leanprover/lean4: Lean 4 programming language and theorem prover · GitHub

https://github.com/leanprover/lean4
generic🟡 PoC Available

oss-security - Lean 4 kernel soundness bug: forging proofs via nested inductive projections (0 = 1 demonstrated)

https://www.openwall.com/lists/oss-security/2026/08/02/1
generic

GitHub - xrchz/CollatzLean: Collatz conjecture in Lean · GitHub

https://github.com/xrchz/CollatzLean
generic

GitHub - endrazine/lean-cve-poc: Example of proving "0 = 1" using a vulnerability in the Lean 4 kernel. · GitHub

https://github.com/endrazine/lean-cve-poc
github_pr

fix: missing check at kernel inductive declaration

Fix merged in leanprover/lean4 PR #14577 on 2026-07-28 — awaiting tagged release

https://github.com/leanprover/lean4/pull/14577
github_commit

commit a39eab69e1ee (leanprover/lean4)

Fix landed in leanprover/lean4 commit a39eab69e1ee — awaiting tagged release

https://github.com/leanprover/lean4/commit/a39eab69e1eee9ad38f4efe507907b1026a77808
generic

Kernel accepts wrong-structure projections, allowing an axiom-free proof of False · Issue #14576 · leanprover/lean4 · GitHub

https://github.com/leanprover/lean4/issues/14576

Vendor Advisories for CVE-2026-72844(1)

These vendors published their own advisory mentioning this CVE — often with vendor-specific remediation steps + affected product lists not in NVD.

Weakness Classification(1)

MITRE Common Weakness Enumeration — the root-cause categories this CVE belongs to.

Data Freshness Timeline

(refreshed 17× in last 7d / 75× in last 30d)

Each row is a source pipeline that fetched or updated this CVE on that date, with what changed. For example, "NVD update" means NVD published or revised its analysis for this CVE; "MITRE cvelistV5" means we ingested or refreshed it from the CNA feed. Most recent first.

Showing the most recent 100 of 125 total refreshes for this CVE.

  1. 2026-10-05 01:50 UTCEG score recompute
  2. 2026-10-05 01:50 UTCGHSA enrichment
  3. 2026-10-04 23:22 UTCEPSS rescore
  4. 2026-10-04 03:30 UTCEG score recompute
  5. 2026-10-04 03:30 UTCGHSA enrichment
  6. 2026-10-03 14:26 UTCEPSS rescore
  7. 2026-10-03 05:09 UTCEG score recompute
  8. 2026-10-03 05:09 UTCGHSA enrichment
  9. 2026-10-02 06:49 UTCEG score recompute
  10. 2026-10-02 06:49 UTCGHSA enrichment
  11. 2026-10-01 19:50 UTCEPSS rescore
  12. 2026-10-01 06:34 UTCEG score recompute
  13. 2026-10-01 06:34 UTCGHSA enrichment
  14. 2026-09-30 08:14 UTCEG score recompute
  15. 2026-09-30 08:14 UTCGHSA enrichment
  16. 2026-09-28 23:42 UTCEG score recompute
  17. 2026-09-28 23:42 UTCGHSA enrichment
  18. 2026-09-28 13:52 UTCEPSS rescore
  19. 2026-09-28 01:22 UTCEG score recompute
  20. 2026-09-28 01:22 UTCGHSA enrichment
  21. 2026-09-27 13:48 UTCEPSS rescore
  22. 2026-09-27 03:02 UTCEG score recompute
  23. 2026-09-27 03:02 UTCGHSA enrichment
  24. 2026-09-26 15:59 UTCEPSS rescore
  25. 2026-09-24 21:21 UTCEG score recompute
Show 75 more
  1. 2026-09-24 21:21 UTCGHSA enrichment
  2. 2026-09-24 02:52 UTCEG score recompute
  3. 2026-09-24 02:52 UTCGHSA enrichment
  4. 2026-09-23 17:54 UTCEPSS rescore
  5. 2026-09-23 04:31 UTCEG score recompute
  6. 2026-09-23 04:31 UTCGHSA enrichment
  7. 2026-09-22 06:11 UTCEG score recompute
  8. 2026-09-22 06:11 UTCGHSA enrichment
  9. 2026-09-21 21:09 UTCEPSS rescore
  10. 2026-09-21 07:50 UTCEG score recompute
  11. 2026-09-21 07:50 UTCGHSA enrichment
  12. 2026-09-20 20:16 UTCEPSS rescore
  13. 2026-09-20 09:01 UTCEG score recompute
  14. 2026-09-20 09:01 UTCGHSA enrichment
  15. 2026-09-19 10:12 UTCEG score recompute
  16. 2026-09-19 10:12 UTCGHSA enrichment
  17. 2026-09-18 19:28 UTCEPSS rescore
  18. 2026-09-18 11:32 UTCEG score recompute
  19. 2026-09-18 11:31 UTCGHSA enrichment
  20. 2026-09-17 13:10 UTCGHSA enrichment
  21. 2026-09-16 14:29 UTCEG score recompute
  22. 2026-09-16 14:29 UTCGHSA enrichment
  23. 2026-09-16 14:08 UTCEPSS rescore
  24. 2026-09-16 05:15 UTCEPSS rescore
  25. 2026-09-15 15:13 UTCEG score recompute
  26. 2026-09-15 15:13 UTCGHSA enrichment
  27. 2026-09-15 03:12 UTCEPSS rescore
  28. 2026-09-14 16:36 UTCGHSA enrichment
  29. 2026-09-13 18:16 UTCEG score recompute
  30. 2026-09-13 18:16 UTCGHSA enrichment
  31. 2026-09-12 19:56 UTCEG score recompute
  32. 2026-09-12 19:56 UTCGHSA enrichment
  33. 2026-09-12 15:02 UTCEPSS rescore
  34. 2026-09-11 21:36 UTCEG score recompute
  35. 2026-09-11 21:36 UTCGHSA enrichment
  36. 2026-09-11 14:53 UTCEPSS rescore
  37. 2026-09-10 23:15 UTCEG score recompute
  38. 2026-09-10 23:15 UTCGHSA enrichment
  39. 2026-09-10 09:35 UTCEPSS rescore
  40. 2026-09-10 00:49 UTCGHSA enrichment
  41. 2026-09-09 01:57 UTCEG score recompute
  42. 2026-09-09 01:57 UTCGHSA enrichment
  43. 2026-09-08 22:01 UTCEPSS rescore
  44. 2026-09-07 18:54 UTCEG score recompute
  45. 2026-09-07 18:54 UTCGHSA enrichment
  46. 2026-09-06 20:34 UTCEG score recompute
  47. 2026-09-06 20:34 UTCGHSA enrichment
  48. 2026-09-06 13:48 UTCEPSS rescore
  49. 2026-09-05 22:13 UTCEG score recompute
  50. 2026-09-05 22:13 UTCGHSA enrichment
  51. 2026-09-04 23:51 UTCEG score recompute
  52. 2026-09-04 23:51 UTCGHSA enrichment
  53. 2026-09-04 05:07 UTCEPSS rescore
  54. 2026-09-04 00:05 UTCGHSA enrichment
  55. 2026-09-03 00:57 UTCEG score recompute
  56. 2026-09-03 00:57 UTCGHSA enrichment
  57. 2026-09-02 14:12 UTCEPSS rescore
  58. 2026-09-02 02:37 UTCEG score recompute
  59. 2026-09-02 02:37 UTCGHSA enrichment
  60. 2026-09-01 13:54 UTCEPSS rescore
  61. 2026-09-01 04:40 UTCEPSS rescore
  62. 2026-09-01 04:40 UTCEPSS rescore
  63. 2026-09-01 04:14 UTCGHSA enrichment
  64. 2026-08-31 05:54 UTCEG score recompute
  65. 2026-08-31 05:54 UTCGHSA enrichment
  66. 2026-08-30 19:18 UTCEPSS rescore
  67. 2026-08-30 19:17 UTCEPSS rescore
  68. 2026-08-30 07:34 UTCEG score recompute
  69. 2026-08-30 07:34 UTCGHSA enrichment
  70. 2026-08-30 01:22 UTCEPSS rescore
  71. 2026-08-29 09:14 UTCEG score recompute
  72. 2026-08-29 09:14 UTCGHSA enrichment
  73. 2026-08-28 21:42 UTCEPSS rescore
  74. 2026-08-28 10:51 UTCEG score recompute
  75. 2026-08-28 10:51 UTCGHSA enrichment

Publicly available exploits

(1 reference)

Working exploit code is in the public domain (1 GitHub PoC). Defenders should treat patch urgency accordingly — public PoCs typically lead to mass-exploitation within 24-72 hours.

  • GitHub PoCendrazine/lean-cve-poc
    First seen Aug 2, 2026

    CVE-2026-72844 : Example of proving "0 = 1" using a vulnerability in the Lean 4 kernel.

    Open source ↗

Related CVEs(same CWE)

Frequently asked(5)

What is CVE-2026-72844?
CVE-2026-72844 is a medium vulnerability published on August 20, 2026. 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…
When was CVE-2026-72844 disclosed?
CVE-2026-72844 was first published on August 20, 2026, with the most recent update on September 24, 2026. EchelonGraph re-ingests CVE updates from NVD on a 2-hour cycle, so this page reflects the latest published state.
Is CVE-2026-72844 actively exploited?
CVE-2026-72844 is not currently on CISA's Known Exploited Vulnerabilities catalog. FIRST EPSS estimates a 0.2% probability of exploitation in the next 30 days (6th percentile of EPSS-scored CVEs).
What is the CVSS score of CVE-2026-72844?
CVE-2026-72844 has a CVSS base score of 6.3 (a secondary CVSS source that NVD displays; NVD's own analysis pending).
How do I remediate CVE-2026-72844?
An upstream fix for CVE-2026-72844 has been merged but is not yet in a tagged release. Until it ships, restrict network exposure of the affected system or apply the vendor's mitigation, then update to the release that contains the fix. The vendor advisories EchelonGraph has for CVE-2026-72844 are linked in the Vendor Advisories panel on this page.

Dependency Blast Radius

Explore the affected products and dependency analysis for CVE-2026-72844

Explore →

Is Your Infrastructure Affected by CVE-2026-72844?

EchelonGraph automatically scans your cloud infrastructure and maps CVE exposure using blast radius analysis.

Book a Demo →Browse All CVEs