# TLA+ ## 定義 TLA+（Temporal Logic of Actions+）は、Leslie Lamport が設計した形式仕様記述言語および検証ツール群である。分散システムやアルゴリズムの挙動を数学的に記述し、TLC モデルチェッカーが有限の状態空間を全探索して**不変条件（invariant）の違反やカウンター例を自動的に発見する**。Amazon DynamoDB・Google Firestore・Azure CosmosDB など主要なクラウドデータストアが設計検証に活用している。 TLA+ の核心は「状態マシン」の考え方である。システムの動作を「初期状態の定義」「各ステップでの状態遷移」「正しい動作の仕様」の 3 要素で記述し、チェッカーが「すべての可能な実行経路」を探索して仕様違反を探す。人間が手動ではなかなか気づけない並行性のバグ・タイミング依存の挙動・稀な競合状態をシステマティックに発見できる点が強み（[[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]]）。 ## TLA+ をインシデント分析に使う [[Finn Hackett]] と [[Markus A. Kuppe]] は SREcon23 Americas で、TLA+ をポストモーテムの補助ツールとして使うワークフローを提案した（[[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]]）。 **ワークフロー**: 1. インシデントレポートと実システムから「何が正しい動作か」の仕様を書く 2. システムの動作をモデル化する（ドメインエキスパートが主導） 3. TLC チェッカーがカウンター例を生成 → 問題を設計レベルで明文化 インシデントレポートは「何が起きたか・なぜ緩和したか」を文書化するが、**「なぜ設計がその動作を許したか」という設計レベルの洞察を欠く**場合がある。TLA+ モデルは小規模再現が困難な問題（レースコンディション、分散整合性の微妙な違反）を数学的に再現し、「疑われていたが証明できなかった」根本原因を確定できる。 **注意点**: モデルの新規構築には数ヶ月かかる（Azure CosmosDB モデルは 3 ヶ月）。一方、既存の高品質モデルを活用すれば 1 日でインシデント分析に使える。モデル構築はドメインエキスパートの関与が不可欠。 ## 横断的知見 - Amazon DynamoDB・Google Firestore・Azure CosmosDB はいずれも TLA+ を設計検証に使っており、プラネットスケール分散ストアにおける TLA+ の採用が業界標準的になりつつある（[[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]] p.9）。ただし論文・公式ドキュメント外での詳細は不明。 - **DDIA 第9章は TLA+ を「ポストモーテムの事後分析」でなく「実装前の設計検証」という異なる適用局面に位置づけ、CockroachDB・TiDB・Kafka という別系統の採用事例と、viewstamped replication のデータ損失発見という具体的な成功例を挙げる**: [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]] はインシデント発生**後**に「なぜ設計がその動作を許したか」を明文化する事後分析ワークフローを扱うが、DDIA 第9章は TLA+ を「アルゴリズムを実装する**前**に、モデルチェッカーが不変条件の違反やカウンター例を全状態空間探索で発見する」という予防的検証として紹介する。具体例として、TLA+ を用いた研究が viewstamped replication (VR) アルゴリズムのプローズ記述の曖昧さに起因するデータ損失の可能性を実証したことを挙げており、これは自然言語による仕様記述が持つ本質的な曖昧さを形式仕様が解消する事例として、ポストモーテム分析とは独立の価値を示す。両ソースを合わせると、TLA+ は「設計前の予防」と「インシデント後の事後理解」という異なる 2 つのライフサイクル局面で使われていることが分かる。(Source: [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]], [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "Model checking and specification languages") - **状態空間爆発への対処は「モデルの近似・上限設定」という共通の限界として両ソースで確認される**: [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]] は SREcon スライドで「failure sim disabled, vars skipped」と実務上の妥協を示すが、DDIA 第9章も「モデル検査は無限の状態空間を持つ現実のアルゴリズムに対して全状態を証明できないため、近似モデルへ縮小するか実行の上限(最大メッセージ数等)を設定する」と同種の限界を一般原理として説明する。より長い実行でのみ現れるバグは発見されない点も共通する。DDIA はこれを「モデルは実装の簡略版であり、仕様と実装が乖離しうる」というモデル検査全般のリスクとして位置づけており、SREcon の実務的妥協はこの一般原理の具体的な現れと解釈できる。(Source: [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]], [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]] "Model checking and specification languages") ## 未解決の問い - TLA+ モデルをゼロから構築するコスト（3 ヶ月）と、「すでにあるモデルを 1 日で使う」との差は大きい。組織が TLA+ を持続的に活用するには既存モデルのライブラリとドメインエキスパートの育成が必要だが、その組織的コストを評価した研究はあるか。 - TLA+ は状態空間を全探索するため、モデルが複雑になると状態爆発（state explosion）が問題になる。SREcon スライドの p.19 は「failure sim disabled, vars skipped」と注記しており、モデルの完全度と計算量のトレードオフが実用上どう扱われているか。 - ポストモーテムにおける TLA+ の活用は「設計レベルの理解」を提供するが、その洞察がシステムの実際の修正にどう繋がるか（「確認できた」止まりか「再設計の根拠」になるか）の成功事例が他にあるか。 - TLA+ による予防的検証(実装前)とポストモーテム分析(インシデント後)の 2 局面を同一のモデルで使い回すことは可能か。DDIA が挙げる CockroachDB・TiDB・Kafka の TLA+ モデルは、SREcon の Azure CosmosDB 事例のようにインシデント分析にも転用されているか。 - モデル検査（TLA+）と決定論的シミュレーションテスト（DST、[[軽量形式手法]] 参照）はどちらも「実装が性質を満たすか」を検証するが、TLA+ が簡略化モデルを検証するのに対し DST は実コードを検証する。両者を同一プロジェクトで併用する場合、どちらを先に適用すべきか、あるいは検証範囲をどう分担すべきか。 ## 関連 - ソース: [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]]（TLA+ をインシデントポストモーテムに適用した事例）/ [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]]（TLA+ を予防的モデル検査として一般化) - エンティティ: [[Markus A. Kuppe]]（TLA+ プロジェクト 10 年以上のエンジニア）/ [[Finn Hackett]]（TLA+ 活用研究の PhD 学生）/ [[Azure CosmosDB]]（TLA+ モデルが公開されているシステム） - 概念: [[ポストモーテム]]（TLA+ が補完する設計レベルの洞察）/ [[結果整合性]]（TLA+ モデルで検証された整合性特性）/ [[軽量形式手法]]（DST という相補的な検証技法）/ [[システムモデルと安全性・活性]]（TLA+ が検証する性質の理論的枠組み） - 学習リソース: http://tlapl.us ## 出典 - [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]]（TLA+ のポストモーテム活用ワークフロー、Azure CosmosDB モデル事例） - [[@2026__OReilly__Designing Data-Intensive Applications 2E - Chapter 9 The Trouble with Distributed Systems]]「Model checking and specification languages」（TLA+ の予防的モデル検査としての位置づけ、CockroachDB/TiDB/Kafka の採用、viewstamped replication のデータ損失発見)