TLA+で検証できること・できないこと

2026年9月30日 TLA+で検証できること・できないこと 「TLA+がAIの過ちを救う」という物語に少しだけ冷静になろう 先週、Claude Codeの発明者であるBoris Cherny氏が、OpusがTLA+1を使用してコード内の競合状態を発見できたと述べました。そして今、インターネット上の誰もが形式検証について話題にしています。長年の教育者（[1][2]）およびTLA+の提唱者として、これは本当にエキサイティングです！ TLA+は、複雑な並行システムを設計し、それらがバグフリーであることを保証するのに優れています。2長年の冷静さの提唱者として、この新しい熱狂は私を心配させます。 私は、形式手法がエージェント型ソフトウェア開発の問題を一度きり解決すると言う人々をたくさん読みましたが、それはナンセンスです。 正しい設計が自動的に正しいコードに変換されるわけではない、といったTLA+の保証できることの弱点については、すでに十分な言葉が費やされてきました。そこで、このニュースレターでは、別の制限に焦点を当てたいと思います。それは、プロパティを検証するには、検証すべきプロパティが必要だということです！では、TLA+で表現することさえできないプロパティとは何でしょうか？（これはTLA+の基本的な知識があることを前提としています。もしあなたが全くの初心者なら、上記の[1][2]をチェックするか、ここで読んでください。） TLA+で検証できること TLA+はシステムを一連の振る舞いに分割します。各振る舞いは状態のシーケンスです。例えば、「ライト1が緑、次に黄色、次に赤」のようなものです。各状態では、「ライト4が緑」や「すべてのライトが赤」のような通常のブール式を表現できます。また、3つの「時間的」論理演算子で式を変更することもできます。 []P（「常にP」）は、現在の状態およびすべての将来の状態においてPが真である場合に真となります。例：[](at_most_one_green)は、将来のすべての状態において緑色のライトが1つ以下である場合に真となります。 P'（「Pプライム」）は、次の状態においてPが真である場合に真となります。例：light="green" && light'="red"は、ライトが緑から赤に変わる場合に真となります。 <>P（「最終的にP」）は、現在の状態または少なくとも1つの将来の状態においてPが真である場合に真となります。例：<>(light4 = "yellow")は、light4が黄色であるか、将来の状態のいずれかで黄色である場合に真となります。 Pがシステムのプロパティであると言うとき、それはすべての振る舞いの初期状態において真であることを意味します。したがって、[]Pというプロパティをチェックすると、それはすべての初期状態において[]Pが真であることを意味し、その後「常に」の定義により、それはその初期状態からのすべての将来の状態においてPが真であることを意味し、それはすべての振る舞いのすべての状態において真であることを意味します。私たちはこれを不変条件と呼び、TLA+でチェックする最も基本的なプロパティの1つです。 プライムと組み合わせてアクションプロパティを取得したり、不変条件を変更したりすることもできます。[](x' >= x)は、xの新しい値が常にxの古い値以上である場合に真となります。もう一つの面白いものは[](P => P')です。Pが真になると、二度と偽になることはありません。 実際のTLA+は、「スタッター不変性」というもののために少し複雑ですが、それは追加の詳細です。 アクションプロパティと不変条件は、どちらも安全プロパティであり、大まかに言うと「悪いことは決して起こらない」ということです。私は安全とライブネスに関する記事をここに書きました。ライブネスは、ちなみに、「良いことは常に起こる」ということです。 すべてのライブネスプロパティは<>に基づいています。それ自体では、<>Pは「すべての振る舞いの少なくとも1つの状態においてPが真である」という意味であり、これは通常、良いシステムプロパティとしては弱すぎます。しかし、組み合わせることで、より興味深いライブネスプロパティを作成できます。 []<>Pは、すべての状態において、Pが少なくとも1つの将来の状態において真である場合に真となります。これは、「ノードが新しいリーダー選挙を行う場合、最終的にリーダーに合意する」といった回復メカニズムを表すことができます。 <>[]Pは、ある時点でPが真になり、永遠に真であり続ける場合に真となります。これは、アルゴリズムが正しい結果で終了することを示すのに役立ちます。 [](P => <>Q)は、Pが真であるすべての状態に対して、Qが真である将来の状態が存在する場合に真となります。これは、Pが最終的にQを引き起こすこと、または「キューに入れられたすべてのメッセージが最終的にリーダーの履歴に含まれる」ことを示すことができます。 式の解析は少し混乱するため、P ~> Q（PはQにつながる）という糖衣構文があります。 ENABLEDや<<A>>_vのような他の演算子もあり、他のトリックを開きますが、チェックするものの大部分は不変条件、アクションプロパティ、ライブネスです。そして、それ自体がトピックである安全とライブネスの組み合わせであるリファインメントです。 TLA+でできないこと まず、明白なことから始めましょう。プロパティを論理式として表現する方法を知らない場合、TLA+は役に立ちません。他の形式手法も同様です。鳥という人間の概念を形式化できないなら、あなたのアプリが鳥を認識することを証明できません。そして残念ながら、私たちが気にする重要なプロパティの多くはこのカテゴリに分類されます。 次に、過度に具体的なもの。TLA+の安全プロパティは、個々の状態（不変条件）または単一ステップ（アクションプロパティ）のレベルで機能します。「削除を押してから元に戻すを押すと元の状態に戻る」とか、「電源を押したら、コンピューターが10ステップ以内にオンになる」といった、2つ以上のステップにわたるプロパティをネイティブに定義することはできません。また、浮動小数点演算や実時間ではなく、論理時間でのプロパティを定義することもできません。 次に、私が最も興味を持っている制限です。TLA+のプロパティは、すべての振る舞いに暗黙的に量化されます。[]Pをチェックすることは「すべての状態においてPが真である」ことを意味すると言いましたが、実際には「すべての振る舞いについて、[]Pはその振る舞いの初期状態において真である」ことを意味します。 TLA+がチェックできるシステムプロパティは、個々の振る舞いすべてにおいて真であるプロパティでなければなりません。それは何を残すのでしょうか？予想以上に多く！まず、「Pが真であるような振る舞い」は存在しません。したがって、実際に到達しなくても、Pが可能であるとは言えません。例としては、ゲームが勝てることを証明することが挙げられます。私たちはこれを到達可能性プロパティと呼びます。 より高度な到達可能性プロパティとしては、「すべての初期状態からPが到達可能である」とか、「Qが真である任意の Стейт からPが到達可能である」といったものがあります。 また、振る舞いのセット全体にわたるプロパティを定義することもできません。これはハイパープロパティと呼ばれます。例えば、電話のハードウェアをモデル化していて、省電力モードが常に通常モードよりもエネルギー消費が少ないことを検証したいとします。プロパティは「アクションの任意のシーケンスは、省電力モードで通常モードよりも多くの電力を消費しない」です。これを反証するには、1つは省電力モードで開始し、もう1つはそうでない、という2つの振る舞いを提供する必要があります。そして通常モードの方が電力が少なくなります。1つの振る舞いだけでは不十分なので、これはTLA+で自然にチェックすることは不可能です。ハイパープロパティはニッチに見えるかもしれませんが、多くのセキュリティプロパティやすべての統計プロパティ（「95パーセンタイル応答時間は5ms」）をカバーしています。 最後に、これは少し学術的ですが、状態空間全体にわたるプロパティを定義することはできません。例えば、状態Xから状態Yへのパスが1つしかないとは言えません。これが実際にどれほど役立つかはわかりません。これらの種類の「メタプロパティ」のほとんどは意味を持つ可能性がありますが、具体的に何であるかはわかりません。 「TLA+」が「できる」こと TLA+がこれらのことをできないと言ったのは、少し単純化しすぎました。それは、あなたが仕様を書いている場合、そしてその仕様があなたが構築したいシステムに直接対応している場合、TLA+はそのシステムプロパティとしてこれらを表現できないことを意味します。しかし、補助変数を使用して2ステップのプロパティを模倣することができます。例えば、すべての状態変更をstate_historyシーケンスに保存し、そのシーケンスに対する不変条件としてプロパティを定義します。自己構成を使用して一部のハイパープロパティを模倣できます。自己構成された仕様の各振る舞いは、実際のシステムの2つの振る舞いになります。 主要なTLA+モデルチェッカー（TLC）は、新しいREACHABLEキーワードを使用して最も基本的な到達可能性プロパティをチェックでき、TLCGetを使用して一部の状態空間プロパティをチェックできます。Andrew Helwerは、公平性と「マシンクロージャ」を使用して「常に到達可能」を模倣することについてのクレイジーな投稿をしています。これらは便利なハックですが、それでもハックです。それぞれに理解するための多くの巧妙さが必要であり、深刻な欠点が伴います。補助変数はリファインメントを台無しにし、s