Boris Cherny 的 TLA+ 病毒式推文展示了形式化模型在代理式編碼中的巨大潛力。本文將提供 TLA+ 的實用入門介紹。但 TLA+ 僅是起點。我們也將探討時序規範、現代證明系統和 AI 代理如何結合，從建模系統行為到生成機器驗證的證明，最終實現軟體在一個循環中被指定、實現和驗證。我們還將搶先預覽 Reasonable 在實現這一目標方面的一些工作。
本週，擁有 30 多年歷史的形式化建模工具 TLA+，因 Boris Cherny 的一則推文而聲名大噪。他使用 Opus 5.5 以 TLA+ 和 Lean 對 Claude Agent SDK 的部分內容進行了建模，網路也隨之沸騰：約 100 萬次觀看、數千次收藏，人們紛紛詢問 TLA+ 究竟是什麼。Boris 的貼文是一個絕佳的展示，也為早期證明 TLA+ 在代理式編碼中物有所值的例子增添了新的註腳：請參閱 Datadog 關於 harness-first agents 的貼文。如果您也是現在好奇 TLA+ 是什麼以及它的用途的人之一，那麼您來對地方了。TLA+ 恰好是我們團隊深入研究的形式化技術之一。但我們關心它還有更大的原因。TLA+ 為我們提供了一種簡潔的語言，用來描述系統允許做什麼，以及系統必須始終或最終為真的性質。這是驗證的有用起點，但並非故事的結局。以下是簡短的版本：
TLA+ 描述了系統的可能行為以及這些行為應滿足的性質。
TLA+ 本身並不完全驗證實作。它檢查的是軟體的模型，而不是軟體本身，而且其主要的模型檢查器僅探索有限的實例。
現代證明系統可以帶我們走得更遠。在 Verus 中，規範、證明和 Rust 實作可以存在於同一語言中。
AI 已經可以自動化這個過程的一部分。我們建立了一個代理式管線，將 16,000 多對 TLA+ 規範/性質轉換為 3,000 多個機器驗證的 Verus 證明。
Reasonable 的部分工作是訓練模型，使代理能夠一致、可靠、快速地完成這項工作。
我們的範例是下方互動式遊樂場中的例子，其中三台電腦 a、b 和 c 必須就誰是領導者達成一致。資料庫依賴於領導者選舉的正確性。我們要求不能同時存在兩個領導者。您可以點擊遊樂場來透過五個遊戲關卡學習 TLA+ 的基礎知識。
TLA+（Temporal Logic of Actions，時序邏輯）是一種用於撰寫兩種物件的語言：
一個轉換系統：系統能做什麼。有狀態（states），即系統的快照（誰是候選人、誰為誰投票、誰是領導者），以及動作（actions），即改變狀態的單一步驟（「a 開始選舉」、「b 為 a 投票」）。在互動式遊樂場中，您可以手動執行這些步驟，像測試人員一樣探索一種可能的執行流程。
時序性質（Temporal properties）是關於執行流程隨時間如何展開的陳述。例如，「永遠不會有兩個領導者。」「最終會選出一位領導者。」
TLA+ 模型聲明了合法的系統狀態以及這些狀態之間的允許轉換。例如，在選舉中，a、b 或 c 中的任何一個都可以從初始狀態開始選舉，並為自己投票，而 b 可以為 a 或 c 投票。它不對轉換施加順序，也不試圖模擬不同事件發生的機率分佈，這對於分散式系統來說是正確的抽象，因為訊息、超時和使用者動作可能以多種不同順序發生。底層數學很簡單，它使用集合、真假陳述和關係。時序性質然後從執行上的運算子構建：
□ P（總是 P）：P 在每個訪問的狀態中都成立。
◇ P（最終 P）：P 在未來的某個狀態中成立。
P ⇝ Q（P 導致 Q）：每當 P 成立時，Q 最終會成立。
兩種性質尤其經常被提及。安全性（Safety）：壞事永遠不會發生。對於我們的選舉：「□（永遠不會有兩個領導者）」。在遊樂場中，模型檢查器會探索所有可能的狀態：三台電腦共有 38 個狀態，並確認該性質。第二級改變了一個規則，允許一台電腦投票兩次。檢查器隨後會返回一個六步執行的流程，最終導致兩個領導者。該執行是一個反例：模型違反性質的一種具體方式。活性（Liveness）：好事最終會發生。僅有安全性是不夠的。一個永遠不做事的系統是完全安全的。因此，我們也可能需要：「◇（有人是領導者）」。第三級展示了這為何重要：一個拼寫錯誤導致任何事情都無法發生，而安全性檢查仍然通過。活性需要公平性假設，這排除了永遠可能發生但就是不被採取的執行。弱公平性 WF(A) 表示一個始終可用的動作最終必須發生；強公平性 SF(A) 涵蓋了無限次可用的動作。心智模型很簡單：TLA+ 模型描述了系統的可能執行軌跡，而性質描述了哪些軌跡是可以接受的。驗證詢問的是每個可能的軌跡是否都可以接受。標準的 TLA+ 模型檢查器 TLC，透過枚舉有限實例的可達狀態來回答這個問題。證明則做出更強的陳述，即該性質普遍成立。更多資訊，Jack Vanlightly 在代理程式使其流行之前，就已在他的部落格上教授 TLA+。
TLA+ 被越來越廣泛地部署，因為這種推理系統的方式在實務上非常有用；您會在 AWS、MongoDB 和 Datadog、Kafka 以及許多其他地方看到它的應用。但有三個重要的注意事項，TLA+ 本身在完全的軟體驗證方面有所不足。
模型檢查只能走這麼遠。實際上，人們最常將 TLA+ 與 TLC 一起使用。TLC 會探索所有可能的執行流程，但僅限於有限的模型。在我們的例子中，狀態空間從三台電腦的 38 個狀態增長到九台電腦的超過一百萬個狀態。要為任意系統大小建立一個性質，您需要一個證明。TLA+ 自身的證明器 TLAPS 在某些情況下可以做到這一點，但其自動化程度有限，尤其是在活性論證方面。
模型不是實作。TLA+ 規範通常是軟體的獨立模型。沒有什麼能自動保證實作的行為與模型完全一致，而且隨著程式碼的變更，兩者可能會逐漸偏離。這是經典的規範到實作差距的一個要素。
TLA+ 無法表達我們可能想要的所有性質。TLA+ 基於線性時序邏輯，它對個別執行進行陳述：「在每次執行中，最終都會選出一位領導者。」但一些有趣的性質涉及替代的未來或策略。
CTL，一種分支時間邏輯，可以表達諸如「從任何狀態，仍然可以啟動新的選舉」之類的陳述。
ATL 可以表達策略性陳述，例如「這台電腦擁有無論其他電腦怎麼做都能成為領導者的策略。」
當我們開始考慮包含多個競爭或協作代理的系統時，這些更豐富的性質就變得相關了。因此，TLA+ 為我們提供了一種異常有用的描述時序行為的語言，但一個完整的驗證堆疊需要更多：更強大的證明機制、與真實程式碼的連結，以及最終更豐富的邏輯。
一種方法是將模型導入現代證明系統。有幾種選擇，例如：
Lean 是互動式的：您（或 AI）逐步編寫證明。它非常通用，廣泛用於數學領域，並且是 Boris 貼文中使用的證明器。
Verus 是自動化的，並且圍繞 Rust 設計。您提供規範和重要的證明結構，而自動化求解器則處理大部分低階推理。
Veil 是一個基於 Lean 的工具，專門為狀態機模型構建。Leo de Moura 推薦了它，最近它被用來驗證一個同步引擎，在此過程中修復了 17 個錯誤。然而，活性仍然是未來的工作，並且驗證的模型仍然獨立於實作。
為什麼使用 Verus？因為規範和證明可以與真實的 Rust 實作並存。這很重要，因為它為我們提供了一條縮小規範到實作差距的途徑：我們不必僅僅證明一個獨立的抽象模型的性質，而是最終可以證明實作細化了該模型。Anvil 等系統已經展示了這種驗證風格；我們在 Reasonable 的工作尤其緊密地建立在 Anvil 的基礎上。
為什麼要自動化形式驗證？涉及的證明通常不像形式驗證這個詞所暗示的那樣奇特。
安全性證明通常是歸納式的。證明該性質最初成立，然後證明每個可能的動作都保留了它。大部分工作包括分解到不同的動作，並追蹤相關的不變量。
活性證明建立進度。通常，隨著系統的進展，某個數量會減少，再加上公平性假設，排除了永遠延遲一個可用動作的執行。WF1、WF2、SF1 和 SF2 等規則封裝了這些論證；我們的時序函式庫將它們實現為已證明的 Verus 引理。
這項工作中有很大一部分是重複性的：追蹤不變量、分解到動作、提供中間引理以及填寫求解器可見的細節。這使其成為證明生成代理的自然目標。
自動定理證明最近在數學領域取得了快速進展。軟體驗證提出了略有不同的問題：在證明任何東西之前，我們需要對軟體預期做什麼有一個有用的描述。TLA+ 在這裡很有吸引力，因為時序規範相對緊湊且易於閱讀，而且因為許多實際系統已經有 TLA+ 模型。如果我們能將這些模型與現代證明系統和實作聯繫起來，就有幾種可能的方向。
細化證明（Refinement proofs）。證明 Rust 實作遵循 TLA+ 模型。Anvil 手動展示了這一點。自動化這個過程的更多部分將減少驗證模型與驗證實作它的軟體之間的差距。
程式合成（Program synthesis）。從模型開始，生成一個實作以及一個證明該實作細化了模型的證明。在此設定下，形式規範約束了程式碼生成和驗證。
協定搜尋（Protocol search）。一旦檢查候選協定的成本足夠低，驗證器就可以成為目標函式：生成協定的變體，驗證它們，並保留滿足所需性質的變體。這開始看起來類似於 AlphaEvolve 等系統，除了正確性是透過形式檢查而不是透過測試估計的。
超越線性時間（Beyond linear time）。多代理系統的某些性質涉及替代的未來或策略，而不是個別的執行軌跡。表達這些需要超越 LTL 的邏輯。Benjamin Brast-McKie 的工作探索了這個問題的這一方面，而我們目前的工作則專注於證明時序性質並將它們與程式碼連結。
我們一直在開發一個將 TLA+ 規範轉換為機器驗證 Verus 證明的管線。我們接下來的部落格文章將更詳細地描述各個部分。目前，主要結果是：
一個 TLA+ 到 Verus 的轉譯器。我們建立了一個演算法轉譯器，並將其與一種代理式替代方案進行了比較，在該替代方案中，一個 LLM 產生翻譯，第二個 LLM 進行審查。
一個帶有反作弊檢查的證明器-審查器循環。一個代理編寫證明，另一個代理審查它。一個獨立的守門員檢查代理是否修改了規範或引入了捷徑，例如 assume(false)。
一個 Verus 中的時序證明資料集。從 16,459 對真實世界的 TLA+ 規範/性質對開始，該管線產生了超過 3,000 個機器驗證的安全性和活性證明。我們還構建了一個包含 40 個任務的評估集。
對當前模型的評估。我們在評估集上測試了封閉式和開放權重的邊緣模型，考察了它們可以完成哪些時序證明以及剩餘的失敗模式在哪裡。
我們將在後續文章中介紹這些結果。
我們正在招聘對推動形式驗證和 AI 代理的邊界充滿熱情的人才。如果您想幫助構建可以機器驗證正確性的系統，我們很樂意與您聯繫：Careers。我們也渴望與構建正確性至關重要的系統的團隊聯繫。我們正在探索機器驗證的證明可以為實際應用解鎖什麼，我們很樂意與您交流：Contact。
