Lean Now Ships with Verified Kernels

AI-driven exploits exposed vulnerabilities in Lean's kernel, so the official distribution now includes tools and alternative kernels to detect and mitigate kernel unsoundness. Lean v4.35.0 adds lake check, which exports a development and rechecks it with leanchecker inside a sandbox (sandbox optional). The distribution also ships four additional kernels - nanoda, lean4lean, con-leche, and con-ron - and a paranoid mode runs all of them plus a variant of the official kernel built with a hardened memory allocator to convert memory corruption into checked aborts. These additions let users recheck projects across multiple independent checkers to catch divergences early.

Con-leche is the first kernel implemented in Lean and proven consistent against a set-theoretic model of Lean's type theory; its proof was produced with AI assistance under human supervision and is machine-checked by the official kernel. Con-leche matches or outperforms the official kernel on Mathlib (0.69x instructions, ~100s on eight threads). To reduce compiler/runtime risk, con-leche was translated to Rust and verified by Aeneas to produce con-ron, so checking with both targets makes identical bugs across runtimes unlikely. Ongoing work includes verifying lean4lean, a kernel renovation plan, easier lake check UX, compiler verification, and scalability improvements (binary export, incremental external checking) to handle huge repositories. Users are encouraged to run lake check paranoid and report any kernel disagreements.