Vitalik Buterin Touts AI-Formal Verification Combo for Secure Software Development
Vitalik Buterin, co-founder of Ethereum, has proposed an innovative solution to enhance software security against hacking. He believes that artificial intelligence (AI) can be used in conjunction with formal verification to create highly secure code.
Buterin's proposal involves pairing AI's ability to generate code quickly with the mathematical rigor of formal verification. This combination could significantly improve the security of software systems, especially those underpinning Ethereum's infrastructure. Formal verification uses mathematical proofs to demonstrate that code behaves correctly in all possible scenarios.
The Lean theorem prover is a key tool in this space, allowing developers to write proofs that can be mechanically checked. Buterin acknowledged a common objection that AI might also be used by attackers to find bugs faster, but argued that this concern is 'transient' and that a verified proof once confirmed is permanent.
Ethereum's post-quantum cryptography and zero-knowledge proofs are areas where formal verification offers a path to confidence that testing alone cannot provide. Buterin cited two ongoing projects as examples of this work in practice, including Arklib and evm-asm.