Vitalik's latest long-read: In the age of AI, how can code become more secure?

Original title: A shallow dive into formal verification

Original author: Vitalik

Original translation: Peggy, BlockBeats

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

What Vitalik discusses in this article is another path for code security in the AI era: formal verification. Simply put, it doesn't rely on human auditors checking code line by line. Instead, the properties a program should satisfy are written as mathematical propositions, and machine-checkable proofs are used to verify whether these properties hold. In the past, formal verification remained a relatively niche research and engineering field due to its high barrier to entry and cumbersome process. However, now that AI can assist in writing code and proofs, this methodology 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 warns that so-called "provable security" does not equal absolute security: proofs may omit key assumptions, the specifications themselves may be written incorrectly, and unverified code, hardware boundaries, and side-channel attacks can become new sources of risk. Nevertheless, it still offers a more reliable security paradigm: expressing the developer's intent in multiple ways and 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, post-quantum signatures, consensus algorithms, and high-performance EVM implementations. The implementation of these systems is extremely complex, but their core security goals can often be formalized relatively clearly. It is precisely in such scenarios that AI-assisted formal verification has the potential to deliver maximum value: let AI write efficient code and proofs, and let humans check whether the proven propositions truly correspond to their desired security goals.

From a broader perspective, this article is also Vitalik's response to cybersecurity in the AI era. Facing a stronger AI attacker, the answer is not to abandon open source, abandon smart contracts, or re-rely on a few centralized institutions, but to compress critical systems into a smaller, more verifiable, and more trustworthy "security core." AI will lead to a massive increase in sloppy 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 of this article.

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

If applied correctly, this approach has the potential to produce both extremely efficient code and code that is far more secure than past software development methods. Yoichi Hirai calls it "the final form of software development." This article attempts to explain the basic logic behind this methodology: what formal verification of software can do, and where its shortcomings and boundaries lie—both in the context of Ethereum and in the broader field of software development.

What is Formal Verification?

Formal verification refers to writing mathematical theorem proofs in a way that can be automatically checked by a machine.

To give a relatively simple but still interesting example, we can look at a basic theorem about the Fibonacci sequence: every third number is even, while the other two are odd.

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

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

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

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

This argument is convincing to humans. 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 could construct a proof that also convinces a computer.

It would look something 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 for good reason: what is intuitive for a computer is completely different from what is intuitive for a human. The "computer" here refers to the old sense of the word—a deterministic program consisting 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 aptly 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 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 one go and complete the argument with just a single line like omega or ring.

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

Verifying Computer Programs

At this point, you might think: Okay, so we can have computers verify proofs of mathematical theorems, allowing us to finally determine which crazy new findings about prime numbers are real and which are just errors hidden in hundred-page PDF papers. Maybe we could even figure out if Shinichi Mochizuki's proof of the ABC conjecture is correct! But besides satisfying curiosity, what practical use does this have?

There are many answers. For me, a very important one is verifying the correctness of computer programs, especially those involving cryptography or security. After all, a computer program is itself 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 a cryptographic communication software like Signal is truly secure. You can first write down mathematically what "secure" means in this context. In summary, you want to prove that, under certain cryptographic assumptions, only someone with the private key can learn any information about the content of the message. In reality, the truly important security properties are numerous.

And it turns out there is indeed a team trying to figure this out. One of the security theorems they proposed looks roughly like this:

Here is a summary of the theorem's meaning from Leanstral:

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, 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 an attacker who only passively observes Signal's key exchange messages cannot distinguish the final session key from a random key with more than a negligible probability.

If combined with a proof that the AES encryption is correctly implemented, you can get a proof that the encryption mechanism of the Signal protocol is secure against a passive attacker.

Similar verification projects already exist for proving secure implementations of TLS and other cryptographic components within browsers.

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

Of course, there are some very important asterisks here, especially regarding what the keyword "secure" actually means. It's easy to forget to prove the truly important claims; it's easy to encounter situations where the claim to be proven doesn't have a simpler description than the code itself; it's easy to inadvertently introduce assumptions that don't ultimately hold within the proofs. It's also easy to decide that only a certain part of the system truly needs formal verification, only to be hit by a critical vulnerability in another part, or even at the hardware level. Even Lean's own implementation could have bugs. But before we dive into these headache-inducing details, let's first explore the almost utopian prospect formal verification could offer if it could be ideally and correctly implemented.

Formal Verification for Security

Bugs in computer code are already concerning.

When you place cryptocurrency into immutable on-chain smart contracts, code bugs become even more terrifying. Because once the code is flawed, North Korean hackers can automatically drain all your money with almost no recourse.

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

When we have powerful AI models, code bugs become even more frightening. Models like Claude Mythos, after another two years of improvement, might be able to automate the discovery of these vulnerabilities.

Facing this reality, some have begun to argue for abandoning the fundamental idea of smart contracts, or even suggest 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 the attacker spends on exploiting them.

And another:

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

Worse, some believe the only solution is to abandon open source.

This would be a grim future for cybersecurity. Especially for those who care about internet decentralization and freedom, it would be an exceptionally grim future. The whole cypherpunk spirit is fundamentally built on the idea that on the internet, the defender has the advantage. Building a digital "castle"—whether manifested as encryption, signatures, or proofs—is 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: either dominate everything or face destruction.

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

I believe 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, we will arrive at a state more favorable to defenders than in the past.

Mozilla agrees. To quote them:

You may need to reprioritize all other tasks and commit to this effort in a sustained and focused way. But there is light at the end of the tunnel. We are incredibly proud to see how the team rose to this challenge, and others will too. Our work is not done, but we have passed an inflection point and are starting to see a better future that goes far beyond just "keeping up." Defenders finally have a chance to achieve a decisive victory.

…

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

Now, if you Ctrl+F search Mozilla's article for "formal" and "verification," you won't find either word. A positive future for cybersecurity does not strictly depend on formal verification, nor on any other single technology.

What does it depend on? Basically, the following picture:

Over the past few decades, many technologies have driven the trend of "declining bug counts":

Type systems;

Memory-safe languages;

Software architecture improvements, including sandboxing, permission mechanisms, and more generally, the clear separation of the "trusted computing base" from "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 was already moving forward.

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

STARKs are a very complex piece of software. However, the core security property they achieve is easy to understand and easy to formalize: if you see a proof pointing to hash H of program P, input x, and output y, then either the hash algorithm used by the STARK is 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 formally verifying various cryptographic protocols, many of which are themselves dependencies of STARKs.

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

Theoretically, a scenario could still arise where we have ten EVM implementations, all proven equivalent to each other, yet all share the same fatal flaw that somehow allows an attacker to drain all ETH from an address they don't control. However, the probability of this happening is much lower than one EVM implementation having such a flaw in isolation today. Another security property we only truly appreciated after painful experience—resistance to DoS attacks—is relatively easy to specify formally.

Two other important directions are:

Byzantine fault-tolerant consensus. In this area, 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 is ongoing work on Lean consensus implementations and their proofs.

Smart contract programming languages. Relevant examples include formal verification work in Vyper and Verity.

In all these cases, a huge incremental value brought by formal verification is that these proofs are truly end-to-end. Many of the most insidious bugs are interaction bugs, occurring at the boundaries between two subsystems considered in isolation. 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 revisit evm-asm. It's an EVM implementation.

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

Literally assembly.

Here's the ADD opcode:

The reason for choosing RISC-V is that ZK-EVM provers currently being built typically work by proving RISC-V and compiling the Ethereum client to RISC-V. Therefore, if you write an EVM implementation directly in RISC-V, it should theoretically be the fastest implementation you can get. RISC-V can also be simulated very efficiently on regular computers, and RISC-V laptops already exist. Of course, to be truly end-to-end, you must also formally verify the RISC-V implementation itself, or the pro