Vitalik: AI-assisted formal verification may become the "ultimate form of software development"

On May 18, Vitalik published a blog post stating that the Ethereum community is attempting to use formalization tools like Lean to directly write code at the underlying language level (such as EVM bytecode, RISC-V assembly) and guarantee correctness and security through machine-verifiable mathematical proofs. Vitalik pointed out that formal verification can be used to verify the end-to-end security and equivalence of cryptographic communication protocols like Signal, TLS, STARK, ZK-EVM, consensus algorithms, and EVM implementations, and can significantly enhance the defender's advantage in the new environment of AI automatically finding bugs. However, he also emphasized that formal verification is not a panacea and is prone to risks such as unmodeled assumptions, side channels, and uncovered modules. Vitalik believes that future software will be built around a small number of "secure cores," with AI responsible for generating a large amount of code and formal verification responsible for ensuring the security of critical infrastructure.