6.8 MEDIUM
- CVSS version (CVSS): 4.0
- Attack Vector (AV): Local (L)
- Attack Complexity (AC): Low (L)
- Attack Requirement (AT): None (N)
- Privileges Required (PR): None (N)
- User Interaction (UI): Passive (P)
- Vulnerable System Impact Confidentiality (VC): None (N)
- Vulnerable System Impact Integrity (VI): High (H)
- Vulnerable System Impact Availability (VA): None (N)
- Subsequent System Impact Confidentiality (SC): None (N)
- Subsequent System Impact Integrity (SI): None (N)
- Subsequent System Impact Availability (SA): None (N)
- Modified Attack Vector (MAV): Local (L)
- Modified Attack Complexity (MAC): Low (L)
- Modified Attack Requirement (MAT): None (N)
- Modified Privileges Required (MPR): None (N)
- Modified User Interaction (MUI): Passive (P)
- Modified Vulnerable System Impact Confidentiality (MVC): None (N)
- Modified Vulnerable System Impact Integrity (MVI): High (H)
- Modified Vulnerable System Impact Availability (MVA): None (N)
- Modified Subsequent System Impact Confidentiality (MSC): Negligible (N)
- Modified Subsequent System Impact Integrity (MSI): Negligible (N)
- Modified Subsequent System Impact Availability (MSA): Negligible (N)
- Safety (S): Not Defined (X)
- Automatable (AU): Not Defined (X)
- Recovery (R): Not Defined (X)
- Value Density (V): Not Defined (X)
- Vulnerability Response Effort (RE): Not Defined (X)
- Provider Urgency (U): Not Defined (X)
- Confidentiality Req. (CR): Not Defined (X)
- Integrity Req. (IR): Not Defined (X)
- Availability Req. (AR): Not Defined (X)
- Exploit Maturity (E): Not Defined (X)
Activity log
- Created suggestion
Lean 4 Kernel Type Checking Bypass via Mismatched Structure Projections
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.
References
-
GitHub Issue #14576 issue-tracking
-
GitHub Pull Request #14577 issue-tracking
-
lean-cve-poc exploit
-
CollatzLean exploit
-
oss-security: Lean 4 kernel soundness bug third-party-advisory
Affected products
- <4.32.2
- ==4.32.2
- ==4.33.0-rc1
Matching in nixpkgs
pkgs.lean4
Automatic and interactive theorem prover
pkgs.leanPackages.Qq
Lean 4 compile-time quote and antiquote macros for metaprogramming
pkgs.leanPackages.Cli
Command-line argument parser for Lean 4
pkgs.leanPackages.aesop
White-box automation for Lean 4
pkgs.leanPackages.lean4
Automatic and interactive theorem prover
pkgs.leanPackages.mathlib
None
-
nixos-26.05 -
- nixos-26.05-small 4.29.0
pkgs.leanPackages.batteries
The batteries-included extended library for Lean 4
-
nixos-unstable -
- nixos-unstable-small 4.30.0-unstable-2026-05-26
-
nixos-26.05 -
- nixos-26.05-small 4.29.0
pkgs.leanPackages.plausible
Property-based testing framework for Lean 4
-
nixos-unstable -
- nixos-unstable-small 4.30.0-unstable-2026-05-26
-
nixos-26.05 -
- nixos-26.05-small 4.29.0
pkgs.leanPackages.importGraph
Tools to analyse and visualise Lean 4 import structures
-
nixos-unstable -
- nixos-unstable-small 4.30.0-unstable-2026-05-26
-
nixos-26.05 -
- nixos-26.05-small 4.29.0
pkgs.leanPackages.LeanSearchClient
Lean 4 client for LeanSearch and Moogle proof search
-
nixos-unstable -
- nixos-unstable-small 4.12.0-unstable-2026-02-12
-
nixos-26.05 -
- nixos-26.05-small 0-unstable-2026-02-12
pkgs.leanPackages.mathlib__archive
Mathematical library for Lean 4
-
nixos-unstable -
- nixos-unstable-small 4.30.0
pkgs.vscode-extensions.leanprover.lean4
This extension provides VS Code support for the Lean 4 theorem prover and programming language
Package maintainers
-
@jthulhu Adrien Mathieu <adrien.lc.mathieu@gmail.com>
-
@Coda-Coda Daniel Britten <nixpkgs@danielb.space>
-
@nadja-y Nadja Yang <nadja@njy.dev>
-
@xhalo32 Niklas Halonen <niklas.2.halonen@aalto.fi>
-
@alexstaeding Alexander Städing <alex@staeding.com>