Vitalik Buterin has outlined how artificial intelligence, combined with formal verification, could significantly improve software security in blockchain systems. In a blog post published on May 18, Buterin explored the pairing of AI's code-generation speed with mathematical rigor to enhance security for Ethereum's infrastructure.
Buterin acknowledged that while AI can generate large volumes of code quickly, the output tends to be less accurate than code produced by careful human developers. Formal verification uses mathematical proofs to demonstrate that code behaves correctly across all possible scenarios, rather than relying solely on testing specific cases.
The Formal Verification Approach
Buterin specifically highlighted the Lean theorem prover as a key tool, which allows developers to write proofs that can be mechanically verified. This creates a layer of mathematical certainty that traditional code review cannot match.
He acknowledged concerns that AI could also be used by attackers to find bugs faster, but argued this concern is "transient." A verified proof, once confirmed, remains permanent, whereas an attacker finding a bug is a one-time event.
Ethereum's Critical Use Cases
Buterin identified two areas where formal verification is particularly important for Ethereum. Post-quantum cryptography becomes essential as quantum computers approach capability to break current encryption schemes. Zero-knowledge proofs are central to Ethereum's scaling strategy through ZK-EVMs and rollups, where subtle bugs in these complex cryptographic systems could compromise entire Layer 2 networks.
Buterin cited two ongoing projects: Arklib, a formally verified implementation of STARKs, and evm-asm, an EVM abstraction designed to make Ethereum's virtual machine more amenable to formal analysis.
Limitations and Economics
Buterin identified two significant limitations. Specification risk occurs when code matches its specification but the specification itself is incorrect. Hardware presents a second challenge, as physical chips running verified software cannot be verified with the same rigor, and a compromised processor could undermine even perfectly verified code.
Despite these caveats, Buterin described AI-assisted formal verification as potentially the "final form" of software development. Formal verification has existed since the 1950s and 1960s but remained confined primarily to aerospace and defense where the cost of mathematical proof justified the cost of failure. AI is now changing the economics by reducing the human effort required to write both code and proofs, potentially making formal verification practical for a wider range of software.
