lean4 vulnerabilities
CVEs whose affected-version data names the lean4 package. Each record lists the affected and patched versions; check a specific version with the dependency checker or POST /api/sbom.
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