Lean now ships with four extra kernels, one proven consistent by Claude
Lean Now Ships with Verified Kernels
AI agents keep finding soundness bugs in Lean's proof checker, so Lean v4.35.0 adds a `lake check` command that rechecks your development in a sandbox against the official kernel, plus four more kernels via `lake check --paranoid`. Con-leche, written in Lean and proven consistent by Claude under Joachim Breitner's supervision, runs at 0.69x the instruction count of the official kernel; con-ron is its Aeneas-verified Rust port.
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).