Vitalik: AI assisted formal verification may become the final form of software development Vitalik posted a blog post stating that the Ethereum community is attempting to use formal tools such as Lean to directly write code in underlying languages such as EVM bytecode and RISC V assembly, and ensure correctness and security through machine verifiable mathematical proofs. Vitalik pointed out that formal verification can be used to verify encrypted communication protocols such as Signal TLS、STARK、ZK‑EVM、 The end-to-end security and equivalence of consensus algorithms and EVM implementation significantly enhance the defense advantage in the new environment of AI automatically finding bugs. However, he also emphasized that formal verification is not omnipotent and can easily overlook risks such as unmodeled assumptions, side channels, and uncovered modules.