Leanは、数学者やコンピュータ科学者が複雑な論理的証明を記述および検証するために使用するソフトウェアツールである証明アシスタントです。その核心には、証明の妥当性を判断する基礎的なコードである「カーネル」があります。これらのカーネルはシステム全体の完全性にとって極めて重要であるため、カーネルの実装におけるいかなるバグも、誤った証明を真として受け入れられる原因となる可能性があります。Lean FROの共同創設者であるLeonardo de Mouraは、このようなソフトウェアにおける脆弱性を特定するAIエージェントの有効性が高まっていることに対応するため、Lean v4.35.0にいくつかの新しいカーネルが含まれていることを発表しました。
Leonardo de MouraはLean FROの共同創設者であり、これらのセキュリティアップデートを発表した主要な人物です。
主な追加機能の一つは、Lean自身で記述され、一貫性が証明された最初のカーネルである「con-leche」です。この文脈における一貫性とは、カーネルが受け入れるすべての環境が、集合論において対応するモデルを持つことを意味します。検証対象となる言語自体で記述されたカーネルを使用することで、開発者はカーネルの実装におけるプログラミングミスによって引き起こされる一連のバグを排除することを目指しています。ソフトウェアの構築に使用されるコンパイラや実行環境からのリスクをさらに軽減するため、チームは「con-ron」も導入しました。このカーネルは、AIを使用してcon-lecheのロジックをRustに翻訳し、その後、Rustコードがチェックアルゴリズムを洗練していることを証明するツールであるAeneasを使用して検証されたものです。証明をcon-lecheとcon-ronの両方に対してチェックすることで、ユーザーは一方の環境には存在するが他方には存在しない可能性のあるバグに対して、高いレベルの保護を得ることができます。
これらの検証済みカーネルは大幅なセキュリティの向上を提供しますが、Leanチームはスケーラビリティが依然として課題であることを認めています。コミュニティが成長し、Mathlibのようなライブラリが数百万行のコードへと拡大するにつれ、外部カーネルを使用して開発を再チェックする現在の手法は非効率になる可能性があります。チームは現在、1億行を超えるような大規模な開発を処理するために、バイナリエクスポート形式やインクリメンタルチェックを検討しています。それまでの間、ユーザーは新しい `lake check --paranoid` コマンドを利用できます。このコマンドは、強化されたメモリアロケータで構築された公式カーネルのバリアントを実行し、潜在的なメモリ破損をサイレントなエラーではなく、チェックされたアボート（中断）に変換します。