Isabelle/HOL: Nitro Isolation Engine を支える定理証明支援系

本ブログは 2026 年 4 月 17 日に公開された Amazon Science Blog “Isabelle/HOL: The proof assistant behind the Nitro Isolation Engine” を翻訳したものです。

Isabelle/HOL は、数学的な記述の表現力、自動化、スケーラビリティのバランスによって、世界初の形式的に検証されたクラウドハイパーバイザーを実現しました。

2025 年の Amazon re:Invent カンファレンスにおいて、Amazon Web Services (AWS) は Nitro Isolation Engine (NIE) を発表しました。NIE は、お客様のデータのセキュリティを確保しながら AWS のお客様にリソースを提供する役割を担うソフトウェアモジュールです。あわせて AWS は、Isabelle/HOL という定理証明支援系 (proof assistant) を使用して、この Isolation Engine の正当性とセキュリティ保証を形式的に検証したことも発表しました。世界初の形式的に検証されたクラウドハイパーバイザーとして、NIE はクラウドセキュリティの新しい標準を打ち立てています。

定理証明支援系とは、人間のユーザーが形式的証明を構築するのを支援する自動化ツールです。その対象は、数学の定理からハードウェアやソフトウェアシステムの妥当性まで、あらゆるものに及びます。広く使われている定理証明支援系はいくつかありますが、私たちが Isabelle/HOL を選んだのは、表現力、自動化、証明の読みやすさ、スケーラビリティのバランスが私たちの用途に最も適していたからです。これは具体的にどういうことなのでしょうか?

コンピュータによる論理的推論

数学に決まった言語というものはありませんが、プログラミング言語が計算タスクを表現するのと同じように、数学的推論を表現するための言語を作ることができます。そして、プログラミング言語に表現力とパフォーマンスのトレードオフがあるように、数学的言語にも表現力と自動化のしやすさのトレードオフがあります。形式的証明の構築は時間がかかり、極めて根気のいる作業であるため (ボトルの中に船を組み立てる作業に似ています)、自動化は不可欠です。

最も初歩的な数学的言語はブール論理です。これは、AND、OR、NOT といった論理演算子の世界です。この言語は非常にシンプルであるため、強力な自動ソルバーが存在します。2016 年、カーネギーメロン大学の Marijn Heule 教授 (現在は Amazon Scholar) とその同僚たちは、未解決の数学的問題であるブール・ピタゴラス数問題をブール論理に符号化し、自動ソルバーを使って、200 テラバイトという史上最大の証明を作り上げました。

一階述語論理と呼ばれるより豊かな数学的言語では、整数などの対象領域について語り、その領域上の関数を定義できます。また、「すべての～について」や「～が存在する」という量化子を主張に含めることで、ブール論理を超える表現が可能になります。この種の言語では、「2 より大きいすべての素数は奇数である」といった文を表現できます。また、Lewis Carroll による次の定理を証明することもできます。ワルツを踊るアヒルはいない。ワルツを断る士官はいない。私の家禽はすべてアヒルである。ゆえに、私の家禽の中に士官はいない。

しかし、ほとんどの人は、プログラミングと同じように型を定義できる、さらに強力な数学的言語を好みます。高階論理には、Haskell などの関数型プログラミング言語に見られるような関数型さえ存在します。高階論理は一階述語論理よりもはるかに豊かで、「数 1 を含み、加法について閉じているすべての集合は、すべての正の整数を含む」といった文を表現できます。数学の大部分を表現できるほど豊かであると考えられています。

最も豊かな数学的言語である依存型理論では、型が任意の値をパラメータとして取ることさえ可能です。例えば T(i) のように、i を整数とすることができます。この種の言語で最もよく知られているのは Lean と Rocq です。

一階述語論理には強力な自動定理証明器が存在しますが、高階論理やそれ以上の言語では、完全な自動化は利用できません。これが表現力の代償です。定理証明支援系を使えば、ユーザーは部分的な自動化の支援を受けながら対話的に証明を構築でき、独自の証明探索をコーディングすることも可能です。定理証明支援系は、論理法則への厳格な準拠を強制します。これは通常、定理を作成する権限をコードの限られた部分にのみ与えるカーネルアーキテクチャによって実現されます。

定理証明支援系は、非常に大規模になり得る形式的仕様の階層を対話的に開発することもサポートします。例えば、Nitro Isolation Engine (NIE) の検証は、Graviton-5 プロセッサのアーキテクチャの仕様、ハイパーコールの Rust コードとその機能的正当性、そして証明すべきセキュリティ特性の仕様の上に成り立っています。形式的証明を構成する 25 万行の大部分は、これらの仕様が占めています。

高階論理は、密接に関連する 2 つの定理証明支援系である HOL と HOL Light でサポートされており、1990 年代からハードウェア設計、浮動小数点アルゴリズム、純粋数学の検証に使われてきました。AWS のシニアプリンシパルアプライドサイエンティストである John Harrison は HOL Light を開発し、暗号アルゴリズムの最適化バージョンを検証することで、Amazon の Graviton2 チップにおけるデジタル署名のパフォーマンスを最大 94% 向上させました。このコードは繊細であり、網羅的なテストは現実的ではありません。このような重要なソフトウェアをデプロイする前に取り得る手段は、完全な機能的正当性の形式的検証しかありませんでした。しかし、ここで注目したいのは Isabelle/HOL です。

Isabelle/HOL の概要

Isabelle/HOL と他の HOL システム (いずれも高階論理に基づいています) の最も目に見える違いは、その仕様記述言語と証明言語です。ほとんどの定理証明支援系では、ユーザーは証明したいことを記述した後、一種のモグラたたきゲームのように、元のゴールを一連のサブゴールに置き換えるコマンドを次々と続けていきます。Isabelle では (Lean でもある程度は)、証明言語によって望ましい中間ゴールを明示的に書き出すことができるため、証明プロセスをより適切に制御でき、より読みやすい証明ドキュメントが得られます。オンラインには多くの例があります。

その他の注目すべき機能は以下のとおりです。

• Rust 言語のかなりの部分を仕様に埋め込むことを可能にしたユーザー設定可能なパーサー
• 例えば + に、さまざまな数値型だけでなくマシンワードやその他の適切な文脈でも自然な意味を与える、原則に基づいたオーバーロードのための型クラス
• 仕様の階層を定義し、証明の中でさえさまざまな方法で解釈できる軽量なモジュールシステムであるロケール (locales)
• 単純化と後ろ向き連鎖による証明探索を通じた、強力な組み込みの自動化
• さらに強力な外部の自動化にワンクリックでアクセスできる sledgehammer
• 実際には偽である主張を特定するための反例発見ツール
• 適合性のテストに使用した、実行可能な高階仕様からのコード生成

NIE の検証にあたっては、まず 分離論理 (separation logic) と呼ばれる特化した言語を Isabelle/HOL の上に実装することから始めました。分離論理は、共有リソースを操作するプログラムコードの検証のために設計されたものです。私たちは独自の証明自動化をコーディングし、組み込みの自動化も活用しました。そのため、分離論理を使いつつ、必要に応じて通常の高階論理も使うことができました。Isabelle は、非常に巨大なサブゴールにも対処できるほど堅牢かつ効率的であることがわかりました。市販のラップトップを使って、25 万行の証明を 30 分で実行できたのです。

Isabelle/HOL の応用事例

NIE 以前の Isabelle の応用事例として最も印象的なのは、おそらく広く使われているマイクロカーネルである seL4 の検証でしょう。この証明も最初に発表された時点では約 25 万行でしたが、現在ではさらに長くなっています。seL4 の開発者たちは、マイクロカーネルの C 実装が抽象的仕様を詳細化したものであることを証明し、コア操作の完全な機能的正当性を実現しました。そして、検証されたコード部分ではバグが一切観測されていません。ただし、未検証の部分や形式化できない一部の前提条件をカバーするために、テストは依然として重要な役割を果たしています。

Isabelle は以下のプロジェクトでも使用されました。

• エラーの特定、特にその型システムの健全性の証明を目的とした、WebAssembly 言語のセマンティクスの形式化
• Cogent プログラミング言語のための検証フレームワークの作成
• 分散編集に使用される、競合のないレプリケートデータ型 (CRDT) のアルゴリズムの正当性の証明
• 純粋数学における数多くの結果の形式化
• 抽象レベルでの暗号プロトコルの検証

Isabelle は無料のオープンソースソフトウェアであり、ダウンロードして利用できます。十分なメモリを備えたマシンであれば、主要なオペレーティングシステムすべてで動作します。