Kiranandcode

**Name of the Vulnerable Software and Affected Versions** Lean 4 (affected versions not specified) **Description** The kernel fails to verify that the structure named in a projection expression matches the type of the value being projected. Additionally, the `environment::add inductive` function in `src/kernel/inductive.cpp` does not type check nested inductive applications replaced by auxiliary types, allowing parametric arguments to bypass checking. A metaprogram running in-process, such as through a malicious Lake dependency or during project builds, can register an ill-typed nested inductive. This is achieved by applying a `.proj C 0` projection to a value of an unrelated type `W`. This leads to type confusion, enabling a proof of False from which any proposition can be derived. The issue can be triggered by padding expressions to cause hash and depth collisions, which bypasses kernel caching. **Recommendations** At the moment, there is no information about a newer version that contains a fix for this vulnerability.