A Yellow Paper you can run: an independent executable EVM spec in Lean 4

Transcript

[music] [music] >> Thank you. Okay, let's start. So, hello. I'm Sergi, and today I'll present to you Zone, an executable specification of the EVM written in Lean 4. So, for those of you of you who are wondering, the name Zone means yellow in French, and as you may have guessed, it is inspired by the yellow paper, which once served as Ethereum's official specification.

So, now when someone says a new EVM specification, your first reaction might be why? We've got plenty already. EELS, the reference specification is written in Python, so we've already got executability covered, and the diverse execution clients also effectively serve as a distributed spec. So, why bother with another? Two reasons. The first practical reason is that writing a second implementation is one of the best ways to spot mistakes in the first.

To build Zone, we had to run the reference's test fixtures and match its output field by field, and that probes the reference in ways that are very different from how clients usually interact with it. So, for the first part of the talk, I'll tell you two stories about errors that turned up and all of which are now fixed upstream. And the second reason is Lean. Uh by now, everyone knows what Lean is, but if you haven't been following, Lean is a programming language that doubles as a theorem prover, which allows you state and prove theorems about the very code that you also compile and run.

And that's how it also ties back to the yellow paper inspiration. It's about facilitating the abstract mathematical reasoning about the EVM that the original yellow paper was characterized by. So this capacity for proofs makes a number of interesting and useful things possible, which I'll show you after the two stories. And you're not going to need to read any lean code to follow along. Also, speaking of AI, almost every result I discussed in this talk was accomplished with extensive AI use, including the formal lean proofs. So when I say we, that means me in collaboration with the AI agents.

First story. The older version of Zone's fixture runner accepted any rejection of an invalid block as correct. And under this version, everything passed. Then the fixture runner was tightened to require reporting of the exact reason for rejection that matches the fixture's expectation, which turned up new divergences. Most of them turned out to be harmless, such as transactions invalid for multiple reasons would where the reported reason varied depending on the order of checks performed.

One of them, however, was a real semantic error. A beacon chain withdrawal carries a mountain way, and EIP 4895 types it as a 64-bit unsigned integer. But Eels modeled it as a 256-bit integer, and so did Zone, whose older core was rebuilt on Eels. So for the fixture with an oversized amount, both decoded it without complaining and rejected the block only when the state root failed to match instead of reporting the expected decoding error.

So we we corrected this error in zone and sent the same fixed upstream as PR 3186 which was merged on August 5th. So in this case, the fixture that reveals the problem had already existed and EELS own test harness even carried a to-do comment saying that exact exceptions should be checked for. So the check was simply too weak to expose the mistake and the second ex a specification turned out to be a good reason to make it stricter.

Second story. TATN the short for transition tool is the interface that Ethereum's test framework uses to run transactions through an EVM implementation and also to generate test fixtures. You take a tool that supports TATN and give it an allocation of accounts and environment and a list of transactions. Then it turn runs them under a chosen fork and gives back the post state, the receipts, and which transactions it rejected, the roots, and the encoded transaction list.

And several tools support it. The reference EELS clients like Geth and Besu and also zone. So here's one tiny TATN case. Three transactions, all from one account starting at non-zero. The first is a legacy transaction with non-zero accepted. The second has nonce nine rejected and nonce too high. And the third is a type two transaction with nonce one also accepted.

The expected behavior for this case is that the invalid middle transaction is dropped. The remaining transactions are treated like a transaction in a single block and the tool returns the result of running that block. But look at what EELS returned. Its transaction try still contains the dropped transaction. And the transaction listed returns not only retains the dropped transaction, but also double encodes the legacy transactions. And its receipt try drops it, but the keys are zero and two. One is missing.

That's a gap that no real block can have. And Geth, on the other hand, exhibits none of these errors. The reason for the try errors is simple. To know whether a transaction should be dropped, you need to process it first. But EELS's transaction processing function has no notion of waiting to see if a transaction is actually valid. Whatever transaction it receives, it immediately writes to the transaction try. And the receipts, even after the rejection, keeps the places in the input, those indices.

Now for block processing, which is the main purpose of EELS, this is fine because any invalid transaction makes whole block invalid, which makes the correctness of the tries and lists a moot point. But reuse that transaction function for T8N without modification, and you get exactly these errors. The list error is a separate slip. T8N writes it straight from its input. Every transaction it was given and and wraps each one as a byte string, which is correct for type transactions, but wrong for the legacy ones.

So it looks pretty simple. Why were these errors not found earlier? Again, it has to do with the way the reference specification is used. The main path that exercises EELS's T8N interface is Fill, the tool for filling test fixtures. But Fill discards both the transaction root and the transaction list that T8N returns. So nothing in parts of the output reaches the fixtures. Also, until a recent October update, Phil disallowed invalid transactions occurring anywhere other than the end of the input list, which precluded gaps in the receipt try like what you've just

seen. So until recently, the main use case of T8N was by construction blind to every error we just discussed. But when implementing T8N for Zone, we had to test T8N itself rather than [snorts] just fill with it directly against EELS and GETH with handwritten cases outside Phil's rules, including the one we we just saw. So Zone replicates EELS as T8N by design. So the three-way run run confirmed it on these cases. EELS and Zone agreed and GETH diverged.

So all of this is fixed now. We reported the roots problem and Elog 108 fixed it. T8N now numbers only the transactions it accepts and leaves the rejected ones out of the list. The double encoding was our pull request and F Salmo turned it into a check across forks and transaction types. Both landed on the 21st of October. A day later, we updated Zone to with the corrected rule and today it matches the fixed reference EELS on all 76 cases of its own T8N test suite, Phil for Phil.

And now the second reason for writing a new specification, namely proving theorems. Having a model of the EVM in Ethereum Prover that you can run and reason about is not new at all. It goes back at least to Yoichi Hirai's 2017 work which formalized the spurious dragon version of the EVM in Isabelle Hall four and and also supported extraction to camel.

What is rarer, though again not unique, is a model in Ethereum prover that runs the whole of today's blockchain test suite, including block processing. Zone passes every blockchain test in the official fixture release test version 21.0.1 for forks from Byzantium to BPO two, all 73,345 cases with zero expected failures. And it also runs fast. All of them run in about 12 minutes on a Zen three desktop. So fixture run is a coffee break and it's not a ceremony that you have to schedule for.

This identity of the artifact, I would argue is key for making rigorous formal verification also practical. It lets you verify contract properties against the very definitions that you tested against Ethereum's fixtures and not just an abstract model whose fidelity that you have to take on faith. So here's an example of the kind of formal verification you can do with zone.

The target is with nine the Hello World of EVM formal verification. It holds ether against token balances and a holder cares about two things that those balances stay backed and that they can get their ether out. We prove both under explicit conditions. To see what a claim like that is worth, I like to ask seven questions of any a contract proof. So let's go through them one by one for West nine. Question one.

Is it about the bytecode that actually runs on the EVM as opposed to an abstract model of the contract or a high-level source code. And the answer is yes. It's the exact 3,124 deployed bytes at Weth 9's main net address as read from the chain. And for those of you who are curious how we deal with the raw bytecode, the key is finding a certificate that says the bytecode's control flow is well behaved, such as a function calls always returning to that call site. Once a certificate is found and the checker confirms it is valid for the bytecode, then you can write your proofs against a higher level representation that is much easier to work with than a raw sequence

of opcodes. And what you prove about it still carries back to the bytes. The checker does not care about how you found that certificate, so we can use just a we can just use a Python program for it. Question two. What does the proof rest on? What does it ask you to trust? For Weth 9, it's just Lean's kernel plus the three standard axioms. Nothing else is admitted. No axioms like global injectivity, no sorry, no native decide, no FFI, no definitions, nothing.

Question three. Was the code specifically designed and generated to be verification friendly? This question matters not for validity, but for reach. There is nothing wrong per se about a purpose-built bytecode that lends itself well to verification. But if a verification method requires a purpose-built bytecode, then by definition that method cannot reach the existing highest value contracts that we care most about.

And that includes the Weth 9 contract in question. So the answer is no. The bytecode is Solc 0.4.19 produced in December 2017 ordinary compiler output never meant to be verified. Question four. Is the machine the real EVM with nothing simplified or abstracted away? And you've already seen the evidence for this one. All seven 73,345 blockchain test cases pass and also building zone found real errors in the reference.

That's still not a proof, but it's reasonably robust evidence that the machine is the real one. Question five. Does the theorem matter? Does it prove a practical property that is desired and expected of the contract such that users and developers would care about its proof? For Weth9 we prove the two properties that every holder relies on. And first backing add up all the Weth balances of every holder that appears in its history and the total never exceeds the ether that the contract actually holds. So every Weth is backed by real ether.

Second, exact withdrawal. When you withdraw an amount your Weth balance goes down by exactly that amount. The contract's ether goes down by exactly that amount and you receive exactly that ether minus only the gas [snorts] you pay. Question six. Does it say the contract works? A lot of formal verification guarantees are partial. If with it says if a withdrawal succeeds then it has property X, but that still holds of a contract on which every withdrawal fails all the time. So we prove the total version.

A withdrawal meeting a set of explicit conditions succeeds after spending an exact amount of gas in closed form. We we also did a check on mainnet and 3,748 total withdrawals of that shape each used exactly that amount of predicted gas. Question seven. It asked something different, not what the proof rests on, [snorts] but which facts must hold on mainnet for it to actually apply.

Do they hold today? A proof whose premises that no user can check helps nobody using the live contract, however however watertight it might be. That is why zones with nine results have parsimonious premises. One particularly minimal example is the backing theorem, which requires only two premises beyond the assumption that zone is the real EVM. First, that the December 2017 block in which was nine was created has a certain hash.

And it's a one public fact you can check about check against any node or block explorer. And second, that there are no collisions among the specific values compared in the proof from that block until now. It's a precisely limited condition, not a global and everything else the theorem needs follows from those two, the creation transaction itself, the correct code installation, and the initial storage state. With nine is just one example from Blanc, the verification stack built on the zone.

And Blanc already has a fairly extensive corpus. It includes 11 deployed artifacts, among them non-trivial ones like Lido circuit breaker, plus compositions like a Uniswap V2 pair contract with with nine and USDC. These contracts were written in Solidity, in Viper, and one in handwritten assembly. So this verification method is not tied to one language. And they also span nine compiler versions deployed from 2017 to this year. So it holds up to a version churn.

The same seven questions we explored for Weth9 are posed for each one of these artifacts, and each result goes a considerable way to answering them, though not all of them equally far yet. For instance, nothing yet proves that Lido circuit breakers calls succeed, and not all of them derive their premises from their historical deployment like a Weth nine does. Those gaps are the work still in progress, and you can refer to the public claim map to see exactly how far its contract gets.

Let me be exact about what all of this does and does not establish. Conformance cases establish agreement on the inputs and outputs they check. They are finite evidence, and they do not establish equivalence with Ethereum on every single input. A kernel checked theorem established that its conclusion follows from the definitions of the premises, definition and the premises, but it does not establish that the statement is the one you actually meant, or more importantly, the one that it should be.

And in my view, this is the hardest open problem in AI assisted formal verification because meaning exists outside of formal systems, and bridging that last mile is not something that machines can do for you. Um AI can still help. You can ask it for more explanation or a more streamlined statement that that is easier to parse, but understanding what a statement means and satisfying yourself that it is a right one is something that you still have to do yourself.

So those are the limits today, and let me close with what comes next and what each step would let you do. First testing. Zone speaks T A N and is checked field for field against the reference, but the test frameworks still cannot call it yet without a local patch. And I plan to make it a transition tool that Phil can call directly and then you can and then if you write tests, you could fill or cross check your fixtures with a second independent tool. Second Amsterdam.

Zone already runs the Amsterdam fixtures of the fixture release we use, and I plan to follow the fork all the way to main net each new fixture release and also the parameters once they are final. Then if you are implementing Amsterdam in a client, you could check your behavior against the second executable spec of the fork. And finally, proofs. As we've already discussed, there are still gaps in how well each contract answers the seven questions, and I plan to close those gaps.

And for instance, every contract will follow with nine's model of deriving as many of its premises as possible from its historical deployment so that those premises can be discharged by checking a single public blocked hash. And that's it for the talk. Thank you. >> [applause] >> Great talk. As I mentioned, right, if you have any questions, just scan the QR code and ask any questions you want. Circuit is a great presentation. So let's pick up the questions. So the first one I like what surprised you most when you compare like sort of your own

specification with the existing tools? >> As in negative surprise in the earlier stage, I was surprised by how horribly slow it was because I was trying to make it run out of compiled lean. And when I was running the legacy fixture set, which is actually smaller than the one I'm running now, I used I I used to put my laptop on for a whole night because it'll take more than like 30 hours to go through all of it. And uh it's only after I started using uh the agent help that they massively optimized the thing and then now I can do it in like 10 minutes. But yeah, that those were the things that you know or the the snags in the earlier part of the the development and I think.

>> Um so the second question I uh we have so many uh clients from uh Ethereum, right? Either Ethereum Foundation or like sort of the community. Um so what's the sort of the practical way for this Ethereum client team to start to use your tool today? >> So if you want to for if you want if you have a contract and a property that you want to verify with Zone and Blong the verification stack, I would say just go go YOLO. Go go just get fork and clone the repo. And there is actually a third repo called uh Crem, which is a AI um AI augmentation stack. It has all the files

and how the AI should interact and how what kind of definitions it should use, what tools will suggest the right tactics for you. And once you have that all those three repos and just tell your tell your agent your favorite agent to just implement this in Blong and give me the property. And I think you'll be surprised by how well they just take the the entire task end to end. I mean that's how I do it now and I don't really I don't ever look at low-level code anymore until unless it's absolutely necessary. Yeah. >> Um anyone have more questions?

Uh actually I have one because like in your presentation you mention um the um the WEE9 example, right? Do you have more similar examples you can share a little bit more on? >> Oh you mean like more contracts or yes. I mean I there is an actually archive paper that I published a few weeks ago and it covers all the artifacts that that has been verified on so far. And it's a little bit dated because I've been doing more work since then, but it's still the most complete coverage that you will get of the results that I have now. So it it includes things like EIP 7002

I actually posted a one on E3 search about it as well. So you can refer to that for more information. And it has a Viper has Viper examples like the the one behind the 2023 hack, the Viper bug. So those are interesting stuff and you can look it up and it has the paper has more details on it. >> Um actually I also have a follow-up question. So we have a lot of features upcoming for the for the Ethereum hard fork, right?

So how long do you think if we apply this form verification on your tools on really like sort of verifying all of them? >> So which one should which one what what are you talking >> you mentioned about this Amsterdam, yeah. >> How how long is it going to take for the Amsterdam thing? I think it's mostly done. It's like it's it already passes the the fixtures in the fixture release that I'm using and it's still waiting for parameters and whatever changes that still might come from upstream. But I think it'll only take a couple days.

That's that's an optimistic estimate, but once Amsterdam is finalized, you will get a version working version of Zone with it and also that supports it for contract verification. And I think that's it. >> [music]