eSpark 用 TLA+ 證明沒有任何設計能同時滿足全部 3 條規則，於是捨棄其中一條

eSpark Learning 是一家為小學提供服務的教育科技供應商，它為每一位客戶執行一套手動、半定期性的設定流程，這套流程要協調多個第三方系統，並直接修改客戶的 IT 網路。隨著使用者規模成長，這樣的工作量變得難以為繼——支援團隊意識到，光是維持現狀，每年就得增聘一名全職人員。管理層一向認為把這套流程自動化太過危險：一個失誤就可能動到客戶的網路，導致合約不保。

工程師 Hillel Wayne 不久前才在一個批次上傳專案上採用形式化規格（TLA+ 風格），在寫程式之前就抓到架構缺陷，讓交付時間縮短了一週。專案經理已定義出這套自動化替代方案為了確保安全而必須保證的三項性質。Wayne 以一種規格語言為系統建立模型，並透過模型檢查器執行，該檢查器會窮盡模擬規格所允許的每一種情境，一旦找到違反規則的情境，就回傳具體的執行軌跡。

經過兩天的建模，每一種設計不是立刻出錯，就是含有某個隱微缺陷，可能在正式環境中潛伏數月而無人察覺，直到最後崩潰。有些設計滿足了三項必要性質中的兩項，但沒有任何一種能同時滿足全部三項。Wayne 並沒有隨便挑一種然後祈禱它行得通，而是把專案經理帶進建模的產出之中，具體展示每一種設計會如何失敗，並詢問業務端哪一項性質是可以割捨的。

內部設計專家判定，其中一項性質只需要「通常」成立，而不必「總是」成立。把這唯一的取捨範圍縮小之後，模型檢查器確認有幾種設計如今可行，團隊便著手打造其中一種。這套自動化設定服務此後運作多年、毫無事故，存續時間甚至超過打造它的工程師們的任期。

模型檢查器證明沒有任何設計能同時滿足全部 3 條規則；協商

以規格語言建模的成本很低，丟掉也無妨；一套大致成形的程式碼庫則不然，因此在實作之前先測試每一種設計構想，避免了浪費工程時間。

模型檢查器會回傳具體的失敗軌跡，對非工程師的利害關係人而言，這比抽象的風險警告更具說服力。

在寫程式之前就揭露「這些設計沒有一種能滿足全部三項需求」，把一個隱含、未經檢視的假設，轉變成專案經理真正能做的明確決策。

當你嘗試的每一種設計似乎都行不通時，先以形式化方式為整個設計空間建模。模型檢查器能把模糊的風險感，轉化為具體、可協商的取捨，讓你在寫下任何一行程式碼之前就能提出來。

這套自動化設定管理服務高效運作多年，遠遠超過打造它的工程師們的任期。Wayne 後來成為全職的形式化規格顧問，並撰寫相關實務文章，包括一本關於這個主題的書，以及為 Alloy 規格語言撰寫文件的工作。