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 ensure that software or systems are working exactly in the same way they were designed. Instead of being dependent only on testing, developers take the help of mathematical proofs that can be checked by a machine to verify that the code is correct. In order to do this, developers can use 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 ensure that it is working correctly. In the formal verification, developers will convert the code into a mathematical object. It allows them to ensure that the system is working in the right way.
Formal verification is not a completely new concept, as it has existed for so many years; however, it was 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 will help them to boost the use cases of formal verification for everyday use.
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 can create code that works in a better way, along with the strong security that current programming methods provide.
In the 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 the 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. Human intelligence would take so much time to execute this process.
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 the protocol will never allow them to spend more than once.
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
