---
title: "Lean Now Ships with Verified Kernels"
slug: lean-now-ships-with-verified-kernels
url: https://listedarticles.com/articles/lean-now-ships-with-verified-kernels
canonical_url: https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/
content_type: announcement
language: en
published_at: 2026-10-15T00:00:00.000Z
updated_at: 2026-10-18T02:12:33.449Z
author: "Leonardo de Moura"
author_url: https://leodemoura.github.io/
authored_by: human
publisher: "Leonardo de Moura"
publisher_url: https://leodemoura.github.io/
topics: ["Formal Verification", "Lean", "Mathematics", "Security", "Programming Languages"]
license: all-rights-reserved
word_count: 708
reading_minutes: 3
citation: "Leonardo de Moura, Leonardo de Moura. \"Lean Now Ships with Verified Kernels.\" 15 Oct 2026. https://leodemoura.github.io/blog/2026-10-15-lean-now-ships-with-verified-kernels/ (all-rights-reserved)"
# The full text follows. The web page shows an extract and sends readers
# to the source above; quote the citation and link the canonical URL.
---

# Lean Now Ships with Verified Kernels

> Leonardo de Moura explains how Lean v4.35 hardens proof checking after AI-found kernel soundness bugs: a sandboxed `lake check` that rechecks developments with the official kernel, four additional independent kernels, and the scaling challenges ahead for multi-million-line proof libraries.

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](https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/), [August 24](https://leodemoura.github.io/blog/2026-8-24-postmortem-for-the-kernel-soundness-bug-hunt/)). 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](https://github.com/leanprover/lean4/releases/tag/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](https://github.com/ammkrn/nanoda_lib), [lean4lean](https://github.com/digama0/lean4lean), [con-leche](https://github.com/leanprover/con-leche), and [con-ron](https://github.com/leanprover/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](https://www.joachim-breitner.de/) at the [Lean FRO](https://lean-lang.org/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](https://leanprover.github.io/con-leche/con-leche-proof-idea.html). 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](https://github.com/leanprover/con-leche/blob/master/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](https://github.com/AeneasVerif/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](https://arthur-adjedj.github.io/) is working on the kernel renovation plan (see issue [#14977](https://github.com/leanprover/lean4/issues/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](https://arena.lean-lang.org/) 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](https://www.anthropic.com/research/formalizing-fermats-last-theorem) is over 13M LoC, [Mathlib](https://github.com/leanprover-community/mathlib4) is 2.5M LoC, and [Tau Ceti](https://taucetiproject.org/) is already over 3M LoC and growing fast. [The General Courtade–Kumar theorem](https://github.com/dpwoodru/general-courtade-kumar-lean) 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.