"Program testing can be used to show the presence of bugs, but never to show their absence!"
—— Edsger W. Dijkstra (1970)
一、歸納法的局限
前面介紹的 TDD、屬性測試、靜態分析與多 Agent 審查，已經能攔截大部分工程缺陷。但從邏輯根基上看，測試始終屬於歸納法（Induction）。
正如 Dijkstra 所言：測試只能證明缺陷存在，無法證明缺陷不存在。
哪怕 Property-based test 隨機跑了十萬組極端輸入，也無法從數學上保證第十萬零一組輸入不會出錯。在航空航天、密碼學協議與金融清算核心這類零容錯場景中，單靠測試仍不夠穩妥。
要從「大概率沒錯」走向「數學上不可能出錯」，需要從歸納法轉向演繹法（Deduction），即形式化驗證（Formal Verification）。
二、形式化驗證的成本與 Lean 4
長期以來，形式化驗證主要停留在高校與少數高安全領域，難以在常規工程中普及。
傳統形式化工具門檻極高。Coq、Isabelle 等交互式定理證明器常要工程師用依值類型（Dependent Types）與一階邏輯手寫數千行證明腳本；TLA+ 主線則是規格與模型檢查，證明另走 TLAPS。成本往往是寫業務代碼本身的數倍。
現代證明語言 Lean 4 與 AI 的結合，開始改變這一成本結構。
Lean 4 既是定理證明器，也是高效自舉的函數式編程語言。基於「柯里-霍華德同構（Curry-Howard Isomorphism）」，規格即類型，程序即證明。函數的類型簽名定義了必須滿足的數學命題，函數體則是對該命題的構造性證明。
三、形式化內核：消除證明幻覺
AI 寫普通代碼時容易產生幻覺，甚至連測試一起偽造。但在 Lean 4 中，錯誤的推導無法通過編譯。
Lean 4 的**邏輯內核（Kernel）**體積很小，且經過嚴格審計。代碼進入內核做類型檢查（Type Check）時：
- 證明步驟只要有一處邏輯斷裂，內核就會直接報錯；
- 註釋裏的自然語言解釋或 Mock 手段對類型檢查無效；
- 每一步推導都必須符合形式公理，否則無法通過編譯。
不過內核只檢查推導是否合法，不檢查命題是否被繞過。Lean 允許用 sorry 跳過證明，也允許自定義 axiom，Agent 完全可能用一句 sorry 換取編譯通過。因此 CI 必須加入 #print axioms 檢查，一旦發現殘留的 sorry 或未經許可的自定義公理便直接阻斷。
這構成了一種清晰的分工：
人類定義數學不變量與業務規格（Spec）；
AI Agent 搜索證明戰術（Tactics），自動填補證明步驟；
Lean 內核在毫秒內完成校驗。
在這套閉環裏，AI 的角色收斂為受控的證明搜尋器。
四、新瓶頸：誰來驗證規格本身？
就算能用 Lean 4 讓 AI 寫出經數學嚴格證明的代碼，問題就徹底解決了嗎？
並沒有。形式化驗證只能證明「代碼符合規格」，無法證明「規格本身符合真實需求」。
這就是形式化方法的邊界：
- 你可以用 Lean 4 證明回贈計算在所有情況下都滿足你寫下的定理；
- 但如果定義定理時漏掉了某條業務排除條款；
- Lean 4 只會嚴格證明這段代碼百分之百符合那份錯誤的規格。
這再次回到 Fred Brooks 指出的問題：代碼實現與邏輯推導屬於次要複雜度，「決定系統到底要做甚麼」才是無法消除的本質複雜度。
五、小結
形式化驗證與 Lean 4 將代碼正確性的校驗交給了數學內核，消除了實現層面的隨機與幻覺。
但即便證明過程可以自動化，系統依然無法脫離人而運轉：誰來決定引入哪條公理？誰在衝突的業務訴求之間做取捨？系統在真實世界引發後果時，又由誰來負責？
最後一篇，我們回到整套工程體系中做決策的人。