PANews 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. Vitalik believes that future software will be built around a small number of "security cores," with AI handling the majority of code generation and formal verification responsible for ensuring the security of critical infrastructure.