Vitalik 最新文章探討「形式驗證」：結合 AI 將是軟體開發最終形態，賦予以太坊極致安全

📄完整原文· 由 trafilatura 自動擷取Gemini 翻譯1505 字

Is the final form of software development here? Ethereum co-founder Vitalik Buterin published a long-form article today (18th) exploring the immense potential of combining "Formal Verification" with AI. He pointed out that writing code in low-level languages and using the Lean language for automated computer verification will empower the Ethereum EVM and ZK systems with unprecedented security and efficiency. Vitalik asserts that while AI may exacerbate vulnerability exploits in the short term, the defensive side will ultimately gain an overwhelming advantage with the aid of formal verification. (Previous coverage: Vitalik: Don't try to fight AI, build a sanctuary for humanity instead) (Background: Vitalik in conversation with Xiao Feng in Hong Kong: Simplifying the Ethereum system is the top priority; if it becomes so complex that only 50 people understand it, developers and users will be scared away) In the world of blockchain, code vulnerabilities often mean tens of millions of dollars evaporating overnight. To address this fatal pain point, Ethereum co-founder Vitalik Buterin has provided his ultimate solution. Vitalik released a new article today (18th) titled "A shallow dive into formal verification." He observed that a new programming paradigm has been rapidly emerging in the Ethereum frontier research circle over the past few months: writing code directly in extremely low-level languages (such as EVM bytecode or assembly) and pairing it with the Lean language to write "mathematical proofs" that computers can automatically check. Vitalik cited developer Yoichi Hirai, hailing this combination as the "final form of software development." Simply put, formal verification is the process of writing proofs for mathematical theorems in a way that computers can automatically and rigorously check. Vitalik illustrated that unlike human intuitive deduction, in the Lean language, developers can convert the security of cryptographic protocols (such as Signal) into theorems. By proving the security of the X3DH key exchange and the correctness of AES implementations, computers can provide "end-to-end" guarantees: no one except the user holding the private key can read the messages. This method of turning program behavior into rigorous mathematical verification significantly enhances the system's Trustlessness. In the cryptocurrency and ZK (Zero-Knowledge Proof) fields, bugs are extremely dangerous. Smart contract errors can lead to stolen funds that cannot be recovered, and bugs in ZK systems can even be maliciously exploited without anyone noticing. With the future emergence of advanced AI (such as Claude Mythos), AI will possess the terrifying capability to automatically discover "Zero-day" vulnerabilities. Faced with this security threat, many are pessimistic, believing that defense will never outperform offense. However, Vitalik presented a strong counter-argument and an optimistic vision: "AI finding vulnerabilities is only a transitional challenge. With the help of formal verification, we will eventually enter a new equilibrium where the 'defensive side' gains a significant advantage." Vitalik firmly believes that formal verification gives us the ability to "prove that everything is correct." The article delves into the current practical applications of formal verification in the Ethereum ecosystem, particularly in EVM implementations and the ZK-EVM field. The developer community is currently attempting to write a RISC-V assembly version of the EVM using the Lean language and proving its absolute correctness in Gas calculation and stack operations. Vitalik depicted an exciting future workflow: AI is responsible for generating highly efficient low-level assembly code, and then formal verification ensures that this code is 100% correct. This means developers can return to efficient low-level development while maintaining the system's understandability and absolute security. Although formal verification currently faces limitations such as high proof complexity, time consumption, and the possibility of errors in the Specification itself, Vitalik predicts that AI will significantly accelerate the proof-writing process, moving formal verification from a niche technology to the mainstream. This will not only give birth to a more secure internet and decentralized systems but also perfectly realize the ultimate ideal of the Cypherpunk.

資料狀態✓ 已擷取全文閱讀原文（動區 BlockTempo）

🔍歷史類似事件· 關鍵字 + 標的比對1 則

2026-05-18

Vitalik：別試著對抗 AI，而是為人類建一個庇護所

相似度 120%關鍵字 vitalik同分類 zh

💡 目前用關鍵字 + 標的比對（MVP）· 之後會升級為 embedding 語意搜尋

原始資訊

ID：d4d77aa407

來源：動區 BlockTempo

發佈：2026-05-18 12:40:34

分類：zh_news · 導出分類 zh

標的：未指定

社群投票：+0 / −0 · ⭐ 0 重要 · 💬 0 留言