Leanが検証済みカーネルを標準搭載、AIによる脆弱性発見に対抗
Lean Now Ships with Verified Kernels
Lean v4.35.0では`lake check`コマンドが追加され、開発内容をサンドボックス内で公式カーネルのleancheckerにより再検査できる。さらにnanoda、lean4lean、con-leche、con-ronの4つの追加カーネルが同梱され、`lake check --paranoid`で全てによる再検査が可能。ClaudeがJoachim Breitnerの監督下で実装・一貫性証明したcon-lecheは、カーネル実装のプログラミングミスというバグのクラスを性能低下なしに排除する。
con-lecheはLeanで書かれ、一貫性が証明された最初のLean用カーネルである。