Vitalik's latest long article: In the age of AI, how can code become safer?

Original title: A shallow dive into formal verification

Original author: Vitalik

Original compiled by: Peggy, BlockBeats

Editor's note: As AI coding capabilities rapidly improve, software security is facing a new paradox: AI can generate code more efficiently, but it can also find vulnerabilities more efficiently. This issue is particularly critical for the crypto industry. Defects in smart contracts, ZK proofs, consensus algorithms, and on-chain asset systems often lead not to ordinary software errors, but to irreversible fund losses and a collapse of trust.

What Vitalik discusses in this article is another path for code security in the age of AI: formal verification. Simply put, it doesn't rely on human auditors checking code line by line. Instead, it writes the properties a program should satisfy as mathematical propositions and then uses machine-checkable proofs to verify whether these properties hold. In the past, formal verification remained a relatively niche research and engineering domain due to its high barrier to entry and tedious process. However, as AI can assist in writing code and proofs, this approach is regaining practical significance.

The core judgment of the article is not that "formal verification can solve all security problems." On the contrary, Vitalik repeatedly reminds us that so-called "provable security" does not equal absolute security: proofs may miss key assumptions, the specification itself might be wrong, and unverified code, hardware boundaries, and side-channel attacks can become new sources of risk. Yet it still offers a more reliable security paradigm: expressing the developer's intent in multiple ways, then letting the system automatically check whether these expressions are compatible with each other.

This is particularly important for Ethereum. The future Ethereum will increasingly rely on complex underlying components, including STARKs, ZK-EVMs, quantum-resistant signatures, consensus algorithms, and high-performance EVM implementations. The implementation of these systems is extremely complex, but their core security objectives can often be relatively clearly formalized. It is precisely in such scenarios that AI-assisted formal verification has the potential to deliver maximum value: letting AI handle writing efficient code and proofs, while leaving humans to check whether the final proven propositions truly correspond to the security goals they intend to achieve.

From a broader perspective, this article is also Vitalik's response to cybersecurity in the AI era. Facing stronger AI attackers, the answer is not to give up open source, abandon smart contracts, or re-rely on a few centralized institutions. Instead, it is to compress critical systems into smaller, more verifiable, and more trustworthy "security cores." AI will lead to a massive increase in rough code, but it may also make truly important code safer than ever before.

The following is the original text:

Special thanks to Yoichi Hirai, Justin Drake, Nadim Kobeissi, and Alex Hicks for their feedback and review on this article.

Over the past few months, a new programming paradigm has been rapidly emerging within Ethereum's frontier R&D circles and many other corners of the computing world: developers writing code directly in very low-level languages, such as EVM bytecode, assembly language, or Lean, and then verifying its correctness by writing automatically checkable mathematical proofs in Lean.

When used correctly, this approach has the potential to produce both extremely efficient code and be significantly safer than past software development methods. Yoichi Hirai calls it "the final form of software development." This article will attempt to explain the basic logic behind this approach: what formal verification of software can do, and what its limitations and boundaries are—both within the Ethereum context and in the broader field of software development.

What is formal verification?

Formal verification refers to the process of writing proofs of mathematical theorems in a way that can be automatically checked by a machine.

To give a relatively simple but still interesting example, consider a basic theorem about the Fibonacci sequence: every third number is even, and the other two are odd.

A simple proof method uses mathematical induction, advancing three numbers at a time.

First, look at the base cases. Let F1 = F2 = 1, F3 = 2. By direct observation, the proposition—"when i is a multiple of 3, Fi is even; otherwise, Fi is odd"—holds true up to x = 3.

Next, the induction step. Assume the proposition holds up to 3k+3, meaning we already know that the parity of F3k+1, F3k+2, and F3k+3 is odd, odd, and even respectively. Then, we can calculate the parity of the next three numbers:

Thus, we have completed the derivation from "the known proposition holds up to 3k+3" to "confirming that the proposition also holds up to 3k+6." By repeating this reasoning, we can be confident that the rule holds for all integers.

This argument is convincing to a human. But what if you want to prove something a hundred times more complex, and you really want to be sure you haven't made a mistake? Then you can construct a proof that a computer can also be convinced by.

It would look roughly like this:

This is the same reasoning, but expressed in Lean. Lean is a programming language often used for writing and verifying mathematical proofs.

It looks quite different from the "human version" I gave above, and there's a good reason for that: what is intuitive to a computer is completely different from what is intuitive to a human. The computer I'm referring to here is the "old-school" computer—a "deterministic" program made of if/then statements, not a large language model.

In the proof above, you are not just stating the fact that fib(3k+4) = fib(3k+3) + fib(3k+2); you are stating that fib(3k+3) + fib(3k+2) is odd, and the rather grandly named omega tactic in Lean automatically combines this with its understanding of the definition of fib(3k+4).

In more complex proofs, you sometimes have to explicitly state at each step which specific mathematical law allows you to take that step, and these laws sometimes have obscure names like Prod.mk.inj. On the other hand, you can also expand huge polynomial expressions in a single step, completing the argument with just one line of code using something like omega or ring.

This unintuitiveness and tedium are major reasons why machine-verifiable proofs, despite existing for nearly 60 years, have remained a niche field. But at the same time, many things that were almost impossible in the past are rapidly becoming feasible due to the rapid progress of AI.

Verifying computer programs

At this point, you might be thinking: okay, so we can let computers verify proofs of mathematical theorems, and we can finally determine which of those crazy new findings about prime numbers are true and which are just errors hidden in hundreds of pages of PDF papers. Maybe we can even figure out if Shinichi Mochizuki's proof of the ABC conjecture is correct! But besides satisfying our curiosity, what practical significance does this have?

There are many answers. And for me, a very important one is: verifying the correctness of computer programs, especially those involving cryptography or security. After all, a computer program itself is a mathematical object. Therefore, proving that a computer program will behave in a certain way is essentially proving a mathematical theorem.

For example, suppose you want to prove whether encrypted communication software like Signal is truly secure. You could first write down mathematically what "secure" means in this context. Generally speaking, you need to prove that, under certain cryptographic assumptions, only the person holding the private key can learn any information about the message content. In reality, there are, of course, many important security properties.

And it turns out there is already a team working on figuring this out. One of the security theorems they propose looks roughly like this:

Here is Leanstral's summary of the meaning of this theorem:

The passive_secrecy_le_ddh theorem is a tight reduction showing that, under the Random Oracle Model, the passive message secrecy of X3DH is at least as hard to break as the DDH assumption.

In other words, if an attacker can break the passive message secrecy of X3DH, then they can also break DDH. Since DDH is generally assumed to be hard, X3DH can be considered secure against passive attacks.

The theorem proves that if an attacker can only passively observe Signal's key exchange messages, they cannot distinguish the final session key from a random key with a non-negligible probability advantage.

If combined with another proof showing that AES encryption is correctly implemented, you then have a proof that the encryption mechanism of the Signal protocol is secure against passive attackers.

Similar verification projects also exist that prove secure implementations of TLS and other in-browser cryptographic components.

If you achieve end-to-end formal verification, you are proving not just that a protocol description is theoretically secure, but that the specific piece of code the user actually runs is secure in practice. From the user's perspective, this greatly increases the degree of "trustlessness": to fully trust this code, you don't need to review the entire codebase line by line; you only need to check the statements that have been proven true.

Of course, there are some very important asterisks here, especially regarding what exactly the keyword "secure" means. It's easy to forget to prove the claims that really matter; it's also easy to encounter a situation where the claim that needs to be proven has no simpler description than the code itself; it's also easy to sneak in assumptions during the proof that ultimately aren't true. You might also easily decide that only a specific part of the system needs formal proving, only to be hit by a critical vulnerability in another part, or even at the hardware level. Even the implementation of Lean itself could have bugs. But before diving into these headache-inducing details, let's take a further look at what a nearly utopian prospect could look like if formal verification were ideally and correctly executed.

Formal verification for security

Bugs in computer code are already concerning.

When you put cryptocurrency into an immutable on-chain smart contract, code bugs become much scarier. Because once the code fails, North Korean hackers could automatically drain all your money, and you would have almost no recourse.

When all this is wrapped in zero-knowledge proofs, code bugs become even scarier. Because if someone successfully breaks the zero-knowledge proof system, they could withdraw all the funds, and we might have no idea what went wrong—or worse, we might not even know that a problem occurred.

When we have powerful AI models, code bugs become even scarier. For instance, a model like Claude Mythos, after another two years of improvement, might be able to automate the discovery of these vulnerabilities.

Faced with this reality, some people argue for abandoning the basic concept of smart contracts, or even believe that cyberspace cannot be a domain where defenders have an asymmetric advantage over attackers.

Here are some quotes:

To harden a system, you need to spend more tokens on finding vulnerabilities than an attacker spends on exploiting them.

And:

Our industry was built around deterministic code. Write code, test it, ship it, and know it works—but in my experience, this contract is breaking down. Among top operators of truly AI-native companies, codebases are starting to become something you "trust will work," and the probability corresponding to that trust can no longer be precisely articulated.

Worse still, some believe the only solution is to give up open source.

This would be a bleak future for cybersecurity. Especially for those who care about the decentralization and freedom of the internet, it would be an extremely bleak future. The entire cypherpunk spirit is fundamentally built on the idea that on the internet, the defender has the advantage. Building a digital "castle"—whether it manifests as encryption, signatures, or proofs—is far easier than destroying it. If we lose this, then internet security can only come from economies of scale, from hunting down potential attackers worldwide, and more broadly, from a binary choice: dominate everything or face destruction.

I disagree with this assessment. I have a much more optimistic vision for the future of cybersecurity.

I believe that the challenge posed by powerful AI vulnerability discovery is serious, but it is a transitional challenge. Once the dust settles and we reach a new equilibrium, I think we will arrive at a state that is more favorable to the defender than the past.

Mozilla agrees with this. To quote them:

You may need to reprioritize all other affairs and dedicate yourself to this task in a sustained and focused manner. But there is light at the end of the tunnel. We are very proud to see how the team has stepped up to meet this challenge, and others will too. Our work is not done, but we have passed the inflection point and are beginning to see a better future that far exceeds just "barely keeping up." The defenders finally have a chance for a decisive victory.

...

The number of flaws is finite, and we are entering a world where we can finally find them all.

Now, if you do Ctrl+F in that Mozilla article for "formal" and "verification," you'll find neither word appears. A positive future for cybersecurity does not strictly depend on formal verification, nor on any other single technology.

So what does it depend on? Basically, it's the picture below:

Over the past few decades, many technologies have driven the trend of "decreasing number of vulnerabilities":

Type systems;

Memory-safe languages;

Software architecture improvements, including sandboxing, permission mechanisms, and more generally, a clear distinction between the "trusted computing base" and "other code";

Better testing methods;

Accumulated knowledge about secure and insecure coding patterns;

An increasing number of pre-written and audited software libraries.

AI-assisted formal verification should not be seen as a completely new paradigm, but rather as a powerful accelerator: it is accelerating a trend and paradigm that has been moving forward for a long time.

Formal verification is not a panacea. But it is particularly suitable in certain scenarios: specifically, when the goal is simpler than its implementation. This is especially evident in some of the most challenging technologies needed for Ethereum's next major iteration, such as quantum-resistant signatures, STARKs, consensus algorithms, and ZK-EVMs.

STARK is a very complex piece of software. But the core security property it achieves is easy to understand and easy to formalize: If you see a proof pointing to the hash H of program P, input x, and output y, then either the hash algorithm used by STARK has been broken, or P(x) = y. Hence, we have the Arklib project, which aims to create a fully formally verified STARK implementation. Another related project is VCV-io, which provides foundational oracle computation infrastructure for formal verification of various cryptographic protocols, many of which are themselves dependency components of STARKs.

More ambitious is evm-asm: a project attempting to build a complete EVM implementation and formally verify it. Here, the security properties are less clear-cut. Simply put, its goal is to prove that this implementation is equivalent to another EVM implementation written in Lean, which can prioritize intuitiveness and readability without considering runtime efficiency.

Of course, in theory, a situation could arise where we have ten EVM implementations, all proven equivalent to each other, yet all share the same fatal flaw, somehow allowing an attacker to drain all ETH from an address they don't have permission to control. However, the probability of this happening is much lower than the probability of such a flaw existing in a single EVM implementation today. Another security property we only truly appreciated after painful experience—DoS resistance—is relatively easy to specify formally.

Two other important directions are:

Byzantine fault-tolerant consensus. In this direction, formally defining all desired security properties is also not easy. But given that related bugs have been very common, attempting formal verification is still worthwhile. Therefore, there are already ongoing works on Lean consensus implementations and their proofs.

Smart contract programming languages. Related examples include formal verification efforts in Vyper and Verity.

In all these cases, a huge added value of formal verification is that these proofs are truly end-to-end. Many of the trickiest bugs are interaction bugs, occurring at the boundaries of two subsystems considered separately. End-to-end reasoning about the entire system is too difficult for humans, but automated rule-checking systems can do it.

Formal verification for efficiency

Let's look at evm-asm again. It is an EVM implementation.

But it is an EVM implementation written directly in RISC-V assembly language.

Literally assembly.

Here is the ADD opcode:

The choice of RISC-V is because ZK-EVM provers currently under construction typically work by proving RISC-V and compiling the Ethereum client to RISC-V. Therefore, if