首頁

快訊深度數據 Skill&API

Vitalik最新長文：AI時代，程式碼如何變得更安全？

閱讀本文需 47 分鐘

當AI開始自動尋找bug，V神給出的答案是「形式化驗證」

原文標題：淺談形式化驗證

原文作者：Vitalik

編譯：Peggy，BlockBeats

編者按：隨著 AI 編程能力快速提升，軟體安全正面臨一個新的悖論：AI 可以更高效地生成程式碼，也可以更高效地發現漏洞。對加密行業而言，這一問題尤其關鍵。智能合約、ZK 證明、共識演算法和鏈上資產系統一旦出現缺陷，後果往往不是普通軟體報錯，而是不可逆的資金損失和信任崩潰。

Vitalik 在本文中討論的，正是 AI 時代程式碼安全的另一條路徑：形式化驗證。簡單來說，它不是依賴人類稽核員逐行檢查程式碼，而是把程式應當滿足的性質寫成數學命題，再用機器可檢查的證明去驗證這些性質是否成立。過去，形式化驗證因門檻高、過程繁瑣，一直停留在相對小眾的研究和工程領域；但隨著 AI 能夠輔助編寫程式碼和證明，這套方法正在重新獲得現實意義。

文章的核心判斷並不是「形式化驗證可以解決一切安全問題」。相反，Vitalik 反复提醒，所謂「可證明安全」並不等於絕對安全：證明可能遺漏關鍵假設，規範本身可能寫錯，未被驗證的程式碼、硬體邊界和側信道攻擊也可能成為新的風險來源。但它依然提供了一種更可靠的安全範式：用多種方式表達開發者的意圖，再讓系統自動檢查這些表達是否彼此兼容。

這對以太坊尤為重要。未來的以太坊將越來越依賴複雜底層組件，包括 STARK、ZK-EVM、抗量子簽名、共識演算法和高性能 EVM 實現。這些系統的實現極其複雜，但其核心安全目標往往可以被相對清晰地形式化。也正是在這類場景中，AI 輔助形式化驗證有可能發揮最大價值：讓 AI 負責編寫高效程式碼和證明，讓人類負責檢查最終被證明的命題是否真的對應自己想要的安全目標。

從更宏觀的角度看，這篇文章也是 Vitalik 對 AI 時代網路安全的一次回應。面對更強的 AI 攻擊者，答案不是放棄開源、放棄智能合約，或重新依賴少數中心化機構，而是把關鍵系統壓縮成更小、更可驗證、更可信的「安全核心」。AI 會讓粗糙程式碼大量增加，但也可能讓真正重要的程式碼變得比過去更安全。

以下為原文：

特別感謝 Yoichi Hirai、Justin Drake、Nadim Kobeissi 和 Alex Hicks 對本文提供反饋與審閱。

過去幾個月裡，一種新的編程範式正在以太坊前沿研發圈以及計算領域的許多其他角落迅速興起：開發者直接使用非常底層的語言編寫代碼，例如 EVM 字節碼、彙編語言，或使用 Lean 編寫代碼，並通過在 Lean 中撰寫可自動檢查的數學證明來驗證其正確性。

如果運用得當，這種方式既有可能生成極其高效的代碼，也可能比過去的軟體開發方式安全得多。Yoichi Hirai將其稱為「軟體開發的最終形態」。本文將嘗試解釋這套方法背後的基本邏輯：軟體的形式化驗證到底能做什麼，它的短板和邊界又在哪裡——無論是在以太坊語境中，還是在更廣泛的軟體開發領域。

什麼是形式化驗證？

形式化驗證，指的是以一種可以被機器自動檢查的方式，撰寫數學定理的證明。

為了給出一個相對簡單、但仍然有趣的例子，我們可以看一個關於斐波那契數列的基本定理：每三個數中就有一個偶數，其餘兩個則是奇數。

一個簡單的證明方法是使用數學歸納法，每次向前推進三個數。

首先看基礎情形。令 F1 = F2 = 1，F3 = 2。通過直接觀察可以看出，這一命題——「當 i 是 3 的倍數時，Fi 為偶數；其他情況下，Fi 為奇數」——在 x = 3 之前都是成立的。

接下來是歸納步驟。假設該命題在 3k+3 之前都成立，也就是說，我們已經知道 F3k+1、F3k+2、F3k+3 的奇偶性分別是奇數、奇數、偶數。於是，我們可以計算下一組三個數的奇偶性：

由此，我們就完成了從「已知命題在 3k+3 之前成立」，到「確認命題在 3k+6 之前也成立」的推導。只要不斷重複這一推理，就可以確信這條規律對所有整數都成立。

這個論證對人類來說是有說服力的。但如果你想證明的東西複雜一百倍，而且你真的非常想確認自己沒有犯錯，該怎麼辦？這時，你就可以構造一個能讓計算機也信服的證明。

它大致會長這樣：

這是同樣的推理，只不過用 Lean 表達出來。Lean 是一種常被用於撰寫和驗證數學證明的編程語言。

它看起來和我上面給出的「人類版」證明很不一樣，這背後有充分理由：對計算機來說直觀的東西，和對人類來說直觀的東西完全不同。這裡說的計算機，是舊意義上的「計算機」——由 if/then 語句構成的「決定性」程序，而不是大語言模型。

在上面的證明中，你並不是在強調 fib(3k+4) = fib(3k+3) + fib(3k+2) 這一事實；你強調的是 fib(3k+3) + fib(3k+2) 是奇數，而 Lean 中那個名字相當宏大的 omega tactic，會自動把這一點和它對 fib(3k+4) 定義的理解結合起來。

在更複雜的證明中，你有時必須在每一步都明確說明：到底是哪一條數學定律允許你走出這一步，而且這些定律有時還帶著一些晦澀的名字，比如 Prod.mk.inj。但另一方面，你也可以一步展開巨大的多項式表達式，並且只需要寫一行如 omega 或 ring 這樣的表達式，就能完成論證。

這裡的不直觀和繁瑣，正是機器可驗證證明雖然已經存在近 60 年，卻一直停留在小眾領域的重要原因。但與此同時，許多過去幾乎不可能的事情，如今正因為 AI 的快速進展而迅速變得可行。

驗證計算機程序

到這裡，你可能會想：好吧，所以我們可以讓計算機驗證數學定理的證明，這樣我們終於能確定，那些關於素數之類的瘋狂新發現，到底哪些是真的，哪些只是藏在上百頁 PDF 論文裡的錯誤。也許我們甚至還能弄清楚望月新一關於 ABC 猜想的證明到底是否正確！但除了滿足好奇心之外，這件事又有什麼實際意義呢？

答案可以有很多。而對我來說，一個非常重要的答案是：驗證計算機程序的正確性，尤其是那些涉及密碼學或安全性的程序。畢竟，計算機程序本身就是一個數學對象。因此，證明一個計算機程序會以某種方式運行，本質上就是在證明一個數學定理。

举个例子，假设你想证明 Signal 这样的加密通信软件到底是否真正安全。你可以先用数学方式寫清楚，在這個語境下，「安全」到底是什麼意思。概括來說，你要證明的是：在某些密碼學假設成立的前提下，只有擁有私鑰的人，才能獲知消息內容的任何信息。現實中，真正重要的安全屬性當然有很多種。

而事實證明，確實已經有一個團隊正在嘗試弄清楚這件事。他們提出的其中一個安全定理，大致長這樣：

以下是 Leanstral 對這一定理涵義的總結：

passive_secrecy_le_ddh 定理是一個緊湊歸約，表明在隨機預言機模型（Random Oracle Model）下，X3DH 的被動消息保密性至少和 DDH 假設一樣難以攻破。

換句話說，如果攻擊者能夠攻破 X3DH 的被動消息保密性，那麼他們同樣也能攻破 DDH。由於 DDH 通常被假定為困難問題，因此 X3DH 也可以被認為能夠抵禦被動攻擊。

該定理證明，如果攻擊者只能被動觀察 Signal 的密鑰交換消息，那麼他們無法以超過可忽略概率的優勢，將最終生成的會話密鑰與一個隨機密鑰區分開來。

如果再結合一個證明，說明 AES 加密被正確實現，那麼你就可以得到一個證明：Signal 協議的加密機制能夠抵抗被動攻擊者。

類似的驗證專案也已經存在，它們用於證明 TLS 以及其他瀏覽器內密碼學組件的安全實現。

如果你能做到端到端的形式化驗證，那麼你證明的就不只是某個協議描述在理論上是安全的，而是使用者實際運行的那段具體程式碼在實踐中也是安全的。從使用者角度看，這會大幅提升「無需信任」的程度：為了完全信任這段程式碼，你不需要逐行檢查整個程式庫，只需要檢查已經被證明成立的那些陳述。

當然，這裡有一些非常重要的星號需要保留，尤其是關於「安全」這個關鍵字到底意味著什麼。人們很容易忘記去證明真正重要的主張；也很容易遇到這樣一種情況：需要被證明的主張，並不存在比程式碼本身更簡潔的描述方式；還很容易在證明中偷偷引入一些最終並不成立的假設。你也很容易判斷說，系統裡只有某一部分真正需要形式化證明，但最後卻在其他部分，甚至硬體層面，被一個關鍵漏洞擊中。甚至 Lean 本身的實現也可能存在 bug。但在討論這些令人頭疼的細節之前，我們先進一步看看：如果形式化驗證能夠被理想且正確地完成，它可能帶來怎樣一種近乎烏托邦的前景。

面向安全的形式化驗證

計算機程式碼裡的 bug，本來就令人擔憂。

當你把加密貨幣放進不可變的鏈上智能合約裡時，程式碼 bug 會變得更加可怕。因為一旦程式碼出錯，朝鮮黑客就可能自動把你的錢全部轉走，而你幾乎沒有任何追索手段。

當這一切又被零知識證明包裹起來時，程式碼 bug 會變得更加可怕。因為如果有人成功攻破了零知識證明系統，他們就可以把所有資金提走，而我們可能完全不知道哪裡出了問題——甚至更糟的是，我們可能根本不知道問題已經發生。

當我們擁有強大的 AI 模型時，程式碼 bug 還會變得更加可怕。比如像 Claude Mythos 這樣的模型，再經過兩年改進之後，可能已經可以自動化地發現這些漏洞。

一些人面對這一現實，開始主張放棄智能合約這一基本理念，甚至認為網絡空間根本不可能成為防守方相對於攻擊方擁有非對稱優勢的領域。

下面是一些引述：

為了加固一個系統，你需要花在發現漏洞上的 token，比攻擊者花在利用漏洞上的 token 更多。

還有：

我們這個行業是圍繞確定性代碼建立起來的。寫代碼、測試、上線，然後知道它能正常運行——但以我的經驗來看，這種契約正在失效。在真正 AI 原生公司的頂尖運營者中，代碼庫已經開始變成某種「你相信它能運行」的東西，而這種相信所對應的機率，已經無法再被精確說明。

更糟的是，有些人認為，唯一的解決辦法是放棄開源。

這對網絡安全來說，將是一個黯淡的未來。尤其對那些關心網際網路去中心化與自由的人來說，這會是一個極其黯淡的未來。整個密碼朋克精神，本質上都建立在這樣一個理念之上：在網際網路上，防守方擁有優勢。搭建一座數位「城堡」——無論它體現為加密、簽名還是證明——要比摧毀它容易得多。如果我們失去了這一點，那麼網際網路安全就只能來自規模經濟，來自在全世界範圍內追捕潛在攻擊者，更廣義地說，來自一種二選一：要麼支配一切，要麼走向毀滅。

我不同意這種判斷。對於網路安全的未來，我有一個乐觀得多的願景。

我認為，強大的 AI 漏洞發現能力帶來的挑戰確實嚴峻，但它是一種過渡性挑戰。等塵埃落定，我們進入新的均衡之後，我們將抵達一個比過去更有利於防守方的狀態。

Mozilla 也認同這一點。引用他們的話：

你可能需要重新排列其他所有事務的優先級，以一種持續而專注的方式投入到這項任務中。但隧道盡頭是有光的。我們非常自豪地看到，團隊如何站出來應對這一挑戰，其他人也會做到。我們的工作還沒有完成，但我們已經越過拐點，並開始看見一個遠不只是「勉強跟上」的、更好的未來。防守方終於有機會取得決定性的勝利。

……

缺陷的數量是有限的，而我們正在進入一個終於可以把它們全部找出來的世界。

現在，如果你在 Mozilla 的這篇文章裡用 Ctrl+F 搜索「formal」和「verification」，你會發現兩個詞都沒有出現。網路安全的積極未來，並不嚴格依賴於形式化驗證，也不依賴於其他任何單一技術。

那它依賴什麼？基本上，就是下面這張圖：

過去幾十年裡，很多技術都推動了「漏洞數量下降」這一趨勢：

類型系統；

內存安全語言；

軟體架構改進，包括沙箱、權限機制，以及更普遍地明確區分「可信計算基」（trusted computing base）與「其他代碼」；

更好的測試方法；

關於安全與不安全編碼模式的知識積累；

越來越多預先編寫並經過審計的軟體庫。

由 AI 輔助的形式化驗證，不應被視為一種全新的範式，而應被看作一種強大的加速器：它正在加速一個早已向前推進的趨勢和範式。

形式化驗證並不是萬能藥。但在某些場景下，它尤其適用：也就是目標遠比具體實現更簡單的時候。這一點在以太坊下一次重大迭代中需要部署的一些最棘手技術裡尤為明顯，例如抗量子簽名、STARK、共識算法和 ZK-EVM。

STARK 是一套非常複雜的軟體。但它所實現的核心安全屬性卻很容易理解，也很容易形式化：如果你看到一個證明，它指向程式 P、輸入 x 和輸出 y 的雜湊 H，那麼要麼是 STARK 所使用的雜湊演算法被攻破了，要麼就是 P(x) = y。因此，我們有了 Arklib 專案，它試圖創建一個經過完整形式化驗證的 STARK 實現。另一個相關專案是 VCV-io，它提供基礎性的預言機計算基礎設施，可用於對各種密碼學協議進行形式化驗證，其中許多協議本身也是 STARK 的依賴組件。

更加雄心勃勃的是 evm-asm：這是一個試圖構建完整 EVM 實現、並對其進行形式化驗證的專案。在這裡，安全屬性沒有那麼清晰。簡單來說，它的目標是證明這個實現與另一個用 Lean 編寫的 EVM 實現是等價的；而後者可以在不考慮具體運行效率的情況下，盡可能追求直觀性和可讀性。

當然，理論上仍然可能出現這樣一種情況：我們有十個 EVM 實現，它們都被證明彼此等價，卻都共享同一個致命缺陷，而這個缺陷 somehow 會讓攻擊者從一個他們沒有權限控制的地址中轉走所有 ETH。但相比今天某一個 EVM 實現單獨存在這種缺陷，這種情況發生的概率要低得多。另一個我們是在慘痛經驗之後才真正意識到其重要性的安全屬性——抗 DoS 能力——則相對容易被明確規定。

另外兩個重要方向是：

拜占庭容錯共識。在這個方向上，形式化定義所有期待的安全屬性同樣並不容易。但鑒於相關 bug 一直非常常見，嘗試形式化驗證仍然值得。因此，現在已經有一些關於 Lean 共識實現及其證明的進行中工作。

智能合約程式語言。相關例子包括 Vyper 和 Verity 中的形式化驗證工作。

在所有這些案例中，形式化驗證帶來的一個巨大增量價值在於：這些證明是真正端到端的。很多最棘手的 bug，往往是交互型 bug，它們出現在兩個被分開考慮的子系統邊界處。對人類來說，端到端推理整個系統太困難了；但自動化的規則檢查系統可以做到。

面向效率的形式化驗證

我們再來看 evm-asm。它是一個 EVM 實現。

但它是一个直接用 RISC-V 汇编语言写成的 EVM 实现。

真的是字面意义上的組合語言。

下面是 ADD 操作碼：

1111₆

之所以選擇 RISC-V，是因為當前正在構建的 ZK-EVM 證明器，通常都是通過證明 RISC-V，並將以太坊客戶端編譯到 RISC-V 來工作的。因此，如果你直接用 RISC-V 寫一個 EVM 實現，理論上它就應該是你能得到的最快實現。RISC-V 也可以在普通計算機中非常高效地被模擬運行，而且 RISC-V 筆記本電腦也已經存在。當然，如果要做到真正端到端，你還必須對 RISC-V 實現本身，或者證明器的算術表示，進行形式化驗證。不過不用擔心——這類工作也已經存在。

直接用組合語言寫代碼，是我們五十年前經常做的事情。從那以後，我們逐漸轉向用高級語言編寫代碼。高級語言會犧牲一定效率，但作為交換，它能讓代碼編寫速度快得多，更重要的是，也讓理解他人的代碼快得多——而這對安全來說是必要條件。

借助形式化驗證與 AI 的結合，我們有機會「回到未來」。具體來說，就是讓 AI 來編寫組合語言代碼，然後再寫出形式化證明，驗證這些組合語言代碼具備我們想要的屬性。至少，這個目標屬性可以只是：它與一個為了可讀性而優化、用某種對人類友好的高級語言寫成的實現完全等價。

這樣一來，就不再需要一個代碼對象同時在可讀性和效率之間做平衡。我們會擁有兩個彼此分離的對象：一個是組合語言實現，它只為效率而優化，並根據具體執行環境的需求進行調整；另一個是安全主張，或者高級語言實現，它只為可讀性而優化。然後，我們再用一個數學證明來證明二者之間的等價性。用戶可以先自動驗證一次這個證明；從那以後，他們只需要運行那個快速版本即可。

這非常強大。Yoichi Hirai 將其稱為「軟體開發的最終形態」，並非沒有道理。

形式化驗證不是萬能藥

在密碼學和計算機科學中，有一個傳統幾乎和形式化方法本身一樣古老：批評形式化方法，或者更寬泛地說，批評對「證明」的依賴。相關文獻中有大量實踐案例。我們先從密碼學早期那些更簡單的手寫證明說起。Menezes 和 Koblitz 在 2004 年曾這樣批評過它們：

1979 年，Rabin 提出了一種加密函數，它在某種意義上是「可證明」安全的，也就是說，它具備一種歸約式安全屬性。

所謂歸約式安全主張是：任何能夠從密文 y 中找出消息 m 的人，也必須能夠分解 n。

在 Rabin 提出他的加密方案後不久，Rivest 指出，頗具諷刺意味的是，正是那個給它帶來額外安全性的特徵，在面對另一類攻擊者時，也會導致系統徹底崩潰。這類攻擊者被稱為「選擇密文」攻擊者。具體來說，假設攻擊者能夠以某種方式誘使 Alice 解密一段由攻擊者自己選擇的密文。那麼，攻擊者就可以按照上一段中 Sam 所使用的同樣流程來分解 n。

Menezes 和 Koblitz 隨後又舉了幾個例子。它們共同呈現出一種模式：圍繞「更容易被證明」來設計密碼協議，往往會讓協議變得不那麼「自然」，也更容易在設計者根本沒有考慮到的場景中崩潰。

現在，我們再回到機器可驗證證明和代碼。下面是一篇 2011 年論文中的例子，作者在經過形式化驗證的 C 編譯器中發現了 bug：

我們發現的第二個 CompCert 問題，體現在兩個 bug 中。這兩個 bug 會生成類似下面這樣的代碼：stwu r1, -44432(r1)

這裡正在分配一個很大的 PowerPC 堆疊框架。問題在於，16 位位移字段發生了溢出。CompCert 的 PPC 語義並沒有規定這個立即數取值寬度上的約束，因為它假設彙編器會捕捉到超出範圍的值。

再看一篇 2022 年的論文：

在 CompCert-KVX 中，commit e2618b31 修復了一個 bug：「nand」指令會被列印成「and」；而「nand」只會在少見的 ~(a & b) 模式下被選擇。這個 bug 是通過編譯隨機生成的程序發現的。

到了今天，也就是 2026 年，Nadim Kobeissi 在描述 Cryspen 中形式化驗證軟件的漏洞時寫道：

2025 年 11 月，Filippo Valsorda 獨立報告稱，libcrux-ml-dsa v0.0.3 在給定相同決定性輸入的情況下，會在不同平台上生成不同的公鑰和簽名。這個 bug 位於 _vxarq_u64 內建函數包裝器中，該包裝器實現了 SHA-3 的 Keccak-f 置換中使用的 XAR 操作。fallback 路徑向移位操作傳入了錯誤參數，導致在沒有硬體 SHA-3 支援的 ARM64 平台上，SHA-3 摘要被破壞。這是一個 I 型失敗：該內建函數被標記為已驗證，而整個 NEON 後端並沒有完成運行時安全性或正確性證明。

還有：

libcrux-psq crate 實現了一個後量子預共享金鑰協議。在 decrypt_out 方法中，AES-GCM 128 解密路徑會對解密結果調用 .unwrap()，而不是繼續傳遞錯誤。一個畸形密文就可以讓進程崩潰。

以上四個問題都可以歸為兩類：

第一類，是只有部分程式碼被驗證了，因為驗證其餘部分太難；而結果證明，未被驗證的程式碼比作者想象中更容易出 bug，而且這些 bug 往往更關鍵。

第二類，是作者忘記明確規定某個關鍵屬性，而這個屬性本來是需要被證明的。

Nadim 的文章對形式化驗證的失敗模式進行了分類；他還列舉了其他失敗類型。例如，另一個主要類型是：形式化規範本身是錯的，或者證明中包含錯誤主張，卻被構建系統靜默接受。

最後，我們還可以看看發生在軟體與硬體邊界上的形式化驗證失敗。這裡一個常見問題，是驗證系統能否抵抗側信道攻擊。即便你用一種理論上完全安全的加密方式保護了訊息，但如果幾米外的某個人能夠捕捉電氣波動，並在幾十萬次加密之後提取出你的私鑰，那麼你依然是不安全的。

「差分功耗分析」（differential power analysis）就是這類技術中一個如今已經被充分理解的例子。

差分功耗分析是一種常見的側信道攻擊。來源：Wikipedia

過去也有人嘗試證明系統能夠抵抗這類攻擊者。然而，任何這樣的證明都需要某種關於攻擊者的數學模型，然後你才能在這個模型下證明安全性。有時，人們會使用「d-probing model」：也就是假設攻擊者能夠探測電路中位置的數量存在一個已知上限。但問題在於，有些洩漏形式並不能被這種模型捕捉到。

這篇文章中觀察到的一個常見問題，是轉換洩漏（transitional leakage）：如果你觀察到的訊號並不取決於某個位置上的具體值，而是取決於這個值的變化，那麼很多時候，你就可以從兩個值——舊值和新值——之間恢復出所需信息，而不只是依賴某一個值。該文章還對其他形式的洩漏進行了分類。

幾十年來，這些對形式化驗證的批評，反過來也幫助形式化驗證變得更好。相比過去，我們現在已經更善於警惕這類問題。但即便到今天，它仍然並不完美。

如果把視角拉遠，這裡其實有一條共同線索：形式化驗證很強大。但無論市場宣傳如何把它包裝成可以帶來「可證明的正確性」，所謂「可證明的正確性」從根本上並不能證明軟體，或者硬體，在真正意義上是「正確的」。

對大多數人來說，「正確」大致意味著：這個東西的行為符合用戶對開發者意圖的理解。

而「安全」大致意味著：這個東西的行為不會以損害用戶利益的方式，偏離用戶的預期。

在這兩種情況下，正確性和安全性最終都歸結為一種比較：一邊是一個數學對象，另一邊是人類的意圖或預期。嚴格來說，人類意圖和預期本身也是數學對象——畢竟，人腦也是宇宙的一部分，而宇宙遵循物理定律；只要你有足夠的算力，理論上就可以模擬它們。但它們是極其複雜的數學對象，無論是計算機還是我們自己，都無法真正理解，甚至無法讀取。出於實際目的，我們可以把它們視為黑箱。我們之所以還能對自己的意圖和預期有一些理解，只是因為每個人都有多年觀察自身想法，並推斷他人想法的經驗。

也正因為我們無法把原始的人類意圖直接塞進計算機裡，形式化驗證就沒有辦法證明某個系統與人類意圖之間的比較。因此，「可證明的正確性」和「可證明的安全性」實際上並沒有證明人類所理解的「正確性」和「安全性」——在我們能夠模擬人腦之前，沒有任何方法能真正做到這一點。

那麼，形式化驗警真正有用的地方是什麼？

我傾向於把測試套件、類型系統和形式化驗證，看作是同一種底層編程語言安全方法的不同實現形式——這可能也是唯一真正說得通的方法。它們的共同點在於：用不同方式對我們的意圖進行冗余說明，然後自動檢查這些不同說明之間是否彼此兼容。

比如，看下面這段 Python 代碼：

在這裡，你用三種不同的方式表達了自己的意圖：

第一，直接表達：通過代碼實現斐波那契公式。

第二，間接表達：通過類型系統說明輸入、輸出以及遞歸過程中的中間步驟都是整數。

第三，採用一種「案例包」的方法：也就是測試用例。

運行這個檔案時，系統會用這些示例來檢查公式是否成立。類型檢查器則可以驗證類型之間是否兼容：把兩個整數相加是一個有效操作，並且會得到另一個整數。類型系統在物理計算中也常常很有用：如果你正在計算加速度，但得到的結果單位是 m/s，而不是 m/s²，那你就知道自己哪裡算錯了。而「案例包」式的定義，測試用例就是其中一種，往往也比直接、顯式的定義更符合人類處理概念的方式。

你能用越多不同方式來表達自己的意圖越好；理想情況下，這些方式應當彼此差異足夠大，迫使你用不同的思考方式來處理同一個問題。這樣一來，如果所有這些表達最終都能相互兼容，那麼你真正表達出自己想要表達內容的概率也就越高。

安全編程的核心，就是以多種不同方式表達你的意圖，然後自動驗證這些表達是否彼此兼容。

形式化驗證可以把這種方法進一步推進。借助形式化驗證，你幾乎可以用任意多種冗余方式來描述自己的意圖；只有當這些描述彼此兼容時，程式才會通過驗證。

你可以同時寫出一個經過優化的實現，以及一個效率很低但便於人類閱讀的實現，然後驗證二者是否一致。你也可以請十個朋友分別列出他們認為這個程式應該滿足的數學屬性，再檢查程式是否全部滿足；如果沒有通過，就進一步判斷到底是程式錯了，還是那條數學屬性本身有問題。而 AI 可以讓上述所有工作都變得極其高效。

那我該如何開始？

現實地說，你大概率不會親自去寫證明。形式化方法之所以一直沒有真正普及，根本原因就在於：大多數人很難理解到底該怎麼寫這些該死的證明。

你能告訴我下面這段程式碼是什麼意思嗎？

（如果你想知道的話，它是某個證明中的許多子引理之一。這個證明針對的是 SPHINCS 簽名某個變體的一項特定安全主張：也就是說，除非出現雜湊碰撞，否則相較於任何其他訊息的簽名，為某一條訊息生成簽名，至少需要在某一條雜湊鏈上使用一個位置更高的值。因此，它需要的訊息無法從另一條簽名中計算出來。）

你不需要手寫程式碼和證明，而是讓 AI 幫你寫程式——可以直接用 Lean 寫；如果你想追求速度，也可以用彙編寫——並在這個過程中證明你想要的各種屬性。

這項任務的一倔好處在於，它本質上是自我驗證的，所以你不需要一直盯着它。你完全可以讓 AI 自己連續運行幾個小時。最糟糕的情況，不過是它原地打轉、沒有取得進展；或者像我的 Leanstral 曾經有一次做的那樣，為了讓自己的工作更輕鬆，直接把它被要求證明的陳述替換掉。

你最終需要檢查的是：它證明出來的那個命題，是否確實是你想要證明的東西。

在這個 SPHINCS 簽名變異中，最終陳述如下：

這實際上已經勉強接近「可讀」的邊緣了：

如果由一個雜湊摘要生成的數字（dig1），不等於由另一個雜湊摘要生成的數字（dig2），那麼以下說法就不成立：

對於所有數字，dig1 的每一位都小於或等於 dig2 的對應位；

對於所有數字，dig2 的每一位都小於或等於 dig1 的對應位。

這裡比較的是通過加入檢驗和（checksum）後生成的「擴展數字」（wotsFullDigits）。也就是說，不可避免地，在某些位置上，dig1 的擴展數字會更高；而在另一些位置上，dig2 的擴展數字會更高。

在用大語言模型編寫證明方面，我發現 Claude 已經足夠好用，DeepSeek 4 Pro 也足夠勝任。Leanstral 則是一個很有前景的替代方案：它是一個規模較小、開源權重、專門針對 Lean 寫作微調的模型。它擁有 1190 億參數，但每個 token 只啟動 60 億參數，因此可以在本地運行，儘管速度會比較慢——在我的筆記本電腦上，大約是每秒 15 個 token。

根據基準測試，Leanstral 的表現超過了許多規模大得多的通用模型：