TLA+でできること・できないこと
原題: What TLA+ can and can't check
なぜ重要か
AIコード生成と形式検証の組み合わせへの期待が高まる中、その限界を技術的根拠で示した議論は開発現場の判断基準を適切に補正する。
Claude Codeの開発者Boris ChernyがOpusモデルによるTLA+を用いたレースコンディション検出を報告したことで、2026年9月末にネット上で形式検証への関心が急拡大した。TLA+の長期教育者Hillel Wayneは同月30日付の記事で「形式手法がAIエージェント開発の諸問題を一挙に解決する」という過熱した期待を批判的に検証。TLA+が表現できる性質（安全性・活性）と、そもそも表現すら不可能な性質の違いを解説した。
発端はClaude Codeの生みの親Boris ChernyによるXへの投稿だ。OpusモデルがTLA+を活用してコードのレースコンディションを発見できたと報告し、形式検証を巡る議論がネット全体に広がった。
TLA+の教育者であり長年の推進者でもあるHillel Wayneはこの熱狂を歓迎しつつも、「形式手法がAIエージェント開発の問題をすべて解決する、というのは無意味な主張だ」と釘を刺す。
記事ではまずTLA+が「チェックできること」を整理している。TLA+はシステムを状態の列（ビヘイビア）として表現し、各状態でブール式を記述する。時相論理演算子として「[]P（常にPが成立）」「P'（次の状態でPが成立）」「<>P（いつかPが成立）」の3つを持つ。これらを組み合わせることで、不変条件（safety）や活性（liveness）を表現できる。たとえば「[]<>P（どの状態からも、将来P が成立する瞬間が必ずある）」はリーダー選出アルゴリズムの収束を表現でき、「<>[]P（ある時点以降Pが永続的に成立する）」はアルゴリズムの正しい終了を示せる。
一方でWayneが強調するのは「性質を検証するには、そもそも検証すべき性質を定式化しなければならない」という根本的な制約だ。TLA+の既存の議論では「正しい設計が自動的に正しいコードに変換されるわけではない」という弱点が多く語られてきたが、今回の記事はそれとは別の限界、すなわち「表現すらできない性質が存在する」点に焦点を当てている。
AIエージェントが自動的にTLA+仕様を書いたとしても、何を性質として定めるかという判断は依然として人間に委ねられている。形式検証はツールであり、問いを立てる能力の代替にはならない、というのがWayneの主張の核心だ。