目錄
- 人工智能與形式化證明能否消除加密漏洞？
- 什麼是形式化驗證？
- 佈特林為何認為人工智能改變瞭遊戲規則
- 加密平臺為何易受軟件漏洞影響
- 為什麼形式化驗證無法保證完全的密碼安全
- 人工智能帶來新挑戰
- 為什麼‘足夠安全’比‘完全無漏洞’更重要
形式化驗證是用數學方法嚴格證明系統是否滿足規范的技術，可窮盡所有場景提供無死角正確性保證。維塔利克認為AI能通過自然語言轉換、自動化模型檢測、神經符號推理等方式，降低形式化驗證門檻，提升驗證效率，助力區塊鏈等復雜系統實現更高安全性。
維塔利克·佈特林表示，人工智能輔助的形式化驗證或可強化加密安全，但數學證明仍存在重大局限性。
人工智能與形式化證明能否消除加密漏洞？
維塔利克·佈特林認為，人工智能可通過形式化驗證提升加密貨幣的安全性。在最近的一篇博客文章中，他指出，借助人工智能的驗證技術有望成為抵禦日益復雜的軟件攻擊的重要保障。
這一概念極具吸引力：人工智能生成或檢查代碼，而數學證明則確保軟件完全按照預期運行。從原理上講，這種方法有望減少嚴重的智能合約漏洞、交易所風險以及共識失敗。
然而，一個重大局限依然存在。即使人工智能推動瞭形式化驗證的發展，加密系統也難以真正保證軟件完全無 bug。現實世界的區塊鏈依賴於諸多假設、硬件組件、外部連接、治理機制以及人為決策，而僅靠數學手段並不能完全規避這些風險。
佈特林的構想或可大幅提高加密貨幣的安全性。不過，它不太可能完全消除出現故障的可能性。
維塔利克·佈特林闡述瞭他關於人工智能輔助形式化驗證的主張
什麼是形式化驗證？
形式化驗證涉及以數學方式證明軟件在既定參數范圍內遵循指定規則。
與其完全依賴人工審核員或測試環境，開發者會創建數學描述，以說明系統應如何運行。隨後，專業工具會檢查代碼是否始終符合這些要求。
例如，經過形式化驗證的智能合約可能在數學上證明：
- 未經適當授權，資產不得提取。
- 代幣的總供應量不得超過固定上限。
- 驗證者不得進行未經授權的狀態變更。
- 在所述條件下，特定攻擊向量是不可能實現的。
簡而言之，測試旨在驗證代碼在選定的幾種情況下是否能正確運行。而形式化驗證則旨在驗證代碼在證明所涵蓋的任何條件下是否都不會違反規則。
這種技術已廣泛應用於航空、國防系統以及其他關鍵硬件和軟件領域。加密開發者正越來越多地將其應用於關鍵安全組件，因為區塊鏈交易往往不可逆轉，且可能涉及巨額資金。
蘋果corecrypto的正式驗證
佈特林為何認為人工智能改變瞭遊戲規則
在2026年5月的文章中，佈特林指出，人工智能可能顯著降低形式驗證的主要缺點之一：其復雜性。
傳統的形式化驗證可能成本高昂、耗時漫長，且需要專業知識。從業者通常需具備定理證明器、證明系統和數學邏輯方面的高級知識。編寫證明有時甚至比開發原始軟件本身還要費力。
佈特林預計人工智能將簡化這一工作流程的某些環節。
他描述瞭一種場景：開發者使用低級語言編寫代碼，或借助Lean等以證明為導向的工具，而人工智能則協助生成證明、識別不一致之處，並以更少的手動幹預確保代碼的正確性。
核心思想是：人工智能不僅可能加速軟件開發，還有望助力軟件安全屬性的數學驗證工作。
Buterin將這種做法定位為一種防禦性應對措施，以應對人工智能在軟件分析領域日益增長的使用。如果惡意行為者能夠利用人工智能更快地識別漏洞，那麼防禦方可能需要更強的數學保障，而不能僅僅依賴傳統的代碼審查。
以太坊聯合創始人維塔利克·佈特林
加密平臺為何易受軟件漏洞影響
傳統銀行通常能夠通過既定流程對欺詐轉賬進行撤銷或追回，但基於區塊鏈的系統在交易完成之後往往提供的選項較少。
即使是去中心化金融（DeFi）協議中一個微小的編程錯誤，也可能導致資產被鎖定、生成未經授權的代幣，或在幾分鐘內讓攻擊者耗盡流動性池。以往的加密貨幣漏洞事件一再表明，即使經過廣泛審查的代碼，在遇到意料之外的情況時仍可能失效。
形式化驗證尤其重要，因為許多加密組件都遵循嚴格的數學或邏輯規則：
- 共識機制遵循既定協議。
- 智能合約執行確定性操作。
- 零知識協議依賴於密碼學的正確性。
- 橋接和卷疊依賴於可驗證的狀態變化。
佈特林指出，諸如STARK、ZK-EVM、共識協議和後量子密碼學等領域是人工智能輔助驗證的有前景候選方向。
這些系統可能非常復雜，僅靠人工審核可能無法有效擴展。
為什麼形式化驗證無法保證完全的密碼安全
盡管形式化驗證前景可觀，但它仍存在重要局限性。其主要挑戰在於，證明僅能確認模型中明確定義的內容。
如果底層假設不完整、不正確或不切實際，即使經過驗證的代碼也可能失效。證明的可靠性僅取決於其所基於的規范。
例如，經過驗證的代碼仍可能因以下原因而失敗：
- 關於用戶行為的錯誤假設
- 有缺陷的外部數據源
- 硬件漏洞
- 編譯器錯誤
- 側信道攻擊
- 治理幹預
- 跨鏈連接故障
- 模型范圍之外的金融攻擊
Buterin還指出，形式化驗證可能會忽略‘未建模的假設’及其他未解決的組成部分。
即使經過數學驗證的橋接合約，仍可能遇到問題，如果：
- 驗證者惡意串通。
- 底層密碼學變得脆弱。
- 外部組件表現異常。
- 規范存在邏輯漏洞。
形式化驗證可降低與軟件相關的風險，但無法消除更廣泛的系統性風險。
人工智能帶來新挑戰
人工智能輔助驗證也帶來瞭額外的擔憂。大型語言模型能夠生成看似令人信服但實際上並不正確的邏輯。專傢們持續指出，此類風險包括幻覺、不可靠的證明，以及自然語言描述與形式化規范之間的不匹配。
研究表明，人工智能生成的證明可能難以應對：
- 復雜的相互依賴關系
- 代碼結構的變更
- 模糊的需求
- 冗長的推理鏈條
- 開發工具的更新
人工智能或許能加快驗證流程，但它無法完全取代熟練的人工監督。
此外，還存在一個更廣泛的問題：人工智能輔助的驗證工具可能會變得過於復雜，以至於隻有少數技術專傢才能真正理解或評估它們。這可能與加密系統通常所倡導的透明性和廣泛參與相沖突。
你知道嗎？人工智能系統正越來越多地被網絡攻擊者和防禦者用於網絡安全領域。雖然開發人員希望人工智能能夠更快速地驗證代碼安全性，但攻擊者也可能利用人工智能工具來識別漏洞、自動化部分漏洞發現過程，並大規模分析協議弱點。
為什麼‘足夠安全’比‘完全無漏洞’更重要
加密安全最終可能不再那麼註重追求完美，而更側重於降低重大故障發生的可能性。
形式化驗證已能讓開發者證明智能合約和協議的重要屬性。人工智能有望使這些方法更快、更經濟且更易於擴展。
僅此進展就能提升以下領域的安全性：
- 錢包應用
- 第二層網絡
- 零知識系統
- 穩定幣基礎設施
- 共識軟件
- 後量子密碼系統
然而，“數學上已證明”絕不能被誤解為“不可能出錯”。
現實世界中的系統融合瞭代碼、人員、經濟激勵和治理結構。數學能夠強化這一系統中的某個部分，但無法消除所有不確定性來源。
佈特林的提議有助於加密貨幣建立更可靠的基礎。但不太可能打造一個完全不受黑客攻擊、惡意攻擊和系統故障影響的生態系統。
人工智能輔助的形式化驗證或將成為加密安全實踐的寶貴補充，而非徹底解決軟件漏洞及更廣泛的系統性風險的方案。
以上就是解鎖形式化驗證新潛力：維塔利克·佈特林闡述 AI 帶來的安全升級價值的詳細內容，更多關於維塔利克：AI助形式化驗證的資料請關註腳本之傢其它相關文章！
原创文章，作者：fanbi，如若转载，请注明出处：https://www.fanbi.net/archives/838
