Lean4
Monthly
Type confusion in the Lean 4 proof assistant kernel allows a malicious metaprogram to produce a proof of False carrying no axioms, from which any proposition can be derived, completely breaking kernel soundness. The vulnerability arises from two related defects in src/kernel/inductive.cpp: projection expressions do not verify that the named structure matches the projected value's type, and environment::add_inductive fails to type-check the parametric arguments of nested inductive applications after they are replaced by auxiliary types, letting those arguments escape kernel verification entirely - exploitable through the normal maximum-kernel-checking addDecl path without sorry, unsafeCast, or unsafe annotations. Publicly available exploit code exists at multiple repositories; this CVE is not listed in CISA KEV.
Type confusion in the Lean 4 proof assistant kernel allows a malicious metaprogram to produce a proof of False carrying no axioms, from which any proposition can be derived, completely breaking kernel soundness. The vulnerability arises from two related defects in src/kernel/inductive.cpp: projection expressions do not verify that the named structure matches the projected value's type, and environment::add_inductive fails to type-check the parametric arguments of nested inductive applications after they are replaced by auxiliary types, letting those arguments escape kernel verification entirely - exploitable through the normal maximum-kernel-checking addDecl path without sorry, unsafeCast, or unsafe annotations. Publicly available exploit code exists at multiple repositories; this CVE is not listed in CISA KEV.