Vitalik analyzes the development and limitations of formal verification, discussions on the "ultimate form" of software development in the AI era heat up

Odaily Planet Daily News: Ethereum co-founder Vitalik Buterin published an article titled "A shallow dive into formal verification," systematically reviewing the latest developments and limitations of formal verification in Ethereum and the broader computing field. The article points out that in recent months, a new programming paradigm is rapidly emerging within Ethereum's frontier research circles: developers directly use very low-level languages (such as EVM bytecode, assembly) or Lean, and verify code correctness through automatically verifiable mathematical proofs. This method theoretically improves both code efficiency and significantly enhances security, being called the "ultimate form of software development" by some researchers.

Vitalik stated that the core of formal verification is verifying program properties through machine-checkable mathematical proofs. Its value lies in shifting "security" from empirical testing to a provable logical system. In encryption communication, cryptographic protocols, and blockchain systems (such as zero-knowledge proofs and consensus mechanisms), this method has begun to be used for end-to-end verification of key system behaviors.

The article also points out that the Ethereum ecosystem is exploring formal verification projects for key infrastructure, including EVM implementations, STARK proof systems, and post-quantum signatures, to enhance protocol-level security and reliability. However, Vitalik also emphasized that formal verification is not a "silver bullet." Its limitations include: security definitions depend on human modeling, some systems are difficult to fully formalize, and hardware or non-verified modules can still become attack surfaces. Additionally, even in the presence of formal proofs, specification errors or uncovered assumptions can still lead to vulnerabilities.

Finally, Vitalik proposed that a more realistic path is to combine formal verification with AI-assisted programming, type systems, testing frameworks, and other methods. Within a framework of "redundantly expressing intentions and automatically verifying consistency," software security can be gradually improved. Amid the trend of AI generating code on a large scale, software systems will gradually differentiate into "vulnerable edge modules" and "highly trustworthy security cores." In the future, formal verification should be concentratedly applied to core systems (such as blockchain protocols, operating system kernels, etc.) to build a digitally verifiable security infrastructure.