TLA+で検証できること・できないこと
원제: What TLA+ can and can't check
왜 중요한가
AI生成コードへの形式検証適用に期待が集まる中、その限界を正確に理解することは、開発現場での誤用を防ぐ上で重要な視点を提供する。
Claude Codeの開発者がOpusによるTLA+でのレースコンディション検出を報告したことを契機に、形式検証への関心が急騰した。長年TLA+を教えてきたHillel Wayne氏が2026年9月30日、「形式手法がAIエージェント開発の問題をすべて解決する」という楽観論に警鐘を鳴らし、TLA+が表現できる性質とできない性質を詳細に解説した。
Claude Codeの発明者であるBoris Cherny氏が「OpusがTLA+を使ってレースコンディションを発見できた」と言及したことで、形式検証への熱狂がインターネット上に広がった。これに対しTLA+の教育者・推進者であるHillel Wayne氏は、過度な期待に警戒感を示した。
TLA+が検証できるのは、システムの「振る舞い」—状態の連続—に対して論理式が成り立つかどうかだ。具体的には、安全性（「悪いことが決して起きない」）と活性（「良いことが必ず起きる」）の2種類の性質を検証できる。安全性は「[]P（常にP）」「P'（次状態でP）」で表現し、活性は「<>P（いつかP）」の組み合わせで表現する。例えば「[]<>P」は「すべての状態で、将来のどこかでPが成り立つ」を意味し、リーダー選出のような回復機構の検証に使える。
一方でWayne氏が強調するのは根本的な制約だ。「性質を検証するには、そもそも検証すべき性質を定義できなければならない」。パフォーマンス要件、ユーザビリティ、ビジネスロジックの曖昧さ、正しい仕様を書く人間の能力—これらはTLA+の外側にある問題であり、形式手法では扱えない。設計が正しくても実装が正しいとは限らない点も既知の限界として挙げられる。
「形式手法はAIエージェント開発を一気に解決する」という言説は誤りであり、TLA+が得意とする並行システムの設計検証という本来の強みを冷静に理解することが重要だとWayne氏は訴える。