2026-10-01 — TLA+ 不能表達的性質：可達性與超性質

TLA+ 不能表達的性質：可達性與超性質

Hillel Wayne, Computer Things · 2026-09-30

TLA+ 的每一個性質都隱含「對所有 behavior 成立」，所以凡是需要「存在某條 behavior」或「比較多條 behavior」的性質，它原生就寫不出來。Hillel Wayne 在 9 月 30 日的文章裡提醒：「用 TLA+ 替 AI 寫的程式把關」這個說法正在升溫，但你得先有一條寫得出來的性質可以驗。

起因是他文中提到，Claude Code 的作者 Boris Cherny 說 Opus 能用 TLA+ 找出程式碼裡的 race condition，之後網路上就滿是「形式化驗證能一次解決 agent 寫程式問題」的討論。

TLA+ 能檢查什麼

TLA+ 把系統看成一組 behavior，每條 behavior 是一串 state。能寫的性質由三個時序運算子組合而成：[]P（always）、P'（下一個 state）、<>P（eventually）。

invariant：[](at_most_one_green)，每個 state 都成立。
action property：[](x' >= x)，每一步都不能讓 x 變小。
liveness：[]<>P、<>[]P、P ~> Q，涵蓋 leader election 最終收斂、訊息最終被讀到這類需求。

invariant 與 action property 屬於 safety（壞事不會發生），liveness 則是好事終究會發生。Wayne 認為這三類加上 refinement，涵蓋了日常檢查的大多數需求。

寫不出來的三類性質

文中先列出兩個比較表面的限制：單一 state 或單一步以外的多步性質寫不出來，例如「按下 delete 再 undo 會回到原狀」或「按下電源後十步內開機」；浮點運算與真實時間也無法表達，只有邏輯時間。

他真正關心的是「性質隱含對所有 behavior 量化」這條限制，它擋掉三類東西：

類別	想說的話	為什麼寫不出來
reachability	「遊戲有可能過關」「使用者永遠可以改密碼」	需要「存在一條 behavior」，而 TLA+ 只有「對所有」
hyperproperty	「省電模式耗電一定不高於一般模式」	要比較兩條 behavior，單一 behavior 無法反證
state space 整體性質	「從 X 到 Y 只有一條路徑」	性質不是針對單一 behavior

Wayne 特別指出 hyperproperty 並不冷門：許多資安性質與所有統計性質都屬於這一類，例如「95 百分位回應時間為 5ms」。

繞路做法與代價

這些限制有 hack 可以繞。用輔助變數把狀態變化存成 state_history 序列，再對序列寫 invariant，可以模擬多步性質；用 self-composition 讓一個 behavior 代表系統的兩條 behavior，可以模擬部分 hyperproperty。

代價他也寫得直接：輔助變數會破壞 refinement，self-composition 讓 state space 指數膨脹，而且模型會變得怪異，與實際系統對不上。換工具也是一條路，例如 CTL 可處理 reachability、PRISM 處理機率性質，但它們在 TLA+ 擅長的地方比較弱，且同樣無法處理無法形式化的性質。

TLC 的進展

文中說主要的模型檢查器 TLC 已可用新的 REACHABLE 關鍵字檢查最基本的 reachability，並以 TLCGet 檢查部分 state space 性質。對應的提案 tlaplus/tlaplus#860（Feature proposal: REACHABLE invariant type）由 Andrew Helwer 於 2024-01-10 提出，掛在 1.8.0 milestone，並於 2026-05-13 關閉。

Helwer 在 9 月 26 日的文章補充了邊界：這類檢查仍是 beta，在模型檔中寫成 _POSSIBLE P，檢查的是「從初始 state 出發，P 是否至少被某條 behavior 滿足過」，不是「從每個 state 出發都到得了 P」。兩篇文章對關鍵字的稱呼不同（REACHABLE 與 _POSSIBLE），實際用哪個請以你安裝的 TLC 版本文件為準，本文無法確認。

\* 單步可達：TLC 今天就能檢查
[](ENABLED Next /\ P')

\* 多步可達：Lamport 的寫法，TLC 目前無法檢查
[](ENABLED [Next]_v^+ /\ P')

完整的「每個 state 都到得了 P」，Helwer 認為可在 state graph 探索完之後，加一個從滿足 P 的 state 反向 BFS 的獨立 pass 來做，但目前尚未實作。

影響範圍

正在用 LLM 產生並 review 並發程式、同時打算靠 TLA+ 當安全網的團隊，要先列出自己的需求是 safety、liveness，還是上表那幾類。「任何時候都能關機」「使用者一定能重設密碼」這類可用性需求，純 invariant 與 liveness 蓋不到，要改用 REACHABLE／_POSSIBLE 當 spec 的單元測試，或接受繞路 hack 的成本。

資安與效能 SLO 類的需求多半是 hyperproperty，別預期 TLC 直接幫你驗證；Wayne 原文也強調，即使模型正確，正確的設計不會自動變成正確的程式碼，這是另一個獨立的落差。

補充：Cherny 的說法只見於 Wayne 文中引述，本文未另行查證。

原始來源：Hillel Wayne 原文、tlaplus#860、Helwer：Can we have reachability properties in TLA+?

End of article