leanprover has 2 CVEs on record. 2 were published in the last 90 days. The median CVSS is 6.3 (medium).
CVEs per month
Last 12 months, by publish date
1225/120126/010226/020326/030426/040526/050626/060726/070826/080926/091026/101126/11
- Exploited share
- 0% vs 1% corpus
- Median CVSS
- 6.3
- Publish → KEV
- —
- Last 90 days
- 2 prev 0
2
Total CVEs
0
Critical
0
CISA KEV
0
Exploited
Worst active — by depth score
CVE-2026-72711Medium· 6.3The Lean 4 kernel does not check that the body of an opaque declaration is closed47CVE-2026-72844Medium· 6.3The 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 appli…47
leanprover vulnerabilities
CVEs affecting leanprover, newest first. Open any entry for full detail, references, and exploit status.
2 CVEsRSS
CVE-2026-72711Medium· 6.3PoCThe Lean 4 kernel does not check that the body of an opaque declaration is closed
The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that …
▾ Twilightleanprover · lean4EPSS 0.18%via NVD
CVE-2026-72844Medium· 6.3PoCThe 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 appli…
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 appli…
▾ Twilightleanprover · lean4EPSS 0.19%via NVD