Vitalik Buterin shared in his latest article that a new paradigm is emerging in Ethereum's frontier development: directly writing code using EVM bytecode, assembly, or Lean, and verifying its correctness with mathematical proofs that can be automatically checked in Lean. AI-assisted formal verification is expected to simultaneously improve code efficiency and security, especially for critical security modules like STARK, ZK-EVM, post-quantum signatures, and consensus algorithms. However, he also emphasized that formal verification is not a silver bullet and can still fail due to incomplete proof coverage, specification errors, hardware side channels, and other issues. In the future, software may split into "secure cores" and "non-secure edges," with Ethereum becoming one of the key secure cores. https://(wublock123.com)/news/vitalik-ai-assisted-formal-verification-ethereum-security-61259