TLA+が検証できることとできないこと
Judul asli: What TLA+ can and can't check
Mengapa Ini Penting
AI時代の形式検証ブームが実態以上に語られるリスクを、専門家が具体的に整理した点が重要。
Boris Cherny（Claude Code発明者）がOpusによるTLA+でのレース条件検出を言及後、形式検証への過大な期待が広がる。長年のTLA+教育者が冷静な分析を提示。
Claude Codeの発明者Boris ChernyがAnthropicのOpusモデルによるTLA+を用いたレース条件の検出に言及したことで、形式検証（Formal Verification）への関心がネット上で急上昇した。一部では「形式手法がエージェント型ソフトウェア開発の問題を完全に解決する」という声も出ているが、長年TLA+を教えてきたHillel Wayneはその楽観論に警鐘を鳴らす。
TLA+が検証できるのは、事前に定義されたプロパティのみだ。システムをbehavior（状態の列）に分割し、`[]P`（常にPが真）、`<>P`（いつかPが真）、`P'`（次の状態でPが真）という時相論理演算子を組み合わせることで、安全性（Safety：悪いことが起きない）と活性（Liveness：良いことが必ず起きる）を表現できる。不変条件（Invariant）や終了保証なども記述可能だ。
しかし根本的な制約がある。「検証するにはまずプロパティが必要」という点だ。仕様を書く人間がそもそも何を保証すべきか分かっていなければ、TLA+は何も検査できない。正しい設計が正しいコードに直結しない問題とは別に、「表現すらできないプロパティが存在する」という限界をWayneは強調する。