TLA+とDafnyで始める形式検証：AWSが毎日10億回実行する品質保証手法
この記事でわかること
- 形式検証の基本概念と、テスト・静的解析との違いをMLの視点で理解できる
- TLA+を使って分散システムの設計をモデル検査する方法を習得できる
- Dafnyで「証明付きコード」を書く感覚を体験できる
- AWSやMicrosoftが形式検証を本番システムにどう適用しているかを知れる
- LLMが形式検証の敷居を劇的に下げる「vericoding」の最新動向を把握できる
対象読者
- 想定読者: ソフトウェア品質に関心のあるMLエンジニア・ソフトウェアエンジニア
-
必要な前提知識:
- プログラミング経験（Python、TypeScript等いずれか）
- 論理式（AND / OR / NOT / 含意）の基本的な読み方
- テスト駆動開発の基礎知識
結論・成果
形式検証は「数学的に正しさを証明する」品質保証手法です。AWSでは2011年から10のシステム（S3、DynamoDB、EBS等）に対して7チームがTLA+を適用し、テストでは発見不可能だった深刻なバグを検出しています。2025年時点で、AWSの自動推論ツールcvc5は毎日約10億回の検証チェックを実行しています（ACM Queue）。
さらに、LLMの進化によって形式検証のコスト構造が変化しつつあります。VeriBenchベンチマークでは、LLMによるDafnyコード生成（vericoding）の成功率が**82%**に達しており（VeriBench）、Martin Kleppmannは「AIが形式検証をメインストリームにする」と予測しています（Kleppmann, 2025）。
形式検証の基本概念を理解する
形式検証とは、ソフトウェアやハードウェアの「仕様」を数学的に記述し、「実装」がその仕様を必ず満たすことを証明する手法です。MLエンジニアにとって身近な例えを使うと、テストが「サンプルデータでの評価」だとすれば、形式検証は「入力空間全体に対する網羅的な証明」に相当します。
テスト vs 静的解析 vs 形式検証
これら3つの品質保証手法は、検証の範囲と保証の強さが異なります。
| 手法 | 検査範囲 | 保証の強さ | コスト | MLでの類似概念 |
|---|---|---|---|---|
| テスト | 有限個の入力 | バグの存在を示せる | 低 | テストセットでの評価 |
| 静的解析 | コードパターン | 特定パターンの検出 | 低 | 型チェック（mypy等） |
| 形式検証 | 全状態空間 | 正しさの数学的証明 | 高 | 入力空間全体の網羅的検証 |
テストの限界は、Edsger Dijkstraの有名な言葉に集約されます。「テストはバグの存在を示すことはできるが、バグの不在を示すことはできない」。形式検証は、この限界を超えてバグの不在を数学的に証明できます。
ただし、形式検証には制約もあります。仕様そのものが間違っていれば検証結果も意味を持ちません。また、全てのソフトウェアに適用するのは現実的でないため、障害時の影響が大きいコア部分に集中して適用するのが実務上のアプローチです。
形式検証の3つの主要手法
形式検証には大きく3つのアプローチがあります。
1. モデル検査（Model Checking）: システムの振る舞いを状態機械（State Machine）として記述し、取り得る全ての状態を自動的に探索します。不変条件（Invariant）に違反する状態が見つかれば、バグに至る具体的なステップを反例として出力します。代表的なツールはTLA+のTLCモデルチェッカーやSPINです。
2. 定理証明（Theorem Proving）: 仕様と実装の関係を論理式として表現し、数学的な証明を構築します。MLの文脈では、モデルの収束証明に近い概念です。代表的なツールはLean 4、Coq、Isabelle/HOLです。証明の構築には人間の介入が必要でしたが、LLMの進化でこの状況が変わりつつあります。
3. SMTソルバー（Satisfiability Modulo Theories）: 制約条件を論理式として表現し、その充足可能性を自動で判定します。「この条件を満たす入力は存在するか？」を自動で回答できます。代表的なツールはZ3（Microsoft Research）で、DafnyやF*の内部エンジンとして使われています。
注意: モデル検査は状態空間の爆発（State Space Explosion）という制約があります。変数やプロセスの数が増えると探索すべき状態数が指数的に増大し、AWSの事例では1つのモデルで310億状態の探索に16-vCPU EC2インスタンスで約5週間を要した例があります（AWS Formal Methods）。
TLA+でモデル検査を実践する
TLA+は、Leslie Lamportが設計した形式仕様記述言語です。分散システムの設計を数学的に記述し、TLCモデルチェッカーで全状態空間を自動探索できます。AWSでS3、DynamoDB、EBSの検証に使われている実績があります。
TLA+の基本構造
TLA+では、システムの初期状態と状態遷移を定義し、全ての状態で満たすべき不変条件を記述します。MLのハイパーパラメータサーチがパラメータ空間を探索するように、TLCは状態空間を網羅的に探索します。
実際に、分散システムでよくある「2つのプロセスが同時にリソースを取得してしまう」問題（排他制御）をTLA+で検証してみましょう。
---------------------------- MODULE MutualExclusion ----------------------------
\* 2つのプロセスの排他制御をモデル化
EXTENDS Integers
VARIABLES pc1, pc2 \* 各プロセスの状態（program counter）
vars == <<pc1, pc2>>
\* 初期状態: 両方ともidle
Init == pc1 = "idle" /\ pc2 = "idle"
\* プロセス1の状態遷移
Enter1 == pc1 = "idle" /\ pc1' = "waiting" /\ UNCHANGED pc2
Access1 == pc1 = "waiting" /\ pc2 /= "critical" /\ pc1' = "critical" /\ UNCHANGED pc2
Exit1 == pc1 = "critical" /\ pc1' = "idle" /\ UNCHANGED pc2
\* プロセス2の状態遷移
Enter2 == pc2 = "idle" /\ pc2' = "waiting" /\ UNCHANGED pc1
Access2 == pc2 = "waiting" /\ pc1 /= "critical" /\ pc2' = "critical" /\ UNCHANGED pc1
Exit2 == pc2 = "critical" /\ pc2' = "idle" /\ UNCHANGED pc1
\* 全体の状態遷移（いずれかのアクションが発生）
Next == Enter1 \/ Access1 \/ Exit1 \/ Enter2 \/ Access2 \/ Exit2
\* 不変条件: 2つのプロセスが同時にcriticalにならない
MutualExclusion == ~(pc1 = "critical" /\ pc2 = "critical")
\* 仕様全体
Spec == Init /\ [][Next]_vars
================================================================================
このモデルでは、MutualExclusionが不変条件（Invariant）です。TLCモデルチェッカーは、Initから到達可能な全ての状態を幅優先探索し、この不変条件に違反する状態がないかを検証します。
TLA+の実行とエラー検出
TLA+を実行するには、TLA+ Toolbox（IDE）またはコマンドラインツールを使います。
# TLA+ Toolsのインストール（Java 11以上が必要）
# GitHub: https://github.com/tlaplus/tlaplus/releases
# コマンドラインでのモデルチェック実行
java -jar tla2tools.jar -config MutualExclusion.cfg MutualExclusion.tla
TLCの出力例（不変条件違反が見つかった場合）:
Error: Invariant MutualExclusion is violated.
Error: The behavior up to this point is:
State 1: pc1 = "idle", pc2 = "idle"
State 2: pc1 = "waiting", pc2 = "idle"
State 3: pc1 = "waiting", pc2 = "waiting"
State 4: pc1 = "critical", pc2 = "waiting"
State 5: pc1 = "critical", pc2 = "critical" <-- 違反!
この反例（Counterexample）が出力されることで、「どの状態遷移の組み合わせでバグが発生するか」が具体的にわかります。上記の例では、Access2の条件が不十分で、プロセス1がcritical状態のときにプロセス2もcriticalに遷移できてしまっています。
よくある間違い: 最初はTLA+を「プログラミング言語」として書こうとしがちですが、TLA+は設計のモデル化ツールです。実装コードではなく、システムの振る舞いの「仕様」を記述するものです。AWSのエンジニアも、最初はこの発想の転換に苦労したと報告しています。
AWSでのTLA+活用事例
AWSのTLA+活用は、形式検証の産業応用として最も成功した事例の一つです。2014年に発表された論文（How Amazon Web Services Uses Formal Methods）では、以下の成果が報告されています。
| システム | 検証対象 | 発見された問題 |
|---|---|---|
| S3 | オブジェクトストレージの整合性 | テストでは見つからない微妙な競合状態 |
| DynamoDB | レプリケーションプロトコル | ネットワーク分断時のデータ不整合 |
| EBS | ボリューム管理の状態遷移 | 障害復旧時のエッジケース |
| 内部分散ロック | ロック取得の公平性 | スターベーション（餓死）の可能性 |
特筆すべきは、AWSのエンジニアがTLA+を2〜3週間で習得し、実用的な成果を出せたことです。正式なトレーニングプログラムなしに、ドキュメントと同僚からのサポートだけで習得した事例もあります。
ポイント: TLA+は設計段階で使うものであり、実装コードから自動生成するものではありません。設計の正しさを検証した後、その設計に基づいて実装を行うワークフローになります。Jack Vanlightlyは「数週間のデバッグは数時間のTLA+で節約できる」と述べています（A Primer on Formal Verification and TLA+）。
Dafnyで「証明付きコード」を書く
Dafnyは、Microsoft Researchが開発した検証対応プログラミング言語です。コードの中に仕様（事前条件・事後条件・不変条件）を直接書き込み、コンパイル時に自動証明してくれます。内部ではBoogie中間言語を経由してZ3 SMTソルバーが証明を行います。
Dafnyの基本：事前条件と事後条件
Dafnyでは、requires（事前条件）とensures（事後条件）を関数に付与できます。Pythonの型ヒントに値の制約を追加したようなものです。
// Dafnyによる二分探索の実装と検証
// 事前条件: 配列がソート済み
// 事後条件: 返り値のインデックスが正しい要素を指す
method BinarySearch(a: array<int>, key: int) returns (index: int)
requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j] // ソート済み
ensures index >= 0 ==> index < a.Length && a[index] == key // 見つかった場合
ensures index < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != key // 見つからない場合
{
var lo, hi := 0, a.Length;
while lo < hi
invariant 0 <= lo <= hi <= a.Length
invariant forall i :: 0 <= i < lo ==> a[i] < key
invariant forall i :: hi <= i < a.Length ==> a[i] > key
{
var mid := lo + (hi - lo) / 2; // オーバーフロー防止
if a[mid] < key {
lo := mid + 1;
} else if a[mid] > key {
hi := mid;
} else {
return mid;
}
}
return -1;
}
このコードをDafnyのコンパイラに通すと、以下が数学的に証明されます。
- ソート済み配列に対して、返り値が正のインデックスなら
a[index] == key - 返り値が負なら、配列中にkeyは存在しない
- ループが必ず終了する（ループ変数
hi - loが単調減少） - 配列の範囲外アクセスが発生しない
# Dafnyのインストールと実行
# https://github.com/dafny-lang/dafny/releases
# 検証のみ（コンパイルなし）
dafny verify BinarySearch.dfy
# 検証 + Pythonコードへのコンパイル
dafny build --target:py BinarySearch.dfy
なぜDafnyを選んだか:
- SMTソルバー（Z3）による自動証明のため、人間が証明を書く負担が小さい
- C#、Go、Python、Java、JavaScriptにコンパイル可能で、既存プロジェクトに統合しやすい
- VeriBenchベンチマークにおいて、LLMによるvericoding成功率が**82%**と他の検証言語より高い（Verus/Rust: 44%, Lean 4: 27%）
Dafnyの実践例：スタックの検証
もう少し実践的な例として、スタックのデータ構造をDafnyで検証してみましょう。
// 検証済みスタック: push/popの正しさを数学的に保証
class Stack<T> {
var items: seq<T> // シーケンス（不変リスト）
// 抽象化関数: 内部表現と外部仕様の対応
function Elements(): seq<T>
reads this
{
items
}
constructor()
ensures Elements() == []
{
items := [];
}
method Push(val: T)
modifies this
ensures Elements() == [val] + old(Elements()) // 先頭に追加
{
items := [val] + items;
}
method Pop() returns (val: T)
requires |Elements()| > 0 // スタックが空でない
modifies this
ensures val == old(Elements())[0] // 先頭要素を返す
ensures Elements() == old(Elements())[1..] // 先頭を除いた残り
{
val := items[0];
items := items[1..];
}
method IsEmpty() returns (empty: bool)
ensures empty <==> |Elements()| == 0
{
empty := |items| == 0;
}
}
Dafnyコンパイラは、Pushの後にPopすると必ずPushした値が返ることを自動証明します。MLエンジニアの視点では、「入力に対する出力の不変性テスト」を100%のカバレッジで実行しているのと同等です。
注意: Dafnyの検証はコンパイル時に完了します。実行時のオーバーヘッドはゼロです。ただし、事前条件（
requires）に違反する呼び出しはコンパイル時エラーになるため、呼び出し側のコードも仕様に適合する必要があります。これは「型安全性の拡張」と考えるとわかりやすいでしょう。
ニューラルネットワークの形式検証を知る
MLエンジニアにとって最も関連が深いのが、ニューラルネットワーク（NN）の形式検証です。DeepMindは「仕様テスト、ロバスト学習、形式検証」の3本柱アプローチを提唱しています（DeepMind Safety Research）。
NN検証の3つのアプローチ
ニューラルネットワークの検証には主に3つのアプローチがあり、それぞれ精度と計算コストのトレードオフがあります。
| アプローチ | 代表ツール | 特徴 | 制約 |
|---|---|---|---|
| SMTソルバー | Marabou 2.0 | NN特性をSMT問題に変換し厳密解を求める | 小規模NNのみ実用的 |
| 抽象解釈 | ERAN | 入力範囲を抽象的に伝播し出力範囲を推定 | 過近似により偽陽性がある |
| バウンド伝播 | alpha-beta-CROWN | GPU加速による効率的な境界伝播と分岐限定法 | VNN-COMP 5年連続優勝 |
alpha-beta-CROWNは、International Verification of Neural Networks Competition（VNN-COMP）で2021年から2025年まで5年連続優勝しており、現在最も実用的なNN検証ツールです。
NN検証が解く問題：敵対的摂動への頑健性
NN検証の典型的な応用は、敵対的摂動への頑健性の証明です。「入力画像に微小なノイズ（ε以下のL∞摂動）を加えても、分類結果が変わらない」ことを数学的に証明します。
# alpha-beta-CROWNによるNN頑健性検証の概念的なフロー
# 実際のコードはhttps://github.com/Verified-Intelligence/alpha-beta-CROWN を参照
# 1. 検証対象のモデルとプロパティを定義
# - モデル: 学習済みニューラルネットワーク
# - プロパティ: epsilon=0.03のL∞摂動に対する頑健性
# 2. バウンド伝播で出力範囲を計算
# - 入力: x ± epsilon の範囲
# - 各層で出力の上限・下限を伝播
# - 最終層の出力範囲で分類結果が変わるか判定
# 3. 分岐限定法で精度を向上
# - 不確定（バウンドが緩い）なニューロンを分割
# - 分割した部分問題を再帰的に解く
# 概念コード（実際のAPIとは異なります）
import torch
def verify_robustness(model, input_image, true_label, epsilon):
"""
モデルの頑健性を検証する概念フロー
- model: 検証対象のNN
- input_image: 入力テンソル
- true_label: 正しいラベル
- epsilon: 許容する摂動の大きさ
"""
# 入力範囲を定義
lower_bound = torch.clamp(input_image - epsilon, 0, 1)
upper_bound = torch.clamp(input_image + epsilon, 0, 1)
# バウンド伝播（実際はalpha-beta-CROWNの内部エンジンが実行）
# 出力の下限が、true_label以外のクラスの上限より大きければ
# → 頑健性が証明される
# 下限 > 上限 でなければ → 検証失敗（反例が存在する可能性）
return "verified" or "counterexample_found" or "undetermined"
NN検証の現在の限界
NN検証は急速に進歩していますが、現時点では以下の制約があります。
1. スケーラビリティ: 検証可能なモデルサイズは、現在の手法では比較的小規模なネットワークに限られます。ResNet-50やTransformerのような大規模モデル全体の検証は、計算コスト的にまだ困難です。
2. 仕様の定義困難: 形式検証の前提として「何が正しいか」の仕様が必要ですが、MLモデルが得意とするタスク（画像認識、自然言語理解等）では、正しさの厳密な定義自体が困難です。L∞摂動への頑健性は検証できますが、「猫の画像を正しく分類する」の数学的定義は自明ではありません。
3. 訓練・データパイプラインの検証: 現在の手法の多くは訓練済みモデルの推論時の性質を検証するもので、訓練プロセスやデータ前処理パイプラインの検証は「重要だが見落とされがちな領域」とされています（A Review of Formal Methods Applied to Machine Learning）。
LLMが形式検証の敷居を下げる：vericodingの最新動向
2025年後半から、LLMを使って「証明付きコード」を自動生成するvericoding（verified coding）という概念が注目されています。形式検証の最大の障壁であった「証明を書くコスト」をLLMが大幅に削減する可能性があります。
vericodingの成功率と課題
VeriBenchベンチマーク（12,504件の形式仕様）での検証言語別LLM vericoding成功率は以下の通りです。
Dafnyの成功率が高い理由は、SMTソルバー（Z3）による自動証明の恩恵です。LLMが生成するコードに仕様注釈（requires/ensures）を適切に付与すれば、証明自体はZ3が自動で行います。一方、Lean 4では人間（またはLLM）が証明の各ステップを明示的に記述する必要があるため、成功率が低くなります。
DeepSeek-Prover-V2：AI定理証明の最前線
DeepSeek-Prover-V2は、671Bパラメータの大規模言語モデルで、Lean 4の定理証明を自動化するツールです。
- MiniF2F-testベンチマークで**88.9%**のパス率を達成
- PutnamBench（大学数学コンテスト問題）で658問中49問を解決
- 強化学習によるサブゴール分解と、非形式的な推論と形式的な証明を組み合わせるアプローチ
seL4の教訓：コスト構造の変化
Martin Kleppmannの分析によると、seL4マイクロカーネル（8,700行のC言語コード）の形式検証には20人年と200,000行のIsabelle証明コードが必要でした（実装1行あたり約23行の証明コード）。この「23:1」のコスト比率が、形式検証の普及を阻んできた最大の要因です。
LLMがこの比率を劇的に改善しつつあります。VeriBenchの結果はその兆候であり、Kleppmannは「5〜10年以内に、形式検証が特殊技術からソフトウェア開発の標準ワークフローに変わる」と予測しています。
トレードオフ: LLMが生成する証明は正しいことが保証されます（証明チェッカーが検証するため）。しかし、LLMが「正しい仕様」を生成するかどうかは別問題です。仕様の妥当性は依然として人間の判断が必要であり、「仕様のレビュー」が新たなボトルネックになる可能性があります。
産業界での形式検証ツール比較
実務で形式検証を導入する際、どのツールを選ぶべきかは重要な判断です。以下に主要ツールの比較をまとめます。
| ツール | 手法 | 対象 | 学習コスト | 産業採用例 |
|---|---|---|---|---|
| TLA+ | モデル検査 | 分散システム設計 | 2-3週間 | AWS, Microsoft, Alibaba |
| Dafny | SMT自動証明 | 実装コード | 1-2週間 | AWS, Microsoft |
| Lean 4 | 依存型+定理証明 | 数学・アルゴリズム | 1-3ヶ月 | DeepSeek, Harmonic |
| SPIN | モデル検査 | 通信プロトコル | 2-4週間 | NASA, 通信業界 |
| Alloy | 軽量形式手法 | データモデル設計 | 1-2週間 | 教育・研究 |
| F* | 依存型+SMT | 暗号実装 | 2-3ヶ月 | Microsoft (Project Everest) |
選定の判断基準:
- 分散システムの設計検証 → TLA+（AWSの実績、学習コストが低い）
- 実装コードの自動検証 → Dafny（Z3による自動証明、多言語コンパイル）
- 暗号・セキュリティ → F*（Project Everestでの実績）
- 数学的証明・研究 → Lean 4（DeepSeek-Prover-V2との連携）
注意: Alloy 6で時相論理のサポートが追加されましたが、TLA+と比較すると表現力に制約があります。構造的なプロパティ（データモデル、API設計）の検証にはAlloyが適していますが、時間的な振る舞い（並行処理、分散プロトコル）の検証にはTLA+が適しています（Alloy 6 vs. TLA+ Discussion）。
よくある問題と解決方法
形式検証の導入でつまずきやすいポイントと対処法をまとめます。
| 問題 | 原因 | 解決方法 |
|---|---|---|
| 状態空間爆発でTLCが終わらない | 変数・プロセス数が多すぎる | 対称性の利用、抽象化レベルの引き上げ |
| Dafnyの証明がタイムアウト | Z3が証明を見つけられない | ループ不変条件の追加、補題（lemma）の分割 |
| 何を検証すべきかわからない | 仕様の定義が曖昧 | 「障害時の影響が最大のコンポーネント」から着手 |
| チームへの導入が進まない | 学習コストへの懸念 | TLA+から始める（2-3週間で成果、PlusCalで敷居を下げる） |
| 既存コードに形式検証を適用したい | レガシーコードに仕様がない | 重要なAPIの事前/事後条件から段階的に追加 |
まとめと次のステップ
まとめ:
- 形式検証は「テストでは見つけられないバグ」を数学的に検出・排除できる品質保証手法である
- TLA+によるモデル検査は、AWSが10のシステムで採用し、エンジニアが2-3週間で習得可能な実用的手法である
- Dafnyは「証明付きコード」をSMTソルバーで自動検証でき、C#/Go/Python等にコンパイル可能である
- NN検証はalpha-beta-CROWNがVNN-COMP 5年連続優勝しているが、大規模モデルへの適用は依然として課題がある
- LLMによるvericodingがDafnyで82%の成功率に到達し、形式検証のコスト障壁が崩れつつある
次にやるべきこと:
- Learn TLA+ でTLA+の基本を習得する（推定2-3週間）
- Dafny公式チュートリアル で小さなアルゴリズムの検証を試す
- 自分のプロジェクトで「障害時の影響が最大のコンポーネント」を特定し、TLA+でモデル化してみる
- NN検証に関心がある場合、alpha-beta-CROWN で小規模モデルの頑健性検証を試す
参考
- How Amazon Web Services Uses Formal Methods - CACM
- Use of Formal Methods at Amazon Web Services (PDF)
- Systems Correctness Practices at AWS - ACM Queue
- AI will make formal verification go mainstream - Martin Kleppmann
- A Primer on Formal Verification and TLA+ - Jack Vanlightly
- Learn TLA+
- Dafny公式サイト
- Dafny GitHub Repository
- DeepSeek-Prover-V2 (arXiv)
- VeriBench: End-to-End Formal Verification Benchmark
- alpha-beta-CROWN - VNN-COMP Winner
- DeepMind: Towards Robust and Verified AI
- A Review of Formal Methods Applied to Machine Learning (arXiv)
- Galois: Formal Methods + AI
- Practical Formal Methods: Companies List (GitHub)
注意: この記事はAI（Claude Code）により自動生成されました。内容の正確性については複数の情報源で検証していますが、実際の利用時は公式ドキュメントもご確認ください。