Lean v4.35.0 ships lake check and four extra proof-checking kernels

A post on the Lean blog announces that Lean now ships with verified kernels. It opens with the motivation: AI agents are very effective at finding vulnerabilities in software, and that includes the Lean kernel, the proof checker. The post points to two recent postmortems (August 1 and August 24). In response, the Lean team says it is strengthening the official kernel, adding new kernels, and building tools that make it easier to recheck Lean developments with external kernels.

The first tool is the lake check command in Lean v4.35.0. It exports your development and rechecks it with leanchecker, which the post describes as the official Lean kernel without all the baggage around it. The whole process runs inside a sandbox, which can be turned off with lake check --inadvisably-no-sandbox. Lean also now ships with four additional kernels: nanoda, lean4lean, con-leche and con-ron. Running lake check --paranoid rechecks a development with all of them. In that mode it also runs 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 described as 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 itself is checked by the official Lean kernel, and it assumes the consistency of the set theory used in the model. According to the post, this eliminates a whole class of bugs, namely programming mistakes in the kernel implementation, and 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.

Con-leche is not bulletproof, the post says, because the compiler and runtime used to build it may have bugs. To reduce that risk, Joachim Breitner used AI to translate con-leche to Rust, then used Aeneas, a tool for verifying Rust code using Lean, to prove that the Rust version refines con-leche's checking algorithm. That kernel is con-ron. The reasoning: 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 checking a proof with both con-leche and con-ron gives a high level of protection against this class of bugs.

The team also expects verification of lean4lean to be completed in the next few months. Then the distribution would have three verified kernels. That verification matters additionally because lean4lean's implementation follows the official C++ kernel implementation very closely.

On the official kernel itself, Arthur Adjedj is working on the kernel renovation plan (issue #14977) and has submitted several PRs. Joachim Breitner reviews them, makes sure con-leche implements the same changes, and patches its proof so no new holes appear during the renovation. Adjedj is also working on even simpler kernels, aiming to reduce their complexity and make their specifications easier to validate.

The post closes with a to-do list: a more user-friendly lake check, a way for users to hook their favorite kernel into it (the Lean Kernel Arena has several new and efficient kernels that should be easy to use), and verification of parts of the compiler. Scalability is the big concern. The post cites Anthropic's FLT at over 13M lines of code, Mathlib at 2.5M, Tau Ceti at over 3M and growing fast, and the General Courtade-Kumar theorem repo at above 50M, with community proposals for math libraries in the 1B+ range. The current approach for external kernels does not scale to developments of that size; binary export formats and incremental checking with external checkers are needed. Meanwhile, the Lean FRO asks users to run lake check --paranoid on their own projects and to write to contact@lean-fro.org if the kernels disagree about one of their proofs.

Key facts

• Lean v4.35.0 adds lake check, which exports a development and rechecks it with leanchecker, the official kernel without the surrounding baggage, inside a sandbox.
• Lean now ships four additional kernels (nanoda, lean4lean, con-leche, con-ron); lake check --paranoid runs a project through all of them plus an official-kernel variant built with a hardened memory allocator.
• Con-leche is the first Lean kernel written in Lean and proven consistent, implemented by Claude (Fable and Opus) under heavy supervision by Joachim Breitner at the Lean FRO; on the full Mathlib export it executes 0.69x the official kernel's instructions and takes about 100 seconds on eight threads.
• Con-ron is a Rust translation of con-leche, with a proof via Aeneas that it refines con-leche's algorithm, so a bug in Lean's compiler or runtime is unlikely to be mirrored in it.
• The team says external kernel checking does not scale to libraries of 13M to 50M+ lines of code and that binary export formats and incremental checking are needed.

Why it matters

The post starts from the premise that AI agents are very effective at finding vulnerabilities in software, including the Lean kernel, which is the component that decides whether a proof is accepted. Two recent postmortems on the subject are linked. A proof assistant is only as trustworthy as its checker, so the response is layered: a hardened official kernel, several independent kernels, and one kernel (con-leche) whose consistency is itself proven in Lean. The claim is that this removes a whole class of bugs, programming mistakes in the kernel implementation, without slowing checking down.

Who it affects

Anyone with a Lean development, since lake check works on your own project. The scale figures in the post show who is stretched hardest: Anthropic's FLT development at over 13M lines of code, Mathlib at 2.5M, Tau Ceti at over 3M and growing fast, and the General Courtade-Kumar theorem repo above 50M. Lean community proposals reach the 1B+ range. The Lean FRO team, Joachim Breitner and Arthur Adjedj in particular, carries the kernel renovation and proof maintenance work.

How to use it

Update to Lean v4.35.0 and run lake check to export your development and recheck it with leanchecker in a sandbox. The sandbox can be disabled with lake check --inadvisably-no-sandbox, though the flag's name advises against it. For the strongest check, run lake check --paranoid, which adds nanoda, lean4lean, con-leche and con-ron, plus a variant of the official kernel built with a hardened memory allocator. If the kernels disagree about one of your proofs, the Lean FRO asks you to write to contact@lean-fro.org.

How solid is it

This is the Lean team's own announcement, so the claims are the maintainers' account of their work. The concrete performance figures are for con-leche only: 0.69x the official kernel's instructions on the full Mathlib export, about 100 seconds for the whole library on eight threads, with a PERF.md linked as the reference. No benchmark numbers are given for nanoda, lean4lean or con-ron. The consistency proof for con-leche is checked by the official Lean kernel, and the post says the proof idea is written up separately.

Risks and caveats

The post itself lists the limits. The consistency proof assumes the consistency of the set theory used in the model. Con-leche is not bulletproof, because bugs may exist in the compiler and runtime used to build it, including the bignum library; con-ron exists to cover that, and the protection claimed is a high level, not an absolute one. Lean4lean's verification is expected in the next few months and is not yet done, so three verified kernels is a goal for now. The current approach for external kernels does not scale to the largest developments, lake check still needs to be more user-friendly, custom kernels cannot yet be hooked in, and parts of the compiler remain unverified. No timescale is given for these.

“AI agents are very effective at finding vulnerabilities in our software.”

— Lean blog post, "Lean Now Ships with Verified Kernels"