“If you formally verify end-to-end, then you are proving not just that some description of the protocol is secure in theory, but that the specific piece of code that the user runs is secure in practice,” he wrote. “From a user's perspective, this greatly improves trustlessness: In order to fully trust the code, you don't need to check over the entire code, you simply need to check over the statements that are proven about it.”
“Bugs in computer code are scary,” Buterin wrote.
Undiscovered bugs can be devastating for crypto projects, where software flaws can be exploited to permanently steal users' funds with little chance of recovery.
Buterin said formal verification could also improve trust in AI-generated software by proving that optimized low-level code matches a more readable reference implementation.
“A huge part of the value-add is that the proofs are truly end-to-end,” Buterin wrote. “Often, the nastiest bugs are interaction bugs that sit at the edge of two sub-systems that are considered separately.”
However, while Buterin sees the potential for AI to help secure crypto network code, he cautioned that formal verification cannot fully eliminate security risks.
“Formal verification is not a panacea. But it is particularly well-suited for situations where the goal is much simpler than the implementation,” he wrote. “This is particularly true in some of the most devilishly hard pieces of technology that we will need to deploy in the next major iteration of Ethereum: quantum-resistant signatures, STARKs, consensus algorithms, and ZK-EVMs.”
Buterin rejected the idea that increasingly advanced cyberattacks will eventually make open-source software or decentralized systems impossible to secure.
“This would be a bleak future for cybersecurity. It's especially an extremely bleak future for those of us who care about internet decentralization and freedom,” he said. “The entire cypherpunk ethos is fundamentally based on the idea that on the internet, the defender has an advantage.”
Instead, Buterin argued that future systems will likely depend on highly secured “core” infrastructure protected through formal verification and restricted security environments.
“When it comes to the secure core, we don't let the buggy code multiply,” he said. “We act aggressively to keep the size of the secure core small, and indeed even shrink it further.”
