Vitalik: AI assisted formal verification may become the ultimate form of software security development According to TechFlow, on May 19th, Vitalik Buterin posted on his personal blog that formal verification is rapidly emerging in the Ethereum development circle and the broader computing field. This technology verifies the correctness of code by writing automatically verifiable mathematical proofs in mathematical proof tools such as Lean, and is referred to as the "ultimate form of software development" by researchers. The article points out that formal verification is particularly suitable for scenarios where the target is simple but the implementation is complex, including quantum resistant signatures STARKs、 Consensus algorithm and core Ethereum technologies such as ZK-EVM. V God also emphasized that formal verification is not omnipotent, and its limitations lie in the inability to fully capture human intentions, as well as the risk of normative omissions and partially uncovered code. He put forward an optimistic outlook on this: the combination of AI and formal verification will complement each other - AI is responsible for efficiently generating large amounts of code, while formal verification ensures its accuracy. In the future, software security will form an architecture model of "secure core+insecure edge sandbox", and Ethereum will become one of the important security cores.