Vitalik Analyzes the Development and Limitations of Formal Verification, Discussion on Software Development Entering the "Ultimate Form" in the AI Era Heats Up

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

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

The article also notes that the Ethereum ecosystem is exploring formal verification projects for key infrastructure, including EVM implementations, STARK proving 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 may still become attack surfaces. Furthermore, even when a formal proof exists, specification errors or uncovered assumptions can still lead to vulnerabilities.

Finally, Vitalik proposed that a more realistic path is to combine formal verification with various methods such as AI-assisted programming, type systems, and testing frameworks, to gradually improve software security under a framework of "redundantly expressing intent and automatically verifying consistency." Amidst 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 concentrated on core systems (such as blockchain protocols, operating system kernels, etc.) to build a verifiably secure digital infrastructure.