インターネットがTLA+を発見した。さて、これからどうなる？

ホームについてブログキャリアブログ2026年9月25日インターネットがTLA+を発見した。さて、これからどうなる？Anna Mészáros, Szilvia Ujváry, Kseniia Strelbytska, Balázs Szilágyi, and Ferenc Huszár著Boris Cherny氏のバイラルなTLA+ツイートは、エージェントコーディングにおいて形式モデルがいかに有用であるかを示しました。この記事では、TLA+とは何かについて実践的な入門を提供します。 しかし、TLA+は単なる出発点にすぎません。私たちは、時間的仕様、現代的な証明システム、そしてAIエージェントが、システム動作のモデリングから機械チェック付き証明の生成、そして最終的には仕様、実装、検証が一体となったループへとどのように組み合わされるかについても見ていきます。また、Reasonableでの私たちの仕事の一部である、これを可能にするための簡単な紹介も行います。 Borisがツイートし、インターネットがコピーした 今週、Boris Cherny氏は、30年以上前の形式モデリングツールであるTLA+にツイートで光を当てました。彼はOpus 5.5を使用して、Claude Agent SDKの一部をTLA+とLeanでモデル化し、インターネットはいつものように反応しました：約100万回の視聴、数千件のブックマーク、そして人々はTLA+が実際には何であるかを尋ねています。Borisの投稿は素晴らしいショーケースであり、エージェントコーディングにおいてTLA+が努力する価値があることを示す初期の例に加わります。Datadogの「harness-first agents」に関する投稿を参照してください。 もしあなたが今、TLA+とは何か、そして何のためにあるのか疑問に思っている一人なら、あなたは正しい場所にいます。TLA+は、私たちのチームが深く掘り下げてきた形式手法の1つです。 しかし、私たちがそれに気にかけているのには、さらに大きな理由があります。TLA+は、システムが何を行うことが許可されているか、そしてシステムについて常にまたは最終的に真であるべきこと、を記述するためのコンパクトな言語を提供します。それは検証のための有用な出発点ですが、それが物語の終わりではありません。 以下は短いバージョンです： TLA+は、可能なシステム動作と、それらの動作が満たすべきプロパティを記述します。 TLA+自体は、実装を完全に検証するわけではありません。それはソフトウェアそのものではなく、ソフトウェアのモデルをチェックし、その主なモデルチェッカーは有限なインスタンスのみを探索します。 現代的な証明システムは、私たちをさらに進めることができます。Verusでは、仕様、証明、そしてRust実装が同じ言語で共存できます。 AIはすでにこのプロセスの部分を自動化できます。私たちは、16,000以上のTLA+仕様/プロパティペアを3,000以上の機械チェック付きVerus証明に変換するエージェントパイプラインを構築しました。 したがって、興味深い質問は、エージェントがTLA+を書けるかどうかだけではありません。それは、エージェントが仕様、証明、そして実際のプログラム間を移動できるようになると、何が可能になるかということです。 Reasonableでの私たちの仕事の一部は、エージェントがこれを一貫して、信頼性高く、迅速に行えるようにモデルをトレーニングすることです。 TLA+とは何か 私たちの継続的な例は、以下のインタラクティブプレイグラウンドにあります。ここでは、3台のコンピュータa、b、cが、自分たちのうちのどれがリーダーであるかに合意しなければなりません。データベースは、リーダー選出が正しいことに依存しています。私たちは、同時に2人のリーダーが存在しないことを要求します。プレイグラウンドをクリックして、ゲームの5つのレベルを通じてTLA+の基本を学ぶことができます。 プレイグラウンドを開く↗ TLA+ (Temporal Logic of Actions) は、2種類のオブジェクトを書き出すための言語です： 遷移システム：システムができること。状態（誰が候補者か、誰が誰に投票したか、誰がリーダーか）と、状態を変化させる単一のステップ（「aが選挙を開始する」、「bがaに投票する」）があります。インタラクティブプレイグラウンドでは、テスターのように、手でこれらのステップを実行して、1つの可能な実行を探索します。 時間的プロパティ：実行が時間とともにどのように展開されるかについてのステートメント。例えば、「決して2人のリーダーが存在しない」。「リーダーは最終的に選出される」。 TLA+モデルは、合法的なシステム状態と、それらの状態間の許可された遷移を宣言します。例えば、選挙では、a、b、またはcのいずれかが初期状態から選挙を開始し、その過程で自分自身に投票することができ、bはaまたはcに投票できます。 それは遷移の順序を強制せず、異なるイベントが発生する確率分布をモデル化しようとしません。これは分散システムにとって正しい抽象化であり、メッセージ、タイムアウト、ユーザーアクションは多くの異なる順序で発生する可能性があります。 基盤となる数学は単純で、集合、真偽ステートメント、関係を使用します。時間的プロパティは、実行に対する演算子から構築されます： □ P (常に P)：Pは訪問されたすべての状態で真です。 ◇ P (最終的に P)：Pは将来のある時点で真です。 P ⇝ Q (P は Q を導く)：Pが真であるときはいつでも、Qはその後最終的に真になります。 特に重要な2種類のプロパティがあります。 安全性：悪いことは決して起こらない。私たちの選挙では：「□ (決して2人のリーダーが存在しない)」。プレイグラウンドでは、モデルチェッカーはすべての可能な状態を探索します。3台のコンピュータでは38の状態、9台では100万以上です。任意のシステムサイズに対してプロパティを確立するには、証明が必要です。レベル2では、コンピュータが2回投票できるようなルールを1つ変更します。チェッカーはその後、2人のリーダーで終わる6ステップの実行を返します。その実行は反例です：モデルがプロパティに違反する具体的な方法です。 ライブネス：良いことは最終的に起こる。安全性だけでは不十分です。何も永遠に起こらないシステムは完全に安全です。したがって、次のようなことも要求するかもしれません：「◇ (誰かがリーダーである)」。レベル3は、これがなぜ重要かを示しています：タイプミスが何も起こらないようにし、安全性チェックは依然としてパスします。ライブネスは公平性の仮定を必要とし、アクションが可能なままであっても決して実行されない実行を排除します。弱い公平性 WF(A) は、有効になったアクションは最終的に発生しなければならないことを意味します。強い公平性 SF(A) は、無限回有効になったアクションをカバーします。 メンタルモデルは単純です：TLA+モデルは、システムの可能な実行トレースを記述し、プロパティはどのトレースが許容されるかを記述します。検証は、すべての可能なトレースが許容されるかどうかを尋ねます。 TLC、標準のTLA+モデルチェッカーは、有限インスタンスの到達可能な状態を列挙することによってこれに答えます。証明は、プロパティが一般的に真であるというより強力なステートメントを作成します。 詳細については、Jack Vanlightlyがエージェントが流行するずっと前から彼のブログでTLA+を教えています。 TLA+ではないもの TLA+は、システムに関するこの推論方法が実用的に役立つため、ますます広く展開されています。AWS、MongoDB、Datadog、Kafkaなどで使用されていますが、TLA+だけでは完全なソフトウェア検証には至らない3つの重要な注意点があります。 モデルチェックは限界がある。実際には、人々はTLA+をTLCと組み合わせて最も頻繁に使用します。TLCはすべての可能な実行を探索しますが、有限モデルに対してのみです。私たちの例では、状態空間は3台のコンピュータでは38の状態から、9台では100万以上に増加します。任意のシステムサイズに対してプロパティを確立するには、証明が必要です。TLA+自体のプロバーであるTLAPSは、一部のケースでこれを実行できますが、特にライブネスの議論においては、その自動化は限定的です。 モデルは実装ではない。TLA+仕様は通常、ソフトウェアの独立したモデルです。実装がモデルと正確に動作することを自動的に保証するものはなく、コードが変更されるにつれて両者は乖離する可能性があります。これは、仕様から実装へのギャップという古典的な要素の1つです。 TLA+は、私たちが望むすべてのプロパティを表現できるわけではありません。TLA+は線形時間論理に基づいており、個々の実行に関するステートメントを作成します：「すべての実行において、リーダーは最終的に選出される」。しかし、いくつかの興味深いプロパティは、代替の未来や戦略に関係します。CTL、分岐時間論理は、「どの状態からでも、新しい選挙を開始できる」といったステートメントを表現できます。ATLは、「他のコンピュータが何をしてもリーダーになる戦略をこのコンピュータは持っている」といった戦略的なステートメントを表現できます。 これらのより豊かなプロパティは、複数の競合または協力エージェントを含むシステムを考え始めると関連性が高まります。 したがって、TLA+は時間的動作を記述するための異常に有用な言語を提供しますが、完全な検証スタックにはさらに多くのものが必要です：より強力な証明メカニズム、実際のコードへの接続、そして最終的にはより豊かな論理。 TLA+から証明へ 1つのルートは、モデルを現代的な証明システムに取り込むことです。いくつかの選択肢があります。例としては以下のようなものがあります： Leanはインタラクティブです：あなた（またはAI）が証明をステップバイステップで記述します。それは非常に一般的で、数学で広く使用されており、証明は...