Vitalik Buterin, co-founder of Ethereum, suggests that combining artificial intelligence with formal verification could become the definitive method for software development. In a blog post from May 18, he argues that while AI can generate code rapidly, it lacks the reliability required for critical systems. Formal verification provides a mathematical proof of code correctness, addressing the risks inherent in smart contracts.
Buterin highlights the Lean theorem prover as a key tool for creating mechanically checked proofs. He notes that this approach is essential for developing quantum-resistant signatures and complex zero-knowledge proofs, which are central to Ethereum's scaling strategy. Projects like Arklib and evm-asm are currently applying these methods to improve the security of STARKs and the Ethereum Virtual Machine.
Despite the potential, Buterin identifies two major limitations: specification risk, where the initial requirements might be flawed, and hardware vulnerabilities that formal verification cannot address. He emphasizes that AI reduces the human effort needed for writing proofs, making this rigorous security approach economically viable for a broader range of software applications beyond aerospace and defense.
