你無法對分散式protocol做單元測試。單元測試在一台機器上以單一順序執行一個程序。而你的protocol在五台機器上以十個程序、以你無法控制的順序執行。這兩種現實之間的鴻溝，正是缺陷藏身之處。

模型檢驗彌補了這一鴻溝。它窮舉protocol可能到達的每一種狀態的所有可能交錯。如果存在兩份副本不一致的路徑、存在領導者選舉陷入deadlock的路徑、或存在 split-brain 出現的路徑，模型檢驗器都會發現它。而且是在你寫下第一個 RPC handler 之前就發現。

為什麼分散式缺陷能躲過傳統測試

問題出在狀態爆炸。三個節點交換訊息就可能產生數十億條執行路徑。手寫的整合測試也許只能覆蓋其中十幾條，通常是 happy path 和少數幾個明顯的故障模式。節點 A 恰好在傳送 prepare 和 ack 之間當機的缺陷？祝你在 CI 裡碰上它。

形式化驗證聽起來像是學術練習，但模型檢驗不同。你並非要證明protocol永遠正確。你用規約語言描述protocol，定義你關心的性質，然後讓工具在某一界限內窮舉狀態空間。一旦發現違反，它會給出最小反例追蹤。你會得到一份逐步重現缺陷的配方。沒有 heisenbugs，沒有「在我機器上能跑」。

最實用的工具是 Leslie Lamport 開發的 TLA+。它看起來像數學，因為它就是數學。但數學比你想的簡單，回報則是找到那些否則會在凌晨兩點於生產環境爆發的缺陷。

模型檢驗到底在做什麼

模型檢驗器接收三個輸入：系統描述、環境描述、以及你希望保持的性質。系統描述擷取protocol邏輯。環境描述擷取你無法控制的一切：網路延遲、訊息遺失、節點當機、時鐘偏移。性質通常是不變式（「已提交的日誌永不被覆蓋」）或活性條件（「每個請求最終都會得到回應」）。

然後檢驗器生成每一個可達狀態以及狀態之間的每一個合法轉移。對有限狀態空間它徹底窮舉，對無限空間則做有界探索。若不變式被違反，它停止並報告到達失敗的最短路徑。

這是暴力列舉，不是魔法。模型檢驗器不理解你的意圖。它只是嘗試一切。這正是關鍵所在。你的整合測試受你的假設左右。模型檢驗器沒有假設。

在 TLA+ 中規約一個簡單的共識protocol

來看一個最小範例：一個單法令共識protocol，領導者提出一個值，接受者的法定人數必須在值被選定前接受它。這是 Paxos、Raft 以及你聽過的所有其他共識演算法的核心思想。

以下是該系統的 TLA+ 規約：

------------------------------ MODULE Consensus ------------------------------
EXTENDS Integers, Sequences, FiniteSets

CONSTANTS Values, Acceptors, Quorum

VARIABLES chosen

Init == chosen = {}

Propose(v) ==
  /\\ v \\in Values
  /\\ chosen = {}
  /\\ chosen' = {v}

Next ==
  \\E v \\in Values : Propose(v)

Spec == Init /\\ [][Next]_chosen /\\ WF_chosen(Next)

ChosenUniqueness ==
  Cardinality(chosen) \\leq 1
=============================================================================

這份規約說明：最初沒有任何值被選定。一個 propose 動作可以將 chosen 設為單個值，但前提是截至目前沒有任何值被選定。ChosenUniqueness 不變式規定，任何時候被选定的值至多只有一個。

TLA+ 的模型檢驗器 TLC 會驗證沒有任何執行追蹤違反 ChosenUniqueness。如果你引入一個缺陷，讓兩個領導者可以在不檢查既有值的情況下同時提出，TLC 會在數毫秒內找到反例。

加入混亂的部分：當機與訊息遺失

上面的規約太乾淨了。真正的分散式系統並不乾淨。訊息會遺失。節點會重新啟動。網路分區會把一群節點彼此隔離。只有當你把這些故障也建模進來，模型才有用。

下面是一個更貼近現實的片段，對可能發生遺失的訊息傳遞進行建模：

VARIABLES msgs, acceptorState

Send(m) == msgs' = msgs \\cup {m}

Deliver(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ acceptorState' = [acceptorState EXCEPT ![m.to] = @ \\cup {m.value}]

Drop(m) ==
  /\\ m \\in msgs
  /\\ msgs' = msgs \\ {m}
  /\\ UNCHANGED acceptorState

Next ==
  \\E m \\in msgs : Deliver(m) \\/ Drop(m)

Drop 是重要的補充。它在不改變接受者狀態的情況下建模訊息遺失。TLC 會探索任何訊息被投遞、被丟棄或被無限期延遲的追蹤。當你加入領導者當機與恢復後，狀態空間會成長，但 TLC 仍會系統性地探索它。

這是我剛開始接觸 TLA+ 時被絆倒的地方。我只想建模protocol邏輯。但缺陷不在邏輯裡。它們藏在我沒有考慮到的邏輯與故障模式之間的交互作用中。你必須把兩者都建模。

權衡：狀態空間爆炸與抽象

模型檢驗不是免費的。狀態數量隨程序數與訊息負載大小呈指數增長。一個包含五個值和三個接受者的規約可能產生數百萬個狀態。加入第四個接受者，數量就躍升到數十億。在你的筆記型電腦上跑，記憶體會在完成之前耗盡。

解決方案是抽象。你不是對實際的 64 位元組值建模，而是對兩個值建模：V1 和 V2。如果protocol對兩個值表現正確，具體值就無關緊要。你不對一萬筆記錄的日誌建模，而是對深度為 2 的日誌建模。如果安全性對深度 2 成立，那它對任意深度幾乎總是成立。這被稱為 small-model checking，是該領域的標準做法。

關鍵技能在於學會區分哪些細節重要、哪些不重要。訊息內容對安全性通常不重要。訊息順序幾乎總是重要。節點身份也許不重要，但每個角色中的節點數量重要。

如果狀態空間仍然太大，你還有其他選擇。可以使用對稱性歸約，把相同的節點視為可互換。可以限制搜尋深度。或者換用符號模型檢驗器如 Apalache，它利用 SMT 求解器在不列舉所有狀態的情況下對狀態進行推理。

從規約到實作：保持同步

經過驗證的規約如果與實作背離，就毫無價值。規約是藍圖，程式碼是建築。兩者之間沒有自動橋樑，而縫隙正是缺陷重新潛入的地方。

務實的做法是把 TLA+ 規約當作一份恰好可執行的設計文件。在程式碼審閱時一併審閱它。當實作處理了一個邊界情況時，問問自己規約是否也處理了。當你在正式環境發現缺陷時，檢查規約本能否逮住它。如果不能，更新規約。

有些團隊更進一步，利用 TLC 產生的反例生成測試案例。一份展示兩份副本如何分歧的 TLC 追蹤，可以變成整合測試場景。這是手工活，但它把形式化模型與測試套件連接了起來。

在 Sentry，我們用這種方法驗證了一個分散式限流protocol。規約逮住了一個活性問題：某個恢復中的節點在特定分區場景下可能被餓死。我們的整合測試從未觸發過它，因為它們總是乾淨地修復分區。模型檢驗器不在乎乾淨。它嘗試了混亂的情況，發現了缺陷，讓我們避免了一場非常令人困惑的事故。

入門：你的第一次模型檢驗

如果你想嘗試，從 TLA+ Toolbox 開始。這是一款免費的 IDE，用於編寫和檢驗規約。跟著它自帶的 Paxos 和 Raft 範例練習。它們比上面的共識片段更複雜，但展示了真實protocol如何被建模。

對於你的第一份規約，從自己的系統中挑一個小東西。一個領導者選舉protocol。一個分散式快取失效方案。一個兩階段提交的變體。寫下你相信成立的不變式。然後讓 TLC 告訴你是否成立。答案通常是否定的，而且通常在一小時內就會告訴你。

模型檢驗不會找到所有缺陷。它對效能無能為力，抓不住序列化錯誤，也無法驗證實作是否與規約一致。它的作用是找到整合測試漏掉的深層protocol缺陷，而且在設計階段就找到，此時修復成本為零。

這才是分散式系統中最廉價的缺陷修復。不是更好的除錯器，不是更多的監控。而是在程式碼尚未存在之前就抓住缺陷。