Lean Now Ships with Verified Kernels

AI agents are very effective at finding vulnerabilities in our software. This includes the kernel (the proof checker) of the Lean proof assistant. See our two recent postmortems (August 1, August 24). We are strengthening the official kernel, adding new kernels, and building new tools that simplify rechecking your Lean developments with external kernels. Lean v4.35.0 comes with the lake check command. This command exports your development and rechecks it with leanchecker, the official Lean kernel without all the baggage around it. The whole process runs inside a sandbox. You can disable the sandbox using lake check --inadvisably-no-sandbox. Lean now ships with four additional kernels: nanoda, lean4lean, con-leche, and con-ron. You can recheck your development with all of them using the command lake check --paranoid. In this mode, we also run a variant of the official kernel built with a hardened memory allocator, which turns memory corruption into a checked abort instead of a silently wrong answer.

Con-leche is the first kernel for Lean written in Lean and proven consistent. It was implemented and proven consistent by Claude (Fable and Opus), under heavy supervision by Joachim Breitner at the Lean FRO. "Consistent" here means that every environment con-leche accepts has a model in set theory, following Mario Carneiro's model of Lean's type theory. The proof idea is written up here. The proof itself is checked by the official Lean kernel, and it assumes the consistency of the set theory used in the model. This approach eliminates a complete class of bugs: programming mistakes in the kernel implementation. It does so without a performance penalty. On the full Mathlib export, con-leche executes 0.69x the instructions of the official kernel and checks the whole library in about 100 seconds using eight threads (see PERF.md).

However, con-leche is not bulletproof, because there might be bugs in the compiler and runtime used to build it. To minimize this kind of risk, Joachim used AI to translate con-leche to Rust and then used Aeneas to prove that the Rust version refines con-leche's checking algorithm. Aeneas is a tool for verifying Rust code using Lean. This kernel is called con-ron. The key point is that, since con-leche has a formal consistency proof, any remaining unsoundness bugs are most likely in Lean's compiler or runtime (including the bignum library). It is very unlikely that the same bug also exists in the Rust compiler or runtime, so by checking a proof with both con-leche and con-ron, you gain a high level of protection against this class of bugs.

We also expect the verification of lean4lean to be completed in the next few months, and then we will have three verified kernels in our distribution. The lean4lean verification is also important because its implementation follows the official C++ kernel implementation very closely.

Arthur Adjedj is working on the kernel renovation plan (see issue #14977). Arthur has already submitted several PRs implementing the plan. Joachim is reviewing them, making sure con-leche implements the same changes, and patching its proof to ensure no new holes are introduced during the renovation. Arthur is also working on even simpler kernels for Lean. The goal is to reduce their complexity and simplify the process of validating their specification.

There is still a lot of work to be done. We want a more user-friendly lake check command. We want to enable users to hook their favorite kernel into lake check. The Lean Kernel Arena has several new and efficient kernels. It should be easy to use them. We want to verify parts of our compiler. Scalability is also a major concern now. Anthropic's FLT is over 13M LoC, Mathlib is 2.5M LoC, and Tau Ceti is already over 3M LoC and growing fast. The General Courtade–Kumar theorem repo is above 50M LoC. We are seeing the Lean community write proposals for math libraries in the 1B+ LoC range. The current approach for external kernels does not scale to developments of this size. We need binary export formats and incremental checking with external checkers. At the Lean FRO, we are working on these challenges. In the meantime, run lake check --paranoid on your own project. If the kernels disagree about one of your proofs, we want to hear about it at contact@lean-fro.org.