Vitalik: AI-assisted formal verification is expected to improve both code efficiency and security

Foresight News reports that Vitalik Buterin has published an article exploring the application prospects of formal verification in blockchain security. The article points out that a new paradigm is emerging in Ethereum's frontier research: directly writing code using EVM bytecode, assembly, or Lean, and verifying its correctness with mathematical proofs in Lean that can be automatically checked. Researcher Yoichi Hirai refers to this paradigm as the "final form of software development." Vitalik believes that AI-assisted formal verification is expected to improve both the efficiency and security of code, and is particularly suitable for core security modules such as STARK, ZK-EVM, post-quantum signatures, and consensus algorithms. The article also emphasizes that formal verification is not a panacea and can still fail due to incomplete proof coverage, specification errors, or hardware side channels. In the future, software may split into "security cores" and "non-security peripheries," with Ethereum becoming one of the key security cores.