Vitalik Buterin has published an article discussing the potential applications of formal verification in blockchain security. According to Foresight News, the article highlights a new paradigm emerging in Ethereum's frontier research, which involves writing code directly using EVM bytecode, assembly, or Lean, and verifying its correctness with mathematical proofs that can be automatically checked in Lean. Researcher Yoichi Hirai refers to this paradigm as the 'ultimate form of software development.'
Buterin suggests that AI-assisted formal verification could enhance both code efficiency and security, particularly in critical security modules such as STARK, ZK-EVM, quantum-resistant signatures, and consensus algorithms. However, the article also notes that formal verification is not foolproof and may fail due to incomplete proof coverage, specification errors, or hardware side-channel issues.
Looking ahead, software may divide into 'secure cores' and 'non-secure edges,' with Ethereum positioned as a significant secure core. The exploration of formal verification underscores its potential to bolster blockchain security while acknowledging its limitations.