- Ethereum has named a technology that could strengthen smart contract security in the AI era.
- According to a Vyper developer, formal verification is becoming critically important.
- It helps find bugs that tests miss.
The Ethereum network team published a guest series of posts by the lead Vyper developer under the pseudonym big_tech_sux, focused on the role of formal verification in an era of rapid AI development.
0/ As AI systems become more powerful, formal verification – which is the discipline of using mathematics to prove computer programs correct – shows more and more promise.
— Ethereum (@ethereum) August 5, 2026
A guest thread by @big_tech_sux, lead developer of @vyperlangpic.twitter.com/3T6H76AVrL
The author argues that progress in LLM is making mathematical proofs of program correctness more accessible, and for smart contracts that manage billions of dollars, formal verification is gradually becoming a necessity.
AI Changes the Approach to Software Verification
The series of posts explains that formal verification is a mathematical method that makes it possible to prove a program works correctly across all possible execution scenarios, not just those covered by tests.
As an example, the author cited the function f(x) = x/2, for which it can be mathematically proven that the result will never exceed the input value.
According to him, this methodology can find extremely rare bugs that are virtually impossible to detect through conventional testing.
“Formal verification can catch 1 in 1 quadrillion edge cases which would never come up during testing – and that edge case is the case that can lead to catastrophic failure,” the author noted.
At the same time, he acknowledged that until recently, using this approach required large teams of experts who built mathematical models of programs and carried out complex proofs.
In the developer’s view, modern LLMs significantly simplify this process as we move closer to AGI.
At the same time, the author emphasized that even with AI, formal verification remains a complex and resource-intensive process. In particular, converting source code into a formal model can introduce inaccuracies that affect the reliability of the results.
AI Development Shifts the Balance between Attack and Defense
The piece notes that the development of artificial intelligence simultaneously increases the effectiveness of both defenders and attackers.
The author recalled an incident in which an unreleased OpenAI model was able to find zero-day vulnerabilities that made it possible to bypass multiple layers of protection.
Against this backdrop, formal verification, according to the author, makes it possible to shift the advantage in favor of defenders.
“While attackers only need to find one sequence of inputs which lets them break (into) a system, defenders can use formal verification to prove robustness against all inputs,” he emphasized.
That is why, for mission-critical software — including smart contracts that manage billions of dollars in user funds — formal verification is becoming “not an option, but a necessary prerequisite.”
It is worth noting that this continues a discussion previously started by Ethereum co-founder Vitalik Buterin regarding the use of AI for formal verification of code.
Сообщение Ethereum Explained How AI Changes Approach to Smart Contract Security появились сначала на INCRYPTED.