TLA+で検証できることとできないこと
मूल शीर्षक: What TLA+ can and can't check
यह क्यों महत्वपूर्ण है
AI生成コードの品質保証としてformal verificationへの注目が高まる中、ツールの実際の限界を理解することは現実的な活用に不可欠。
Claude Codeの発明者Boris Chernyが、OpusがTLA+を使ってコードのrace conditionを発見できると言及したことで、formal verificationへの関心が急上昇した。しかしTLA+の長年の教育者Hillel Wayneは、「TLA+がagentic software開発の問題をすべて解決する」という期待に警鐘を鳴らしている。
Claude Codeの発明者Boris Chernyが先週、OpusがTLA+を活用してrace conditionを検出できると述べたことで、インターネット上ではformal verificationの話題が一気に広まった。TLA+の長年の教育者・支持者であるHillel Wayneはこの盛り上がりを喜びつつも、「formal methodsがagentic software開発の問題をすべて解決する」という主張を「ナンセンス」と断言する。
TLA+が検証できるものとして、Wayneはまずシステムを「behaviors（振る舞いの列）」として表現し、各状態でboolean式を評価できることを説明する。時間論理演算子として「[]P（常にPが成立）」「P'（次の状態でPが成立）」「<>P（いつかPが成立）」の3つを使い、safety property（悪いことが起きない）とliveness property（良いことが必ず起きる）を表現できる。
しかし核心的な限界は、「検証するにはそもそも検証すべき性質が必要」という点だ。TLA+はシステムの設計レベルの論理的正しさをチェックできるが、「検証したい性質を人間が正確に定義できるか」という問題は別の話。性質を定義できなければ、どれだけ強力なツールも何も保証できない。正しい設計が正しいコードに自動変換されるわけでもない。WayneはTLA+の可能性を否定しているわけではなく、過剰な期待に対してバランスを求めている。