Description

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.

Executive Summary

Technical Details

Mitigations

References

Additional Metadata

{
  "score": "6.3",
  "pubDate": "2026-08-20T18:16:45.290Z",
  "pubdate": "2026-08-20T18:16:45.290Z",
  "executiveSummary": "This vulnerability is a type confusion flaw within the Lean 4 kernel, specifically affecting the type-checking and inductive type registration logic. The primary impact is the generation of an ungrounded proof of False carrying no axioms, effectively compromising the logical soundness of the proof assistant and allowing the derivation of any arbitrary proposition.\nThe affected product is Lean 4, specifically involving the kernel components responsible for processing projections and inductive types. The risk implications are severe for environments relying on formal verification, as core logical guarantees can be entirely bypassed.\nAttacker capabilities require the execution of an in-process metaprogram, such as building a malicious project or importing an untrusted Lake dependency. Exploitation does not require bypass flags like sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or modified .olean files, operating strictly through standard kernel-checked pathways.",
  "technicalDetails": "The vulnerability stems from two core weaknesses in the Lean 4 kernel: first, the kernel projection logic fails to verify that the structure named in a projection expression matches the type of the value being projected. Second, environment::add_inductive in src/kernel/inductive.cpp fails to type-check nested inductive applications that are replaced by auxiliary types, allowing parametric arguments to bypass validation.\nExploitation proceeds via an in-process metaprogram that registers an ill-typed nested inductive. Within this construct, a constructor applies a .proj C 0 projection to a value of an unrelated type W. Because the structural validation is missing, the kernel admits the malformed declaration through the standard checked addDecl path at maximum kernel checking settings.\nThe published proof of concept utilizes an expression-padding technique where two expressions are padded until their cryptographic hashes and approximate depths collide. This technique specifically defeats kernel memoization and caching mechanisms, forcing the kernel to re-evaluate expressions and reach the underlying flaw, though hashing collisions represent the trigger mechanism rather than the root cause.\nThe resulting state is a severe type confusion vulnerability. By circumventing type constraints during inductive type elaboration and projection evaluation, the system accepts unsound definitions that produce a proof of False with zero axioms. Consequently, any false proposition can be derived, breaking the fundamental correctness guarantees of the Lean 4 theorem prover."
}