Vitalik: Ethereum will become an important component of the 'security core', and AI assisted formal verification can enhance code security BlockBeats News: On May 19th, Vitalik Buterin, co-founder of Ethereum, published an in-depth analysis of the current status and prospects of formal verification technology. He believes that combining AI with formal verification will become the "ultimate form of software development" and a key path to maintaining network security in the face of powerful AI opponents. Vitalik pointed out that the core of formal verification is to transform the correctness of code into mathematical theorems that can be automatically verified by computers, thereby ensuring software security through mathematical proofs, rather than relying on traditional testing or manual auditing. He believes that this paradigm is particularly suitable for scenarios where the goal is much simpler than implementation, such as quantum resistant signatures, STARK proof systems, Byzantine fault-tolerant consensus algorithms, and ZK-EVM, which are precisely the core technological components of Ethereum's next phase of upgrade. However, Vitalik also admits that formal verification is not omnipotent. Common failure modes include: only verifying a portion of the code without missing critical defects, security specifications themselves being flawed, and bypass attacks at software and hardware boundaries that are difficult to capture by existing proof models. He emphasized that 'provable correctness' essentially verifies the inherent consistency between different expressions of intent, rather than absolute correctness against human true intentions. Vitalik holds a cautiously optimistic attitude towards the network security challenges brought by AI. He believes that AI assisted formal verification will drive the evolution of software architecture towards a pattern of "secure core and insecure edge": edge components run in sandboxes and are granted minimal permissions; The security core is continuously strengthened through formal methods, carrying the highest level of trust burden in the process of social digitization. Ethereum will become an important component of this security core. [Original link]