Vitalik 認為以太坊下一階段關(guān)鍵在于：聚焦安全與去中心化，推進擴容、zk 驗證、抗量子技術(shù)；實現(xiàn)賬戶抽象提升用戶體驗；強化隱私保護；借助 AI 提升協(xié)議證明能力；讓手機、IoT 設(shè)備能完成鏈驗證，打造最安全、可靠、值得長期依賴的全球計算基礎(chǔ)設(shè)施。

"代碼即法律"——這是區(qū)塊鏈世界最早的信念之一。但如果代碼本身有 bug 呢?如果 AI 讓 bug 變得無處不在呢?這是 Vitalik 最新長文試圖回答的問題。

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

過去幾個月里，一種新的編程范式在以太坊的前沿研發(fā)圈以及計算領(lǐng)域的許多其他角落迅速獲得青睞：直接用非常底層的語言（例如 EVM 字節(jié)碼、匯編語言）或 Lean 編寫代碼，并使用自動可校驗的、用 Lean 編寫的數(shù)學證明來驗證其正確性。

如果操作得當，這不僅有可能輸出極其高效的代碼，而且比以往的編程方式要安全得多。Yoichi Hirai 將此稱為"軟件開發(fā)的終極形態(tài)"。

這篇文章將試圖揭開其中的基本原理，探討軟件的形式化驗證能做什么，以及在以太坊及其他領(lǐng)域中，它的弱點和局限性在哪里。

什么是形式化驗證？

形式化驗證是指以能夠被自動檢查的方式，為數(shù)學定理編寫證明。為了給出一個相對簡單但仍然有趣的例子，讓我們來看看關(guān)于斐波那契數(shù)列的一個基本定理：每第三個數(shù)字是偶數(shù)，其余的是奇數(shù)。

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 ...

證明這一點的一個簡單方法是數(shù)學歸納法，每次向前推進三步。

首先是基本情況。設(shè) F1 = F2 = 1，F(xiàn)3 = 2。通過觀察，我們看到該陳述（"Fi 在 3 的倍數(shù)時為偶數(shù)，否則為奇數(shù)"）在 x = 3 之前是成立的。

接下來是歸納情況。假設(shè)該陳述在 3k+3 之前成立，即我們已經(jīng)知道 F3k+1、F3k+2、F3k+3 的奇偶性分別是奇數(shù)、奇數(shù)、偶數(shù)。我們可以計算下一組三個數(shù)的奇偶性：

F3k+4 = F3k+2 + F3k+3 = 奇數(shù) + 偶數(shù) = 奇數(shù) F3k+5 = F3k+3 + F3k+4 = 偶數(shù) + 奇數(shù) = 奇數(shù) F3k+6 = F3k+4 + F3k+5 = 奇數(shù) + 奇數(shù) = 偶數(shù)

因此，我們從知道該陳述在 3k+3 前成立，推導出了該陳述在 3k+6 前成立。我們可以反復應(yīng)用這個推論，從而確信該規(guī)則對所有整數(shù)都成立。

這個論點足以讓人類信服。但是，如果你想證明復雜一百倍的東西，而且你想非常非常確定自己沒有犯錯呢？好吧，你可以給計算機提供一個它能信服的證明。

以下是它的具體呈現(xiàn)方式：

-- Fibonacci with fib 0 = 0, fib 1 = 1, fib 2 = 1 (indices offset by 1)
def fib : Nat → Nat
  | 0     => 0
  | 1     => 1
  | n + 2 => fib (n + 1) + fib n

-- Claim: fib (3k+1) is odd, fib (3k+2) is odd, fib (3k+3) is even.
-- Equivalently: every third Fibonacci number starting from fib 3 is even.
-- We prove all three at once by induction on k, since each case
-- of the next block is built from the previous block.
theorem fib_triple (k : Nat) :
    fib (3 * k + 1) % 2 = 1 ∧
    fib (3 * k + 2) % 2 = 1 ∧
    fib (3 * k + 3) % 2 = 0 := by
  induction k with
  | zero => decide
  | succ k ih =>
    -- Rewrite the new indices into the form (something) + 2 so fib unfolds.
    refine ??_, ?_, ?_?
    · show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1
      omega
    · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1
      omega
    · show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)
      + (fib (3 * k + 3) + fib (3 * k + 2))) % 2 = 0
      omega

這是同樣的推理邏輯，但用 Lean 表達出來。Lean 是一種常用于編寫和驗證數(shù)學證明的編程語言。

這看起來與上面給出的"人類"證明不同，原因很充分：對計算機直觀的東西（在"計算機"的傳統(tǒng)意義上，即由 if/then 語句組成的"確定性"程序，而不是大型語言模型）與對人類直觀的東西截然不同。

在上面的證明中，你沒有強調(diào) fib(3k+4) = fib(3k+3) + fib(3k+2) 這個事實，而是強調(diào)了 fib(3k+3) + fib(3k+2) 是奇數(shù)，而 Lean 中名字相當宏大、叫做 omega 的策略會自動將其與它對 fib(3k+4) 定義的知識結(jié)合起來。

在更復雜的證明中，你有時候必須在每一步明確指定是哪條數(shù)學定律允許你采取當前這一步，有時還要用到像 Prod.mk.inj 這樣晦澀的名字。

但另一方面，你可以在一步之內(nèi)展開巨大的多項式表達式，并且只需通過像 "omega" 或 "ring" 這樣的單行表達式來證明它是合理的。

這種不直觀和繁瑣很大程度上解釋了為什么盡管機器可驗證的證明已經(jīng)存在了近 60 年，該領(lǐng)域卻依然小眾。但另一方面，由于人工智能的快速發(fā)展，許多以前不可能的事情現(xiàn)在正迅速成為可能。

當數(shù)學證明開始守護代碼

到目前為止，你可能會想：好吧，計算機能夠驗證數(shù)學定理的證明了，所以我們終于能確定關(guān)于質(zhì)數(shù)之類的瘋狂新結(jié)論里哪些是真的，哪些只是百頁 pdf 論文里的錯誤。

也許我們甚至能弄清楚望月新一關(guān)于 ABC 猜想的觀點是否正確！

但拋開獵奇心不談，那又怎樣？

有很多可能的答案。但對我來說非常重要的一個答案是，驗證計算機程序的正確性，特別是那些執(zhí)行密碼學或與安全相關(guān)任務(wù)的程序。

畢竟，計算機程序是一個數(shù)學對象，因此證明計算機程序以某種方式運行本身就是一個數(shù)學定理。

例如，假設(shè)你想證明像 Signal 這樣的加密通信軟件是否真的安全。你可以寫下在這種背景下"安全"在數(shù)學上的含義。

從高層次來看，你要證明的是，假設(shè)某些密碼學假設(shè)成立，只有擁有私鑰的人才能了解有關(guān)消息內(nèi)容的任何信息。在現(xiàn)實中，有許多不同的安全屬性都非常關(guān)鍵。

事實證明，真的有一個團隊在試圖弄清楚正是這個問題！他們的一個安全定理看起來是這樣的：

theorem passive_secrecy_le_ddh
    (g : G)
    (adv : PassiveAdversary G SK) :
    passiveSecrecyAdvantage (F := F) g adv ≤
    ProbComp.boolDistAdvantage
      (DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))
      (DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

以下是 Leanstral 對其含義的總結(jié)：

passive_secrecy_le_ddh 定理是一個緊湊歸約，表明 X3DH 的被動消息保密性至少與隨機預(yù)言模型下的 DDH 假設(shè)一樣難。 如果對手能夠破解 X3DH 的被動消息保密性，那么他們也能破解 DDH。

由于我們假設(shè) DDH 很難破解，因此 X3DH 對被動攻擊也是安全的。 該定理證明了，如果對手可以被動觀察 Signal 的密鑰交換消息，他們無法以優(yōu)于可忽略的概率將其產(chǎn)生的會話密鑰與隨機密鑰區(qū)分開來。

如果你將其與 AES 加密實現(xiàn)正確的證明結(jié)合起來，你就得到了 Signal 協(xié)議的加密對被動攻擊者是安全的證明。

類似的項目也證明了 TLS 和瀏覽器內(nèi)密碼學其他部分的實現(xiàn)是安全的。

如果你進行端到端的完全形式化驗證，你證明的就不只是協(xié)議的某種理論描述是安全的，而是用戶運行的具體代碼在實際中也是安全的。

從用戶的角度來看，這極大地提升了免信任性：為了完全信任代碼，你不需要檢查整個代碼庫，你只需檢查關(guān)于它被證明的那些聲明。

現(xiàn)在，有一些重要的大前提需要牢記，尤其是關(guān)于"安全"這個至關(guān)重要的詞到底意味著什么。

人們很容易忘記證明那些真正重要的聲明。很容易發(fā)現(xiàn)，有時候要證明的聲明并沒有比代碼本身更簡單的描述方式。

很容易在證明中偷偷引入最終并不成立的假設(shè)。也很容易決定系統(tǒng)中只有一個部分真正需要被形式化證明，結(jié)果卻被其他部分（甚至硬件）中的嚴重漏洞擊中。

就連 Lean 實現(xiàn)本身也可能有 bug。但在我們討論所有這些惱人的細節(jié)之前，讓我們首先深入探討一下，正確且理想地完成形式化驗證可能帶來的烏托邦。

為安全而生的形式化驗證

計算機代碼中的 bug 很可怕。

當你把加密貨幣放入不可變的鏈上智能合約，而朝鮮可以在代碼出現(xiàn) bug 時自動抽干 你的所有資金且你無法申訴時，代碼中的 bug 就變得更加可怕。

當這一切被包裝在零知識證明中時，bug 就變得越發(fā)可怕，因為如果有人設(shè)法黑入零知識證明系統(tǒng)，他們可以提取所有的錢，而我們完全不知道出了什么問題（更糟糕的是，甚至不知道何時出了問題）。

當我們擁有強大的AI模型，比如再迭代兩年后的Claude Mythos，可以自動化地發(fā)現(xiàn)這些 bug 時，代碼中的 bug 就更加更加可怕了。

有些人對這種現(xiàn)實的反應(yīng)是主張放棄智能合約的基本理念，甚至認為網(wǎng)絡(luò)領(lǐng)域根本無法成為防御者能夠?qū)粽邠碛胁粚ΨQ優(yōu)勢的領(lǐng)域。

一些引言：

要加固一個系統(tǒng)，你需要花費比攻擊者用于利用漏洞更多的代幣來發(fā)現(xiàn)這些漏洞。

以及：

我們這個行業(yè)是建立在確定性代碼的基礎(chǔ)上的。編寫它、測試它、發(fā)布它、確信它能運行，但在我的經(jīng)驗中，這種契約正在破裂。

在真正AI原生公司的頂尖運營者中，代碼庫已經(jīng)變成了你"相信"它能運行的東西，而你不再能精確說明它的成功概率。

更糟糕的是，一些人認為唯一的解決方案是放棄開源。

對網(wǎng)絡(luò)安全而言，這將是一個黯淡的未來。尤其是對于我們這些關(guān)心互聯(lián)網(wǎng)去中心化和自由的人來說，這是極其悲觀的前景。

整個密碼朋克精神從根本上建立在這樣一個理念上：在互聯(lián)網(wǎng)上，防御者具有優(yōu)勢，建立一座數(shù)字"城堡"（無論是加密、簽名還是證明）要比摧毀一座容易得多。

如果我們失去了這一點，那么互聯(lián)網(wǎng)安全就只能來自規(guī)模經(jīng)濟，來自在全世界追捕潛在的攻擊者，并且從更廣泛的意義上說，只能在統(tǒng)治與毀滅之間做二選一。

我不同意，我對網(wǎng)絡(luò)安全的未來有著更加樂觀的愿景。

我認為強大的 AI 漏洞尋找能力帶來的挑戰(zhàn)是嚴峻的，但它是一個過渡性的挑戰(zhàn)。一旦塵埃落定，我們進入新的平衡點，我們將獲得比過去更加有利于防御者的環(huán)境。

Mozilla 同意我的觀點。引用他們的話：

你可能需要重新調(diào)整所有其他事務(wù)的優(yōu)先級，把持續(xù)和全神貫注的精力投入到這項任務(wù)中，但隧道的盡頭是有光明的。

我們對我們的團隊如何迎接這一挑戰(zhàn)感到非常自豪，其他人也會做到。我們的工作尚未完成，但我們已經(jīng)度過了難關(guān)，并且能夠窺見一個不僅是勉強跟上、而是要美好得多的未來。

防御者終于有機會決定性地贏得勝利。 ... 缺陷是有限的，我們正在進入一個終于可以把它們?nèi)空页鰜淼氖澜纭?/p>

現(xiàn)在，如果你在 Mozilla 的帖子中使用 Ctrl+F 搜索"形式化"和"驗證"這兩個詞，你將會發(fā)現(xiàn)零個匹配項。網(wǎng)絡(luò)安全的積極未來并不完全依賴于形式化驗證，或者任何其他單一技術(shù)。

它取決于什么？基本上是這張圖表：

CVE漏洞數(shù)量隨時間的下降趨勢

幾十年來，許多技術(shù)促成了漏洞數(shù)量的下降：

• 類型系統(tǒng)
• 內(nèi)存安全語言
• 軟件架構(gòu)的改進（包括沙盒化、權(quán)限控制，以及更廣泛地明確區(qū)分"可信計算基礎(chǔ)"與"其他代碼"）
• 更好的測試方法
• 關(guān)于安全和不安全編碼模式的知識體系不斷豐富
• 預(yù)先編寫并經(jīng)過審計的軟件庫不斷增加

在人工智能輔助下的形式化驗證不應(yīng)該被視為一種全新的范式，而應(yīng)該被看作是已經(jīng)在向前發(fā)展的趨勢和范式的強大加速器。

形式化驗證不是萬能的。但它特別適合目標比實現(xiàn)簡單得多的情況。這在我們將需要在以太坊的下一個主要迭代中部署的一些極其復雜的棘手技術(shù)中尤為真實：抗量子簽名、STARKs、共識算法以及 ZK-EVMs。

STARK 是一款非常復雜的軟件。但它實現(xiàn)的核心安全屬性很容易理解和形式化：如果你看到一個指向程序 P 的哈希 H、輸入 x 和輸出 y 的證明，那么要么 (i) STARK 中使用的哈希算法被攻破了，要么 (ii) P(x) = y。

因此我們有了 Arklib 項目，它正試圖創(chuàng)建一個完全經(jīng)過形式化驗證的 STARK 實現(xiàn)（參見 VCV-io，它提供了基礎(chǔ)的預(yù)言機計算基礎(chǔ)設(shè)施，可用于形式化驗證各種其他加密協(xié)議，其中許多是 STARK 的依賴項）。

更具野心的是 evm-asm：一個構(gòu)建完全經(jīng)過形式化驗證的整個 EVM 實現(xiàn)的項目。

這里的安全屬性就沒那么簡單明了了：基本上，目標是證明其等效于用 Lean 編寫的另一個 EVM 實現(xiàn)，不過那個實現(xiàn)可以為了最大化直觀性和可讀性而編寫，完全不用考慮具體的運行效率。

有可能我們會得到十個 EVM 實現(xiàn)，都可證明地互為等價，且它們碰巧都包含同一個致命缺陷，能讓攻擊者抽干 他們沒有權(quán)限動用的地址里的所有 ETH。

但這比現(xiàn)今某個 EVM 實現(xiàn)存在這類缺陷的可能性要小得多。而另一個我們在經(jīng)歷了痛苦教訓后才明白其重要性的安全屬性，即抗DoS攻擊能力，就很容易規(guī)范。

另外兩個重要領(lǐng)域是：

• 拜占庭容錯共識。在這里，要形式化規(guī)范所有期望的安全屬性同樣困難，但考慮到 bug 曾經(jīng)如此普遍，還是值得一試的。因此我們在 Lean 中有進行中的共識協(xié)議的 Lean 實現(xiàn)及證明。
• 智能合約編程語言：參見 Vyper 和 Verity 中的形式化驗證。

在所有這些情況中，形式化驗證帶來的巨大附加值之一在于這些證明真正是端到端的。通常，最討厭的 bug 都是交互 bug，它們潛伏在兩個被獨立考慮的子系統(tǒng)的交界處。

對于人類來說，端到端地推理整個系統(tǒng)太困難了。但自動化的規(guī)則檢查系統(tǒng)能夠做到。

為效率而生的形式化驗證

讓我們再看看 evm-asm。這是一個 EVM 實現(xiàn)。但它是直接用 RISC-V 匯編編寫的 EVM 實現(xiàn)。

貨真價實地。

這是 ADD 操作碼：

import EvmAsm.Rv64.Program
namespace EvmAsm.Evm64
open EvmAsm.Rv64

/-- 256-bit EVM ADD: binary, pops 2, pushes 1.
    Limb 0: LD, LD, ADD, SLTU (carry), SD (5 instructions).
    Limbs 1-3: LD, LD, ADD, SLTU (carry1), ADD (carryIn), SLTU (carry2), OR (carryOut), SD (8 each).
    Then ADDI sp, sp, 32.
    Registers: x12=sp, x7=acc, x6=operand, x5=carry, x11=carry1. -/
def evm_add : Program :=
  -- Limb 0 (5 instructions)
  LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;

  -- Limb 1 (8 instructions)
  LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;

  -- Limb 2 (8 instructions)
  LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;

  -- Limb 3 (8 instructions)
  LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;
  ADD .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;
  ADD .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;
  OR' .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;

  -- sp adjustment
  ADDI .x12 .x12 32
end EvmAsm.Evm64

之所以選擇 RISC-V，是因為正在構(gòu)建的 ZK-EVM 證明器通常通過證明 RISC-V 并將以太坊客戶端編譯為 RISC-V 來運作。因此，如果你有一個直接用 RISC-V 編寫的 EVM 實現(xiàn)，這應(yīng)該是你能得到的最快實現(xiàn)。

RISC-V 也可以在普通計算機內(nèi)非常高效地被模擬（且市面上也有 RISC-V 筆記本電腦）。

當然，為了真正實現(xiàn)端到端，你必須形式化驗證 RISC-V 的實現(xiàn)（或證明器的算術(shù)化）本身，但別擔心，這方面的工作也已經(jīng)存在了。

直接用匯編編寫代碼是我們在五十年前常做的事情。從那時起，我們已經(jīng)放棄了這種做法，轉(zhuǎn)而使用高級語言編寫代碼。

高級語言在效率上有所妥協(xié)，但作為交換，它們編寫代碼的速度快得多，更重要的是，理解他人代碼的速度也快得多，這對于安全來說是必不可少的。

借助形式化驗證和人工智能的結(jié)合，我們有機會"回到未來"。

具體來說，我們可以讓人工智能編寫匯編代碼，然后編寫一個形式化證明來驗證該匯編代碼具有所需屬性。

至少，所需屬性可以僅僅是與那些為提高可讀性而優(yōu)化、且用某種人類友好的高級語言編寫的實現(xiàn)完美等價。

我們不再需要單一的代碼對象在可讀性和效率之間進行平衡，而是擁有兩個獨立的對象：一個（匯編實現(xiàn)）僅優(yōu)化效率，同時考慮到其執(zhí)行的特定環(huán)境的需求；另一個（安全聲明，或高級語言實現(xiàn)）僅優(yōu)化可讀性，然后我們通過數(shù)學證明來證明兩者之間的等價性。

用戶可以（自動地）驗證一次該證明，從那時起，他們只需運行快速版本。

這種方法非常強大，Yoichi Hirai 稱之為"軟件開發(fā)的終極形態(tài)"是有原因的。

形式化驗證不是靈丹妙藥

在密碼學和計算機科學領(lǐng)域，有一個傳統(tǒng)幾乎與形式化方法本身的歷史一樣悠久：那就是批評形式化方法（或更廣泛地批評對"證明"的依賴）的傳統(tǒng)。

這些文獻充滿了實際案例。讓我們從早期簡單密碼學時代手寫的證明說起，此處引用了 Menezes 和 Koblitz 在 2004 年的批評：

1979 年，Rabin 提出了一種加密函數(shù)，該函數(shù)在某種意義上是"可證明"安全的，也就是說，它具有一種歸約主義的安全屬性。

歸約主義安全聲明指出，能夠從密文 y 中找出消息 m 的人，也必須能夠分解 n。 ... 在 Rabin 提出其加密方案后不久，Rivest 指出，具有諷刺意味的是，正是賦予其額外安全性的這一特性，如果它面臨另一種名為"選擇密文"的攻擊者時，會導致全線崩潰。

也就是說，假設(shè)攻擊者可以以某種方式欺騙 Alice 解密其選擇的密文，那么攻擊者就可以遵循 Sam 在上一段中用來分解 n 的相同步驟。

Menezes 和 Koblitz 接著給出了更多例子。常見的規(guī)律是：圍繞著使加密協(xié)議更加"可證明"而進行的設(shè)計，往往會使它們變得更不"自然"，這使得它們更有可能在設(shè)計者甚至沒有考慮過的情況下發(fā)生崩潰。

現(xiàn)在，讓我們回到機器可驗證的證明和代碼。這是一篇 2011 年發(fā)現(xiàn)經(jīng)過形式化驗證的 C 編譯器中存在漏洞的論文：

我們發(fā)現(xiàn)的第二個 CompCert 問題體現(xiàn)在兩個導致生成如下代碼的 bug 中： stwu r1, -44432(r1) 此處正在分配一個大型的 PowerPC 堆棧幀。

問題在于 16 位的位移字段溢出了。CompCert 的 PPC 語義沒有規(guī)定對此立即數(shù)寬度的限制，他們假設(shè)匯編器會捕獲超出范圍的值。

還有一篇 2022 年的論文：

在 CompCert-KVX 中，提交 e2618b31 修復了一個 bug："nand"指令會被打印為"and"；"nand"僅被用于極少見的 ~(a & b) 模式。該 bug 是通過編譯隨機生成的程序發(fā)現(xiàn)的。

而今天，在 2026 年，以下是 Nadim Kobeissi 描述 Cryspen 中經(jīng)過形式化驗證的軟件的漏洞：

在 2025 年 11 月，F(xiàn)ilippo Valsorda 獨立報告了 libcrux-ml-dsa v0.0.3 在給定相同確定性輸入的情況下，在不同平臺上產(chǎn)生了不同的公鑰和簽名。

該 bug 存在于 _vxarq_u64 內(nèi)部包裹函數(shù)中，該函數(shù)實現(xiàn)了 SHA-3 的 Keccak-f 置換中使用的 XAR 操作。后備機制向移位操作傳遞了不正確的參數(shù)，在沒有硬件 SHA-3 支持的 ARM64 平臺上損壞了 SHA-3 摘要。

這屬于類型 I 故障：該內(nèi)部函數(shù)被標記了，而整個 NEON 后端都沒有完成對運行時安全性或正確性的證明。

以及：

libcrux-psq 庫實現(xiàn)了一個后量子預(yù)共享密鑰協(xié)議。在 decrypt_out 方法中，AES-GCM 128 解密路徑對解密結(jié)果調(diào)用了 .unwrap() 而不是傳播錯誤。一個格式錯誤的密文就能讓進程崩潰。

以上四個問題都屬于以下兩種類型之一：

• 只驗證了部分代碼的情況（因為驗證其余部分太難了），結(jié)果發(fā)現(xiàn)未驗證的代碼比作者想象的漏洞更多（且方式更致命）。
• 作者忘記規(guī)定需要證明的關(guān)鍵屬性的情況。

Nadim 的文章包含了對形式化驗證失敗模式的分類；他也給出了其他類型的失敗模式（比如，另一個主要的情況是"形式化規(guī)范本身就是錯的，或者證明中包含了被構(gòu)建系統(tǒng)默默接受的虛假聲明"）。

最后，我們可以看看軟件和硬件邊界上的形式化驗證失敗。這里的一個常見問題是驗證抗側(cè)信道攻擊的能力。

即使你有完美安全的加密形式來保護你的消息，如果幾米外的人能夠捕捉到電信號波動并在幾十萬次加密后提取出你的私鑰，你仍然是不安全的。

這是一篇關(guān)于"差分功率分析"的文章，這是一個目前已經(jīng)被充分理解的此類技術(shù)例子。

差分功率分析是側(cè)信道攻擊的一種常見類型。來源：維基百科

一直有人試圖證明能抵御此類攻擊者的安全性。然而，任何這樣的證明都需要某種攻擊者的數(shù)學模型，讓你能夠針對其證明安全性。

有時會使用"d 探測模型"：我們假設(shè)攻擊者在電路中可以查詢的位置數(shù)量有一個已知的限制。但是，有些泄漏形式是這種模型無法捕捉的。

正如這篇文章中所觀察到的，一個常見問題是過渡性泄漏：如果你能觀察到一個不僅取決于某個位置的值，還取決于該值變化的信號，那么這通常足以讓你從兩個值（新舊值）而不是僅僅一個值中恢復你所需的信息。

這篇文章給出了其他形式泄漏的分類。

幾十年來，對形式化驗證的這些批評幫助形式化驗證變得更好。相比過去，我們現(xiàn)在更善于提防此類問題。但即使在今天，它也不完美。

縱觀全局，這里有一條主線索。形式化驗證很強大。

但無論營銷術(shù)語如何讓形式化驗證聽起來像是給了你"可證明的正確性"，所謂的"可證明的正確性"從根本上并不能證明軟件（或硬件）是"正確的"。

按照大多數(shù)人類的理解，"正確"的意思類似于："事物的行為符合用戶對開發(fā)者意圖的理解"。

而"安全"的意思類似于："事物的行為沒有違背用戶的期望，做出對用戶利益不利的事情"。

在這兩種情況下，正確性和安全性都歸結(jié)為數(shù)學對象與人類意圖或期望之間的比較。

人類的意圖和期望在技術(shù)上也是數(shù)學對象，畢竟人類的大腦也是宇宙的一部分，它遵循著如果你有足夠的算力就可以模擬的物理定律。

但它們是令人難以置信的復雜數(shù)學對象，計算機和我們自己都無法理解甚至無法讀取。

就所有實際意圖和目的而言，它們都是黑匣子；我們之所以對自己的意圖和期望有任何了解，僅僅是因為我們每個人都有多年觀察自己想法和推斷他人想法的經(jīng)驗。

并且由于我們無法將原始的人類意圖塞進計算機，形式化驗證就無法證明與人類意圖的比較。

因此，"可證明的正確性"和"可證明的安全性"實際上并沒有證明我們?nèi)祟愃斫獾?quot;正確性"和"安全性"。除非我們能完全模擬人類大腦，否則任何東西都做不到。

那它到底有什么用?

我傾向于將測試套件、類型系統(tǒng)和形式化驗證都看作是對編程語言安全性同一底層方法的不同實現(xiàn)方式（這可能也是唯一合理的方法）。

它們都是關(guān)于用不同方式冗余地規(guī)范我們的意圖，然后自動檢查這些不同規(guī)范之間是否相互兼容。

以這段 Python 代碼為例：

def fib(n: int) -> int:
    if n < 0:
        raise Exception("Negative values not supported")
    elif 0 <= n < 2:
        return n
    else:
        return fib(n-1) + fib(n-2)

if __name__ == '__main__':
    assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]
    assert fib(15) == 610

在這里，你用三種不同的方式表達你的意圖：

• 顯式地，通過在代碼中實現(xiàn)斐波那契公式
• 隱式地，通過類型系統(tǒng)（指定輸入、輸出和遞歸中間步驟均為整數(shù)）
• 通過"樣例包"方法：測試用例

運行文件會將公式與示例進行核對。類型檢查器可以驗證類型是否兼容：將兩個整數(shù)相加是合規(guī)操作，并會產(chǎn)生另一個整數(shù)。

類型系統(tǒng)往往是在物理學中檢查作業(yè)的好方法：如果你在計算加速度，卻得出了一個單位是米/秒而不是米/秒²的答案，你就知道你做錯了。

而測試用例就是"樣例包"定義的一個實例，對于人類來說，處理概念時這種方式往往比直接顯式的定義自然得多。

你能用越多不同的方式來規(guī)范你的意圖，理想情況下是那些要求你以不同思維方式來解決問題的截然不同的方式，一旦所有這些表達形式都被證明是相互兼容的，你就越有可能實際上表達出了你真正想要的東西。

安全編程在于用多種不同的方式表達你的意圖，然后自動驗證這些表達式是否全都相互兼容。

形式化驗證使你能將這種方法進一步延伸。通過形式化驗證，你可以用幾乎無限數(shù)量的不同冗余方式來規(guī)范你的意圖，程序只有在它們?nèi)考嫒輹r才能驗證通過。

你可以規(guī)范一個高度優(yōu)化的實現(xiàn)以及一個效率極低但易于人類閱讀的實現(xiàn)，并驗證它們是否匹配。你可以請你的十個朋友提供他們認為你的程序應(yīng)具備的數(shù)學屬性列表，然后檢查它是否全部通過。

如果沒通過，找出到底是程序錯了還是數(shù)學屬性定錯了。而且，你可以使用人工智能極度高效地完成所有這些操作。

那么我該如何開始？

現(xiàn)實一點講，你不會自己編寫證明的。形式化方法一直沒有流行起來的原因，就是大多數(shù)人無法弄明白怎么寫這些晦澀的內(nèi)容。你能告訴我下面這段代碼的意思嗎？

  /-- Helper: pointwise ≤ at the foldl level with an accumulator. -/
private theorem foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (a b : Nat) (hAcc : a ≤ b)
    (hLE : Forall? (· ≤ ·) ds1 ds2) :
    List.foldl (λ acc d => acc * w + d) a ds1 ≤
    List.foldl (λ acc d => acc * w + d) b ds2 := by
  match ds1, ds2, hLE with
  | [], [], .nil => exact hAcc
  | d1::ds1', d2::ds2', .cons hd htl =>
    simp [List.foldl]
    refine foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl
    exact Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) hd

（如果你想知道，這是針對一種 SPHINCS 簽名變體的一項特定安全聲明的證明中的許多子引理之一。

具體來說，該聲明是：除非發(fā)生哈希碰撞，否則某條消息的簽名將至少在一條哈希階梯上的某處需要比任何其他消息的簽名更高的值，因此它包含了無法從那另一個簽名中計算出來的信息）

無需手動編寫代碼和證明，你只需讓人工智能為你編寫程序（無論是直接用 Lean 寫，還是為了速度用匯編語言寫），并在過程中證明任何期望的屬性即可。

這項任務(wù)有個好處是它本身就是自我驗證的，因此你不需要去監(jiān)督，你只要讓人工智能自己連續(xù)運行好幾個小時就行。

最糟糕的結(jié)果也就是它在原地打轉(zhuǎn)而毫無進展（或者，就像我的 leanstral 曾做過的那樣，它為了減輕自己的工作負擔，擅自替換掉了被要求證明的聲明）。

你在最后唯一需要檢查的，就是它證明的聲明是否符合你的要求。

在 SPHINCS 簽名變體中，這是最終聲明：

theorem wots_fullDigits_incomparable
    {dig1 dig2 : List Nat} {w l1 l2 : Nat}
    (hw : 0 < w)
    (hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)
    (hBound1 : ? d ∈ dig1, d < w) (hBound2 : ? d ∈ dig2, d < w)
    (hL2suff : l1 * (w - 1) < w ^ l2)
    (hNeq : dig1 ≠ dig2) :
    ? Forall? (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧
    ? Forall? (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2) 

這實際上處于勉強能讀懂的邊緣：

如果從一個哈希摘要（dig1）生成的數(shù)字不等于從另一個哈希摘要（dig2）生成的數(shù)字

那么以下兩種情況都不成立：

• 對于所有數(shù)字，dig1 的數(shù)字 <= dig2 的數(shù)字
• 對于所有數(shù)字，dig2 的數(shù)字 <= dig1 的數(shù)字

在通過添加校驗和生成的"擴展數(shù)字"（wotsFullDigits）中也是如此。也就是說，在 dig1 的擴展中，不可避免地有些地方的數(shù)字會更高，而在另一些地方，dig2 的擴展中的數(shù)字會更高。

在使用大型語言模型編寫證明方面，我發(fā)現(xiàn) Claude 和 Deepseek 4 Pro 都能勝任。Leanstral 是一款經(jīng)過專門微調(diào)以編寫 Lean 的較小開源權(quán)重模型，它是一個很有前景的替代方案。

它擁有 119B 的參數(shù)量，每個 token 激活 6B，你可以在本地運行它，盡管速度較慢（在我的筆記本電腦上速度約為 15 tok/sec）。根據(jù)基準測試，Leanstral 優(yōu)于大得多的通用模型：

根據(jù)我目前的個人經(jīng)驗，它比 Deepseek 4 Pro 稍差一些，但仍然很有效。

形式化驗證無法解決我們所有的問題。

但是，如果我們希望互聯(lián)網(wǎng)安全的模型不再建立在人人都信任少數(shù)幾個強大組織的基礎(chǔ)上，我們就有必要轉(zhuǎn)而去信任代碼，這包括在面對強大的人工智能對手時也能信任代碼。

AI 輔助下的形式化驗證讓我們在實現(xiàn)這一目標的道路上邁出了堅實的大步。

就像區(qū)塊鏈和 ZK-SNARKs 一樣，人工智能和形式化驗證也是非?；パa的技術(shù)。

區(qū)塊鏈以隱私和可擴展性為代價賦予你開放的可驗證性和抗審查性，而 ZK-SNARKs 又把隱私和可擴展性還給了你（實際上甚至比你之前的還要多）。

人工智能以準確性為代價賦予了你編寫大量代碼的能力，而形式化驗證又把準確性還給了你（實際上甚至比你之前的還要高）。

在默認情況下，人工智能將催生大量極為草率的代碼，bug 的數(shù)量將會增加。

事實上，在某些情況下，容忍 bug 的增加才是正確的權(quán)衡：如果 bug 是輕微的，那么即使是存在 bug 的軟件，也比沒有該軟件要好。

但在這里，網(wǎng)絡(luò)安全有著樂觀的未來：軟件將（繼續(xù)）分 裂 成圍繞"安全核心"的"不安全邊緣部分"。

不安全的邊緣部分將在沙箱中運行，只被賦予完成工作所需的最低權(quán)限。

安全核心將管理一切。如果安全核心崩潰，一切都會崩潰，包括你的個人數(shù)據(jù)、你的金錢等等。但是如果某個不安全的邊緣部分崩潰了，安全核心依然能保護你。

當涉及到安全核心時，我們不能讓存在 bug 的代碼泛濫。我們會采取激進的行動來保持安全核心規(guī)模的小巧，甚至進一步縮小它。

相反，我們將人工智能帶來的所有額外性能完全投入到使安全核心更安全的任務(wù)中，從而使其能夠承受我們在高度數(shù)字化的社會中賦予它的極高的信任重任。

操作系統(tǒng)的內(nèi)核（或者至少是其中一部分）將成為這樣的一個安全核心。

以太坊將是另一個。

希望至少對于所有非性能密集型的計算，你所使用的硬件會成為第三個。

與物聯(lián)網(wǎng)相關(guān)的系統(tǒng)將是第四個。

至少在這些安全核心之中，那句古老的格言"bug 是不可避免的，你只能在攻擊者之前盡力去找到它們"將被證偽，取而代之的是一個更加充滿希望的世界，在那里你將獲得真正的安全。

但如果你心甘情愿將你的資產(chǎn)和數(shù)據(jù)交給那些編寫拙劣、可能意外將它們吞噬進黑洞的軟件，好吧，你當然也擁有那個自由。

以上就是Vitalik分析：以太坊（ETH）下一階段，這些關(guān)鍵點將引領(lǐng)變革的詳細內(nèi)容，更多關(guān)于Vitalik：以太坊下一階段關(guān)鍵點的資料請關(guān)注腳本之家其它相關(guān)文章！

你可能感興趣的文章

• 

  區(qū)塊鏈研究員證實：以太坊（ETH）基金會“完全履職”助力去中心化進程

  區(qū)塊鏈研究員指出，以太坊基金會作為非營利組織，通過資助核心研發(fā)、支持生態(tài)項目、組織開發(fā)者大會及運行漏洞賞金計劃等舉措，正積極履行其'長期主義'使命，逐步弱化中心化…

  2026-05-24
• 

  以太坊（ETH）憑生態(tài)與技術(shù)優(yōu)勢，穩(wěn)坐長期優(yōu)質(zhì)買入席位

  盡管近期加密貨幣市場波動不斷，以太坊憑借其強大的技術(shù)生態(tài)與廣泛的應(yīng)用場景，展現(xiàn)出強勁韌性,其智能合約平臺持續(xù)吸引開發(fā)者，DeFi、NFT等領(lǐng)域蓬勃發(fā)展,隨著網(wǎng)絡(luò)升級推進…

  2026-05-23
• 

  哈佛大學一個季度清倉以太坊（ETH），市場表現(xiàn)或促其調(diào)整配置

  哈佛大學在2026年第一季度徹底清倉了全部以太坊頭寸，此前該頭寸僅持有一個季度，持倉價值8680萬美元，因以太坊價格下跌，清倉時虧損超3000萬美元,此次清倉是哈佛連續(xù)第三…

  2026-05-22
• 

  ETH最忠誠多頭也清倉，以太坊怎么了？Bankless內(nèi)部發(fā)生了什么？

  老牌以太坊核心布道機構(gòu) Bankless 迎來劇變，最忠誠多頭公開宣布清倉hth，團隊大幅裁員,機構(gòu)發(fā)展轉(zhuǎn)向弱化以太坊側(cè)重，疊加以太坊基金會高管與技術(shù)骨干接連離職，曾經(jīng)強勢的…

  2026-05-22
• 

  以太坊（ETH）價緊局勢下，Vitalik以前瞻視野推進隱私元數(shù)據(jù)改革

  近期以太坊價格走勢緊繃，市場多空博弈激烈，價格波動牽動投資者神經(jīng),在此背景下，以太坊聯(lián)合創(chuàng)始人Vitalik未將目光局限于價格起伏，而是聚焦隱私和元數(shù)據(jù)改革，試圖通過技…

  2026-05-21
• 

  以太坊交易員提醒：2000美元支撐成關(guān)鍵，失守ETH或大跌！

  以太坊交易員發(fā)出警告，當前ETH價格在2000美元附近膠著，此支撐位極為關(guān)鍵,若有效跌破，技術(shù)面將觸發(fā)大量止損盤，市場看跌情緒或急劇升溫，空頭力量增強，ETH價格可能大幅…

  2026-05-20
• 

  以太坊（ETH）基金會：Josh Stark與Trent Van Epps相繼離職

  以太坊基金會再迎兩位重量級人物離職，高層管理成員Josh Stark與Trent Van Epps相繼宣布離開,Josh Stark任職五年后選擇離職，Trent Van Epps也于同期辭職，計劃繼續(xù)參與Pro…

  2026-05-19
• 

  韓國一殯葬公司杠桿投資ETH ETF，錄得3300萬美元未實現(xiàn)虧損

  韓國某殯葬公司涉足加密貨幣投資，重倉杠桿ETH ETF,受市場波動影響，ETH價格下跌，該公司錄得3300萬美元未實現(xiàn)虧損,此事件凸顯加密貨幣高杠桿投資風險，即使非傳統(tǒng)金融企業(yè)…

  2026-05-19
• 

  ETH跌破2000美元！空頭"接管"后，以太坊能否逆襲？

  以太坊價格跌破2000美元關(guān)鍵心理關(guān)口后，交易員指出空頭已'掌控局面',技術(shù)面顯示，ETH若未能守住該支撐位，可能進一步下探至1800-1900美元區(qū)間，甚至觸及1750-1700美元支撐…

  2026-05-18
• 

  Vitalik Buterin隱私池轉(zhuǎn)賬11.3萬美元，或為以太坊（ETH）隱私新風向

  據(jù)鏈上監(jiān)測，以太坊聯(lián)合創(chuàng)始人Vitalik Buterin通過其支持的隱私協(xié)議Privacy Pools轉(zhuǎn)移了50.25枚ETH，價值約11.3萬美元,該協(xié)議采用零知識證明技術(shù)，允許用戶匿名轉(zhuǎn)移資產(chǎn)，…

  2026-05-16