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

CoinFeed reported on May 18th that Vitalik Buterin published a blog post stating that the Ethereum community is experimenting with using formal tools like Lean to write code directly in underlying languages ​​(such as EVM bytecode and RISC-V assembly) and ensuring 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, significantly enhancing the defender's advantage in the new environment where AI automatically finds bugs. However, he also emphasized that formal verification is not a panacea and can easily overlook risks such as unmodeled assumptions, side channels, and uncovered modules.