以太坊共同創辦人 Vitalik Buterin 表示，AI 驅動的駭客攻擊興起，並不會讓資訊安全成為一場註定失敗的競賽，他反而指向形式化驗證，作為證明軟體安全的方法。他主張，開發者不必依賴漏洞的發現，而能以數學方式證明程式符合既定的安全需求。

在 5 月 18 日發表、並於 X 上分享的部落格文章中，Buterin 主張 AI 可以讓這類驗證在規模化下變得可行，他表示這種方法對關鍵系統最為重要，包括密碼學、訊息協定與區塊鏈軟體。

安全必須先被定義才能被證明

Buterin 表示，要證明一個程式是安全的，首先必須定義「安全」究竟意謂著什麼。他以加密通訊軟體 Signal 為例，指出單靠加密並無法涵蓋所有安全問題。完整的定義可能必須考慮訊息偽造、傳送失敗、重播訊息、被駭裝置與金鑰外洩等情況。

硬體則帶來更多複雜性。實體訊號可能洩漏資訊，而訊息大小、傳送者身分與時序等細節本身就可能透露資訊。這些考量加總起來，可能使安全定義超過 1,000 行程式碼。即便如此，Buterin 主張，相對於底層實作，定義仍是驗證上較小的目標。

形式化驗證瞄準完整程式

形式化驗證並非新概念：它長期應用於航空與醫療軟體等安全關鍵領域，因為這些領域失敗的代價極高，但所需的投入也使其在一般用途開發中相當罕見。歷史上，開發者僅驗證他們自己認定具安全關鍵性的部分，主要是因為驗證需要大量心力。Buterin 主張，AI 可以改變這個等式，讓完整程式的驗證更為可行，並將涵蓋範圍擴展至資料庫、網路、快取層與其他元件。

他將此目標與傳統模式做出區隔；在傳統模式中，防禦者搶在攻擊者之前發現漏洞。在他的方法下，軟體透過證明其符合安全需求而變得更有韌性。他表示，當不同群體設定各自的需求時，定義也可以被合併；而當兩個定義無法共存時，開發者可以隔離出底層的設計衝突。不過他承認，某些使用者介面仍然更難處理。

以太坊軟體面臨複雜的驗證需求

Buterin 指出訊息傳遞協定、沙盒、SNARKs——證明某項運算被正確執行的精簡密碼學證明——以及全同態加密（允許直接在加密資料上進行運算）等領域，是定義與實作之間的區別可能產生影響之處。他將此方法直接與以太坊的發展方向連結，表示區塊鏈需要更強的軟體安全，尤其是在追求可擴展性與隱私的系統中。

這樣的情境凸顯了利害關係：區塊鏈軟體是開放原始碼，其所支援的網路直接保管資產，因此同一份程式碼同時暴露在攻擊者與防禦者的眼前——在這種條件下，不依賴誰先發現漏洞的保證就顯得格外重要。

他的論述核心在於數學驗證，而非僅依賴漏洞發現。他表示，驗證必須超越被挑選出的程式碼區段：定義需要縝密的工作，而實作則仍須接受形式化檢查。在他看來，AI 可以承擔這個流程的規模，涵蓋資料庫、網路、快取與其他元件。值得關注的問題是，AI 輔助的工具能否將完整程式驗證帶入生產規模的日常實務，包括他所指出最難處理的使用者介面。