# 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）。ただし論文・公式ドキュメント外での詳細は不明。 ## 未解決の問い - TLA+ モデルをゼロから構築するコスト（3 ヶ月）と、「すでにあるモデルを 1 日で使う」との差は大きい。組織が TLA+ を持続的に活用するには既存モデルのライブラリとドメインエキスパートの育成が必要だが、その組織的コストを評価した研究はあるか。 - TLA+ は状態空間を全探索するため、モデルが複雑になると状態爆発（state explosion）が問題になる。SREcon スライドの p.19 は「failure sim disabled, vars skipped」と注記しており、モデルの完全度と計算量のトレードオフが実用上どう扱われているか。 - ポストモーテムにおける TLA+ の活用は「設計レベルの理解」を提供するが、その洞察がシステムの実際の修正にどう繋がるか（「確認できた」止まりか「再設計の根拠」になるか）の成功事例が他にあるか。 ## 関連 - ソース: [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]]（TLA+ をインシデントポストモーテムに適用した事例） - エンティティ: [[Markus A. Kuppe]]（TLA+ プロジェクト 10 年以上のエンジニア）/ [[Finn Hackett]]（TLA+ 活用研究の PhD 学生）/ [[Azure CosmosDB]]（TLA+ モデルが公開されているシステム） - 概念: [[ポストモーテム]]（TLA+ が補完する設計レベルの洞察）/ [[結果整合性]]（TLA+ モデルで検証された整合性特性） - 学習リソース: http://tlapl.us ## 出典 - [[@2023__SREcon23Americas__Turning an Incident Report into a Design Issue with TLA+]]（TLA+ のポストモーテム活用ワークフロー、Azure CosmosDB モデル事例）