On October 15, Leonardo de Moura, the designer of Lean, published a post titled "Lean Now Ships with Verified Kernels." Starting with Lean v4.35.0, the toolchain can recheck your development with several independent kernels.

Why now? The first sentence answers it: "AI agents are very effective at finding vulnerabilities in our software. This includes the kernel (the proof checker) of the Lean proof assistant."

So apart from AI writing proofs well, AI is good at finding bugs in the checker itself. That flips the question: with which checker do you verify an AI-written proof?

Background

In Lean, the kernel is the final judge. If the kernel accepts a proof, the conclusion is mathematically true. So a bug in the kernel means a wrong proof can pass. That is a soundness problem.

[Lean's trust structure]

a user writes a proof
      |
  the kernel (proof checker)  <- a bug here lets a bad proof pass
      |
  "the theorem is true"

The problem: the kernel is itself software. It can have bugs.
And the thing that is good at finding those bugs is AI agents.

de Moura points to two recent postmortems on kernel soundness bugs (August 1 and August 24). And then this response.

What was added

The core of v4.35.0 is lake check.

[lake check]
- 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
- lake check --inadvisably-no-sandbox disables the sandbox
  (the flag name itself says "inadvisably")

[lake check --paranoid]
- rechecks with every kernel shipped with Lean
- additionally runs a variant of the official kernel built with
  a hardened memory allocator that turns memory corruption
  into a checked abort instead of a silently wrong answer

Four additional kernels ship with the distribution: nanoda, lean4lean, con-leche, and con-ron. Two of them are the interesting part of this story.

A kernel Claude implemented and proved consistent

The most striking item is con-leche. The post describes it directly:

con-leche
- the first kernel for Lean written in Lean
- a kernel proven consistent
- implemented and proven consistent by Claude (Fable and Opus)
- under heavy supervision by Joachim Breitner at the Lean FRO

What "consistent" means:
  every environment con-leche accepts
  has a model in set theory
  (following Mario Carneiro's model of Lean's type theory)

Performance: on the full Mathlib export,
  0.69x the instructions of the official kernel
  checks the whole library in about 100 seconds using eight threads

Why does this matter? con-leche eliminates a complete class of bugs: programming mistakes in the kernel implementation. The reason is a proof that whatever the kernel accepts has a model. And there is no performance penalty — it executes fewer instructions than the official kernel.

Distrusting the compiler too: con-ron

con-leche is still not bulletproof, because the compiler and runtime used to build it can have bugs. So comes the next step.

con-ron
- Joachim 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

The key argument:
- con-leche has a formal consistency proof
  -> any remaining soundness bugs are most likely in
     Lean's compiler or runtime (including the bignum library)
- it is very unlikely 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

So the trust chain grows one more link: not just "proof to kernel," but "kernel to the toolchain that built it." Verification of lean4lean is expected within a few months, which would bring the distribution to three verified kernels.

The risks and the scaling problem that remain

Balance matters here.

[Risks not fully eliminated]
- con-leche is not bulletproof; compiler/runtime bugs remain possible
  (which is why con-ron is used alongside it)
- multi-kernel checking does not remove every possibility of error
- "paranoid" mode costs more resources

[Scaling]
- Anthropic FLT         : over 13M LoC
- Mathlib               : 2.5M LoC
- Tau Ceti              : already over 3M LoC and growing fast
- General Courtade-Kumar: above 50M LoC
- the community is discussing 1B+ LoC math library proposals
-> the current external-kernel approach does not scale to this size
-> binary export formats and incremental checking are needed

de Moura is candid about the remaining work: a friendlier lake check, letting users hook their favorite kernel into it (the Lean Kernel Arena has new and efficient kernels), verifying parts of the compiler, and the scaling problem above.

Conclusion: make independent verification a habit

The briefing's action, turned into an experiment:

[Compare two commands in a Lean project]

1. Basic check
   [ ] lake check
       -> rechecks with the official kernel (leanchecker) in a sandbox

2. Multi-kernel check
   [ ] lake check --paranoid
       -> rechecks with every shipped kernel, plus the hardened-allocator variant

3. What to compare
   [ ] checking time and resource use
   [ ] whether any proof makes the kernels disagree
   [ ] if so, report it to Lean FRO ([email protected])

4. Set a team rule
   [ ] attach --paranoid results to PRs for critical proofs
   [ ] keep basic checks for the rest to control cost

One line captures it.

Instead of trusting what AI produces,
recheck it along several independent paths.

The principle is not limited to mathematical proofs. Wherever AI writes code, documents, or makes decisions, the same question remains: what do we verify this with, and along how many independent paths? Lean 4.35 shows how the most rigorous field answers it. In an age where AI finds bugs in our verification tools, verification itself has to be multiplied.

Further reading

References

Go deeper with a course

The habit of verifying AI output independently is a matter of judgment and decision-making. Designing when a human steps in over an automated judgment, and how to verify it, becomes concrete when you work with Decision AI and human-in-the-loop patterns.