Buterin有信心，最終可能發生相反的情況：AI或許會賦予防禦者所需的工具，從一開始就能建立顯著更難被利用的軟體。
「關於AI駭客意味著網絡安全註定失敗的觀點越來越常見。我不同意，」Buterin週三在X社群平台發佈的一篇冗長且內容詳實的貼文中寫道。
根據這位Ethereum聯合創辦人的說法，一旦開發者開始充分利用形式化驗證，網絡安全自然應該偏向防禦者。
Buterin還將這種信念直接與自己接觸加密貨幣的經歷聯繫起來，透露他大約90%的淨資產仍在crypto中。
他認為，任何繼續持有大量cryptocurrency的人，實際上都是在隱含地押注：即使面對日益複雜的攻擊者，也能構建出足夠安全的數位系統。
「如果AI能證明Navier-Stokes與FLT，那麼AI也能將『這個程式是安全的』這個陳述作為一個數學定理來證明，」Buterin寫道，指的是Navier-Stokes問題和Fermat's Last Theorem。
他的論點基於形式化驗證，即以數學方式證明軟體滿足特定屬性的方法。
Buterin在5月的一篇文章中也廣泛討論過這一想法，認為AI輔助形式化驗證將成為安全關鍵軟體變革性的工具。然而，要證明這類軟體的安全性，可能依舊充滿挑戰。
定義問題
Buterin以加密即時通訊應用Signal作為例子，說明為何這可能很困難。
攻擊者可能試圖偽造訊息、阻止訊息送達、重放舊訊息、入侵伺服器、操控發現他人公鑰的過程，或利用作業系統中的某個漏洞。
其他問題也可能來自受損的資料庫、惡意的程式庫、編譯器，甚至硬體層級的資訊洩漏。
即使對話內容維持加密，攻擊者仍可能知悉通訊雙方是誰。因此，對於「安全」這個詞背後數學定義本身，都可能變得極為複雜。
「所以……連定義本身都可能超過一千行程式碼，且需要深入且謹慎的思考去釐清，」Buterin寫道。
攻擊者與防禦者
毫無疑問，更強大的AI系統可能使尋找漏洞變得更容易。
但同樣的機器推理能力提升，也可能大幅降低以形式方式證明軟體依據嚴謹安全規範運作的成本。
雙方都將擁有AI。
