コードにバグあり？Lean4 が証明する：エンジニア向け形式検証

コードにバグあり？Lean4 が証明する：生成 AI 時代における「絶対的な正しさ」の追求

生成 AI がコードを大量に生み出す現在、従来のテストや LLM による評価では「すべての入力」に対する正しさを保証できません。これに対し、数学的証明によって仕様と実装の整合性を保証する「形式検証（Formal Verification）」が、ソフトウェアの信頼性を根本から高める鍵となります。

テストや AI 評価の限界：なぜ「確率的」では不十分なのか

現在、ビルダーは週に数百ものプルリクエストを生成しています。その正しさをどう保証するか？LLM をジャッジとして使う方法は確率的（probabilistic）であり、テストも一部の入力しかチェックできません。人間のコードレビューに至っては、AI エージェントのスピードには追いつきません。

「これらすべてが、『すべての入力に対してコードが正しい』と言えるわけではありません。」

形式検証は、この課題を解決します。これは数学的な証明を行い、すべての可能な入力に対してコードが仕様を満たすことを保証する手法です。

人間と AI の役割分担：仕様の「人間所有」モデル

形式検証を実践するための重要なアプローチとして、「バックドブン開発（Back-driven development）」が提案されています。このプロセスでは、役割を明確に分割します。

1. 人間が仕様（Specification）を所有する：何が正しいかを定義します。これは Lean 言語で直接記述するか、自然言語で書いて AI に形式化させます。
2. AI が実装と証明を生成する：定義された仕様に基づき、コードを実装し、その正しさを証明する論理を構築します。

ここで重要なのは、仕様こそが「生きているアーティファクト」であり、人間が最終的に検証・承認する必要がある点です。仕様は上流（upstream）に位置するため、ここが間違っていればすべてが崩壊します。AI は下流（downstream）の実装と証明の生成に集中し、人間は「何が正しいか」という本質的な定義を担当します。

Lean4 の仕組み：小さな信頼済みカーネルによる絶対的保証

形式検証の中心を担うのが、プログラミング言語であり証明支援系でもある Lean です。その最大の特徴は、定義（コード）と証明（定理）を同じ言語で記述できる点にあります。翻訳レイヤーが存在しないため、複雑な証明も一貫して扱えます。

小さな信頼済みカーネルの力

Lean のアーキテクチャには「小さな信頼済みカーネル（small trusted kernel）」という仕組みがあります。これは、すべての証明が最終的に通る唯一のチェックポイントです。

「あなたが信じる必要があるのは、この小さなカーネルだけです。」

複雑な証明プロセスは、チェスに例えられます。プレイヤー（ユーザーや AI）は「タクティクス（戦術）」という駒を動かし、ゴール（定理の証明）を目指して盤面を進みます。途中で詰みそうな場合はバックトラックして別の道を探ります。しかし、最終的に盤面が整ったとしても、それが正しいかどうかは、独立した小さなカーネルが厳密にチェックします。

もし証明に誤りがあれば、このカーネルが即座に拒否します。また、このカーネル自体もオープンソースであり、C++ や Rust などで独自の実装をすることも可能です。これにより、特定の言語やツールへの依存を避け、多角的な検証が可能になります。

実世界での実践：既存コードとの統合事例

形式検証は理論だけでなく、実際の開発現場でも活用されています。

Zlib の Lean 変換：AI が証明を生成する例

Andreio AI は、C 言語の圧縮ライブラリ「Zlib」を Lean に変換し、その正しさを証明しました。このプロジェクトでは、自然言語で記された仕様（「圧縮したデータを復元すれば元のデータに戻る」）から AI が形式仕様を生成し、さらに AI がコードを実装して 32,000 行に及ぶ証明論理を構築しました。

AI は問題を小さなサブゴール（補助定理）に分解し、それぞれをタクティクスで解決。最後にカーネルがこれを検証することで、完全な正しさを保証しています。

Rust と Lean の連携：AWS Cedar の事例

既存の Rust コードを形式検証する際にも、Lean を活用できます。AWS が提供する認可ポリシー言語「Cedar」がその好例です。

Cedar の仕様は Lean で記述され、実際のプロダクションコードは Rust で動作します。両者は「差分テスト（differential random testing）」によって検証されます。つまり、同じ入力に対して Lean の仕様モデルと Rust の実装コードが同じ出力を返すかを 1 億回以上ランダムにテストし、 nightly に実行しています。

「この条件を満たさないバージョンは決してリリースされません。」

Solvers と Verus：静的チェックによる効率化

さらに、Solvers（ソルバー）と呼ばれる強力な計算機を活用する手法もあります。Verus は Rust 用の形式検証ツールで、Z3 というソルバーを使用します。

コードに requires（事前条件）や ensures（事後条件）といった注釈を追加し、静的解析によって正しさをチェックします。これは実行時に消去される「ゴーストコード」として機能するため、パフォーマンスへの影響はありません。

未来の標準：Strata が拓く多言語環境

「すべてのプログラミング言語で形式検証を行いたい」という要望に応えるため、AWS はオープンソースツール Strata を開発中です。これは、任意の言語を Lean の中間表現に変換するコンパイラのような役割を果たします。

Strata は高レベルな中間表現から低レベルな「Strata Core」へと落とし込み、これを Lean 証明支援系や SMT ソルバー、モデルチェッカーなどのエンジンに配信します。これにより、特定の言語に縛られず、あらゆる環境で形式検証を適用することが可能になります。

まとめ：確率的正しさから絶対的正しさへ

生成 AI の時代において、コードの信頼性を高めるには「おそらく正しい」状態から脱却し、「数学的に証明された正しい」状態を目指す必要があります。Lean4 や Strata といったツール群は、そのための具体的な道筋を示しています。

「この新しい世界では、ソフトウェアやシステムが『おそらく正しい』のではなく、『絶対的に正しい』ものになることを目指しましょう。」

今日からでもブラウザ上の Lean で仕様を書き始め、AI に実装と証明を任せることで、より堅牢なソフトウェア開発への第一歩を踏み出すことができます。