On May 18, Ethereum co-founder Vitalik Buterin shared his thoughts on the AI-based formal verification process under the blog post titled “A shallow dive into formal verification.”
Many people have claimed that with AI-assisted bug finding, secure code (and hence trustless anything) will be impossible.
I have a much more optimistic take, and AI-assisted formal verification is a major part of the reason why:https://t.co/0ceMBZ6uqj
— vitalik.eth (@VitalikButerin) May 18, 2026
In this blog post, he shared his views on how the integration of artificial intelligence with formal verification techniques can enhance the development of blockchain and cryptography.
What is Formal Verification?
According to the official blog post shared by Vitalik Buterin, formal verification is a process that uses mathematics to prove that software works exactly the way developers intended. Instead of being dependent only on testing, developers take the help of mathematical proofs that can be verified by a machine to confirm the code works correctly. One method used for this is proof by induction.
Vitalik Buterin has shared an example of a simple Fibonacci sequence to explain this concept.
(Source: vitalik.eth.limo)
In traditional programming, developers write code, and then they check it to make sure it works correctly. In formal verification, developers convert the code into a mathematical model, allowing them to mathematically prove that the system behaves as it is supposed to.
Formal verification is not a completely new concept, as it has existed for so many years; however, it is a complex process and a very uphill task to implement on a large scale. But thanks to the impressive growth in artificial intelligence, this integration will make this job easy for developers. AI will help developers to generate complex proofs to make the process more efficient, which could expand the practical use of formal verification in everyday software development.
How Formal Verification Secures Code and Blockchain Ecosystem
In the blog post, Vitalik Buterin stated that the formal verification will create a “new programming paradigm” for the Ethereum blockchain network. By integrating this new approach of formal verification, developers will be able to write code in very basic programming languages, such as EVM bytecode, assembly, or a language called Lean.
After writing the code, developers will be able to use mathematical proofs that a computer or system can verify automatically. Yoichi Hirai, an expert in the subject of software formal verification, called this the “final form of software development”. According to him, this new method could improve software reliability and security.
In traditional testing methods, developers are only able to check the specific conditions. In this kind of method, there are high chances that they might miss rare bugs that happen only under certain conditions. This problem can be resolved in formal verification.
Vitalik Buterin has proposed that many important parts of Ethereum have security properties that are a perfect fit for formal verification. These parts include STARKs, ZK EVMs, post quantum signatures, consensus rules, and EVM systems. While most systems are very complex, there are some features that can be proven mathematically.
The boom in artificial intelligence is making formal verification more practical for real-world applications. AI technology will allow software to generate mathematical proofs and verify simple-level code, such as EVM bytecode. Performing this process manually can take significant time and expertise.
Vitalik affirmed that, where nowadays AI is being used to exploit vulnerabilities present in the code and smart contracts, formal verification can play a major role in reducing this threat caused by AI.
Instead of resolving bugs in the code one by one, developers will take a mathematical approach to ensure the safety of key properties. For example, they can ensure that a protocol never allows double spending.
This new verification process will provide numerous benefits to blockchain and the entire cryptography system. This includes better bug prevention, as this system will eliminate large categories of errors automatically.
Also Read: THORChain Reveals New Details on $10 Million Exploit
