leanprover

Records3All Threatist records

Exploited (KEV)0None in CISA KEV

CVSS critical0CVSS 9.0–10.0

CVSS high0CVSS 7.0–8.9

Exploited now

leanprover records in CISA KEV

No leanprover vulnerabilities are listed in CISA KEV.

Records

3 records

TI-2026-51070 CVE-2026-72844 · GHSA-4fhc-8rq3-cjvg

Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections

MEDIUM 63

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 neste…

CVSS 4.0MEDIUM 6.8 Local No auth User interaction EPSS 0.00187 Published 2026-08-20 Fixed in 4.32.2 CWE-843

TI-2026-50947 CVE-2026-72711 · GHSA-fhmq-xvc2-q54h

Lean 4 before 4.32.2 Kernel Accepts Opaque Declaration With an Unbound Free Variable

MEDIUM 63

The Lean 4 kernel does not check that the body of an opaque declaration is closed.

CVSS 4.0MEDIUM 6.8 Local No auth User interaction EPSS 0.00176 Published 2026-08-24 Fixed in 4.32.2 CWE-20

TI-2026-25224 CVE-2026-32732 · GHSA-6ggm-pwr9-r5h2

XSS in @leanprover/unicode-input-component

LOW 3

Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant.

CVSS 4.0N/A 0.0 Network No auth User interaction EPSS 0.00318 Published 2026-03-13 Fixed in 0.2.0 CWE-80

Open these records in search →

Critical	0
High	0
Medium	2
Low	0
No CVSS	1