Vitalik analyzes the development and limitations of formal verification, and the discussion on software development entering the "ultimate form" in the AI era is heating up Odaily Planet Daily News: Ethereum co-founder Vitalik Buterin has published an article titled "A Shallow Dive into Formal Verification", which systematically outlines 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 in the forefront research circle of Ethereum: 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 can improve code efficiency and significantly enhance security, and is referred to as the "ultimate form of software development" by some researchers. Vitalik stated that the core of formal verification is to validate program properties through machine testable mathematical proofs, and its value lies in the ability to shift "security" from empirical testing to provable logical systems. This method has begun to be used for end-to-end verification of critical system behavior in encrypted communication, cryptographic protocols, and blockchain systems such as zero knowledge proofs and consensus mechanisms. The article also points out that the Ethereum ecosystem is exploring formal verification projects for key infrastructure such as EVM implementation, STARK proof system, and anti quantum signature to enhance protocol level security and reliability. However, Vitalik also emphasized that formal verification is not a 'silver bullet'. Its limitations include: security definitions rely on human modeling, some systems are difficult to fully formalize, and hardware or unverified modules may still become attack surfaces. Furthermore, even in the presence of formal proofs, incorrect specifications or uncovered assumptions may still lead to loopholes. Vitalik ultimately proposed that a more realistic approach is to combine formal verification with various methods such as AI assisted programming, type systems, and testing frameworks, gradually improving software security within the framework of "redundant expression of intent and automatic verification of consistency". Under the trend of AI generating code on a large scale, software systems will gradually differentiate into "vulnerable edge modules" and "highly trusted security cores". In the future, formal verification should be applied to core systems (such as blockchain protocols, operating system kernels, etc.) to build verifiable and secure digital infrastructure.