Foreign media: Ethereum co-founder Vitalik Buterin recently posted that as AI participates in code and proof generation, formal verification has the potential to evolve from a niche tool into a more commonly used software development method. This is also his core response to concerns that AI will make writing secure code increasingly difficult.
Formal verification is no longer reliant solely on manual effort.
Formal verification involves using mathematical proofs to confirm that code behaves as expected under specified conditions. It differs from traditional testing, which can only cover a subset of scenarios; formal verification aims to express critical behaviors as machine-checkable proofs.
Buterin believes that the advancement of this technology has been slow in the past, primarily because the cost of writing proofs was too high, and manually completing them was both time-consuming and prone to errors. The role of AI lies in assisting with the generation of both code and proof text, which developers then verify to ensure that the claimed behavior truly matches the intended software behavior.
Multiple directions on Ethereum are already being explored.
The article notes that formal verification has been advanced in some foundational technologies within the Ethereum ecosystem, including post-quantum signatures, the STARK proof system, consensus algorithms, and ZK-EVM. These systems are complex, but their security goals are often well-defined.
Buterin cited examples of projects attempting to build formally verified STARK implementations, teams advancing EVM implementations written in RISC-V assembly and mathematically verified against readable reference implementations, and Byzantine fault-tolerant consensus protocols being formally specified and verified using tools like Lean.
He also acknowledged that there are boundaries.
Buterin did not describe formal verification as a silver bullet. He noted that proofs may only cover parts of the system, leaving unverified sections potentially vulnerable; developers might also overlook critical properties, or the initial formal specification itself could be flawed.
Additionally, side-channel attacks at the hardware level and other issues may bypass software implementations that are “mathematically correct.” In other words, formal verification can enhance the trustworthiness of critical modules, but it does not automatically equate to “absolutely correct” in every real-world sense.
The key system will be smaller and harder.
Buterin described a direction that splits software into two layers: one responsible for low-risk functions with limited permissions, running in an isolated environment; the other retains only the most critical core capabilities, such as Ethereum itself, the operating system kernel, or sensitive IoT infrastructure.
In his view, the smaller core system is the one that truly requires intensive protection. The computational and generative capabilities provided by AI may enable formal verification to be widely deployed for the first time. The ultimate goal is not “zero vulnerabilities,” but rather ensuring that the most critical software components are no longer primarily reliant on experience and luck, but are instead built on a more verifiable foundation.