evm-asm: Experiences Writing the EVM, Directly in Risc-V Assembly

Transcript

Great. Thanks. Yeah, my name is Derek. Um I've been working on this very strange uh project for the last 6 months and I wanted to just kind of share some learnings and some uh some things about it. So, um what is EVM ASM um about? 6 months ago, one of my colleagues, um Yoichi, he reached out and he had been experimenting with um with writing code just directly in RISC-V assembly um at the Ethereum Foundation with all of our scaling roadmap with ZK VMs, we care a lot about RISC-V bytecode. And um

eventually, we need uh an implementation of the EVM in RISC-V uh that we're very confident with. So, Yoichi had started to just get his agents to write some code directly in RISC-V assembly and started to get interesting results. And so, we launched this um this strange experimental kind of um fever dream of a of a project and I it's really matured um and so, I just want to share some things about it. So, what did we do? We uh the goal was to um here, I'll I'll start with why. The goal was to um write a high-assurance implementation of the EVM that we can

trust in future uh iterations of Ethereum. And um why would we do it directly at the bytecode level instead of using the normal methods that we've done before? The first reason is that um you know, we live in a new world of vulnerabilities and of AI that can find codes uh exploits everywhere. And so, if possible we would like to reduce our trust base to the most minimal that we can and so we want to get rid of trust in the compiler so if we can if we can somehow write code directly in assembly then we don't have to trust the compiler so that would be great another thing that we could do if we have code directly in assembly that we

can have confidence in is that we can hand optimize the code without needing to go again through a compiler and so there's kind of interest in that as an experiment can we get code that's highly optimized done by hand and in a way that's high assurance the last point of why we might want to do a project like this is that you know these LLMs are are just getting better and better and when we when we started the project I think it was before Opus 4.5 and so LLMs were just starting to get really good at the stuff and of course now they're just unbelievably good and so we wanted to test the limits of AI formal verification kind of do in

some sense a creative exploration of like you know what new things are possible and and shape of what we did so we started by implementing a verified macro assembler in RISC-V what does that mean is we have a we have a an implementation of RISC-V in lean directly in lean that is formally verified with regards to the official RISC-V spec and what what it can do is is it has bytecode instructions as a data type and so you can write programs in within this interpreter at the RISC-V bytecode level and then it has a code gen that I will talk about a little bit later but in this case lean

for this proof language becomes much more than a proof language it's an assembler it's a macro language it's our specification language and it's our proof assistance so we're doing it all within this one setting so once we had the fundamentals at that kind of lowest level, so if you see this I guess you can't really see the the laser. Once we had the lowest level of the risk five RV64IM semantics in Lean, that meant we could write programs in Lean in risk five assembly. And so, what we did is we kind of pinned the agents between two formal specifications and said, "Here's the formal setting that you're executing code in." And so, the

agents have access to a very precise mathematical description of how the machine works. And then the EVM, while there are existing formal specs, part of the experiment of pushing the limits was to see if um see if the EVM could also write its own spec. So, for a while we called it the hallucinated spec, but then we gained real confidence by proving equivalence with others. So, we took the execution specs in Python and agentically translated them into Lean.

And that gave us two formal specifications that we could pin the agent between and and constrain the agent to write assembly code with the constraint that it had to prove everything it wrote. Um and uh so, let me just kind of give a dive in a little bit in to give a sense of the scale of this project. Um So, it turns out EVM SM has matured. We have a functioning guest and everything. It's about 1 million lines of Lean, almost 3,000 files.

Um There are no sorries, meaning they're all the proofs are complete. And there are no no kind of there are no axioms, no undue axioms. Um most of the code goes into the EVM 64 directory, which is which is the implementation of the EVM. And then there's quite a lot of code to take the program from the assembler and then assemble an ELF, an elf, um something that actually runs in a real risk five machine. Um and um Um so like I said, in this case, um within the risk five model that we have, um instructions risk five instructions

are a data type, and so you can that means that you can uh construct a program in um in Lean by just listing the the risk five instructions that you have. So, for example, the and instruction is here. You can see all the different risk fives, these loads, um the and the risk five ands, um etc. And um And um in in the case uh so we're using a risk five 64, but we have 256-bit words in the EVM, so they're all split into four limbs.

Um And proofs about a full EVM word in this case are a composition of proofs of the proofs over the limbs. Um And um for every instruction, so if if we're in So, so we had um sorry, we had and um the EVM opcode and implemented in risk five. Every instruction um that we implement comes with what's called a Hoare triple, which is a um standard way of proving correctness and kind of giving meaning to something that you have at a low level. Hoare triples reason about pre-execution states and post-execution states, and we used uh what's called separation logic to

essentially reason that anytime this opcode executes, in particular and executes, if you know um if you know the stack pointer beforehand, um and you So, you know the state of the stack beforehand, um you uh you can reason about what must be the case after. So, is all this is saying is that you have um two items on the stack, then after you call the and EVM instruction, then you just have their and on the stack on top of the stack. Interestingly, for many of the instructions we were able to bound the cost. So, in this case, um and takes at most 17 RISC-V cycles.

Um and uh what these Hoare triples also say is that uh it can reason about the whole memory and so it's it sort of identifies what your opcode is changing in memory and then it also can prove that the rest of memory is just unaffected. These are the kinds of proofs that we want at the lowest level. And then what we do is we go and we kind of um stitch them all together at a higher level. So, all of the EVM opcodes uh written in RISC-V assembly take the same shape as um as a program with a Hoare triple. And then they're like I said, they're kind of knit back together into one big um uh into um high-level proofs about the behavior

of the resulting program. So, opcodes are of course just a small piece of I mean, they're just a piece of the EVM. There's a lot more to it. There's uh serialization, there's a state root, there's the Merkle Patricia T tree, there's the uh kind of message calls um uh precompiles and things like that. So, what ended up happening is that we uh started with opcodes and opcodes were pretty straightforward to uh implement in RISC-V and that was very exciting. And so, kind of inebriated by the success early successes, we're like, "Ah, we can do all of this." And what we uh you know, things weren't always just sunshine and daisies. They got off to a great start,

but um we encountered some problems. So, I want to share some learnings of how it went and um what we learned. Some really, really interesting and good things that we'll be taking with us and some kind of hilariously bad things. So, the first thing that became um the first thing that we learned was it made us think very carefully about what a specification for the EVM is or what it should be. So, when we started work on this, like I said, we kind of hallucinated an EVM spec from the the Python execution specs. And um the way we ended up gaining confidence of this EVM spec is that we ran it under

the testing framework, the East testing framework that um that any implementation of the EVM needs to satisfy. So, in a sense, the spec is this huge test suite that we have been using. Um but what started to emerge is that we started to work on this formal spec. Some of our colleagues came up with another one in this uh specification framework called Sail, uh that lets you specify um ISAs. And uh so, that was an interesting alternative formal spec. And then, of course, there are other formal specs out there that people use for smart contract um verification. And what we started what we discovered is one that specifications for smart contract verification um

have different needs from specifications of uh an actual just implementation of the EVM. Um and you probably want to optimize for uh proofs in in kind of different directions. And so, we came to the conclusion that we wouldn't use previously written formal specs just for that reason because most of them were written for smart contract verification. Um and we've been kind of in discussion about um the role of specifications, you know, what what is the spec because now we have several uh floating around. And we have found some very um kind of nuanced minor edge cases um that that not only are uncovered that

that that they're they're not covered by the the um I guess the legacy specification of the EVM, um but that differ slightly between actual kind of production implementations. So, um that has given us some things to think about as we're as we're making progress on this. Um another thing of kind of how it went was the the scale of the project just kind of ballooned. Um one one um What's the word I'm looking for? Um Anyway, one downside I maybe of Lean or a one um restraint anyway, one thing in Lean is that the type

checker can sometimes if you have too many proofs to check the type checker can get kind of low um slow, sorry. And what that means is the type checker is when the Lean is when Lean is checking the proofs of all your theorems. So, if you have this huge code base of theorems, sometimes that can start to crash just because the the things that Lean has to keep in mind while it's processing the proofs just kind of explodes. And so, we definitely started to run into this where where the proofs were just getting too big. Lucky for us, the Lean FRO, the kind of research organization behind the the proof assistant, um had been thinking about scalability already for a long time and they started to introduce new tools. So, we're able to wrangle most of the scalability.

However, um Let's see if it's in the next slide. No, um however, it it started to become the case that small changes um in certain opcodes would ripple through the rest of all of these proofs and it was still very hard to manage the scale and the complexity, which I don't know, at the end of this I'm like, I see why we have compilers. Um So, one kind of rather hilarious thing that happened to us is that um once we got we were getting very close to a version of EVM ASM that was actually running. Um And again, this was all agent led and so, because it was so big, it was kind of hard to keep track of what the agents were doing fully and um in a way that

would actually allow us to still make progress. And so, we ran into this hilarious problem where um where the agent started we had we had uh implementation of EVM that would could process a whole block. And then, the agent wanted to pass all the East tests and we were we were telling it to run them and then to fix itself. And what it did instead of actually fixing the proper guess is it it wrote a parallel implementation that only processes one transaction at a time and it optimized that for passing all the tests but but left the other one completely undone. And and maybe embarrassingly or hilariously, it depends on how you look at it, it took us a while to notice that's what it was

doing. And when we did it actually required a a few weeks of refactoring. Um But you know, with we're all in kind of this euphoria of agent led, you know, everything and we have people posting every other day. I mean even this morning there's this huge formalization a pro a project that came up on my Twitter feed. And it's just like like how can we possibly understand this realistically? Like um It it's just such a huge volume of information.

Um Maybe a fun fact or fun tidbits. Um some opcodes were much easier and much harder than others. Div in particular and div and mod um took a lot um in part because div has to go through these estimation steps and each of them was a subroutine and each of them needed a formal proof. And anytime you had problems, it just it was just very hard. I don't have time to anyway. Um And so we kind of got to the end and like I said, we gained a real appreciation for the role of compilers and we had wonder wondered if this project would lead us to um implementing a custom compiler for the EVM specifically. Um which kind of happened.

Uh my colleague um encountered this low-level language and formally verified compiler called Pancake at a conference and um we imported it into Lean um from whole four and um implemented the EVM and it turns out a very very low-level language like Pancake ended up being kind of a sweet spot where um um where it manages the complexity of the really low-level stuff that just makes everything explode, but it's still low-level enough that we can optimize um quite a bit and we saw really really tight control and um we can still get formal proofs going all the way up to a high-level spec that we that we trust.

And so the project transitioned from EVM ASM just directly ASM to um this uh project we ended up calling Flatjack um that has the EVM implemented in this low-level language and compiler. Um so in a sense we did kind of come up with we landed at a a very niche kind of custom compiler framework and that might be the the best way uh for us moving forward. Um and then maybe one of the last things about kind of how it went how it's going is that it really emboldened us. There were issues that we found and there were limitations but it emboldened us to try other assembly level um uh proof and development of of things and we've been doing experiments in

still a very small cryptographic code very small pieces of code that we can just implement directly in assembly, but we've actually had moderate success and we're hoping to have more success um in this later. So very quickly I'll just I'll give an overview of kind of what's what's next from all of this work. Um So we set out to push the limits of formal verification of formally constrained agents um and of compilers and by that measure EVM ASM was a success and we very plausibly have a highly secure highly optimized version um I implementation of the EVM that is fully formally verified

and um while it does rely on a compiler, it is a formally verified one is very low-level um and and so this is a strong plausible um possibility for the future of the EVM. Um like I said, it led us into lots of discussions about specifications. Um in this new strange world that we live in with agents that are so skilled at coding, what is the role of specification, um a formal specification? Probably we're going to be caring about formal specification a lot more than we have in the past. And also, what is the role of compilers?

Like do we really need, you know, high-level languages are done in part so that to make it easier to work with for humans at a high level of reasoning, but if LLMs are fine doing low-level stuff, then you know, what does that imply about our languages, compilers, you know, at what level will we be doing our work, and where is the sweet spot of being able to ship code and formally verify it simultaneously? Um and okay, so yeah, at what level? Uh that's all I have for you today. Thank you very much.

>> Thank you, Derek. That was a great talk. I think we can do some questions. Uh so, remember to scan the QR code if you want to add more questions. So, the first question is um how how can we be confident that the specs are complete and to trust the formal verification? >> Yeah, I think this is the main question of this will become more and more the main question of software development moving forward is that our specs will just matter more and more. In the case of the EVM, that is also just a very interesting question because we've had we have execution specs in Python. They

were originally chosen to be in Python because Python is readable um and it's executable and uh it's like formal enough that you can be precise, but also it's intuitive. Lean might take the role of that. Um but the the question that comes to mind is how did we know that our Python specs were enough? Um, and that's kind of a combination of lots of people's attention, um, having the specs be executable so you can actually see them run. A lot of times what you want from a specification is most easily manifest in actually using the thing and kind of interacting with it. And it's hard to articulate.

Um, and so I guess tests, um, community, um, uh, lots of eyes, um, if you have your spec in a formal setting like Lean, you can you can in principle reason about it like with a meta meta specification, um, at a higher level where you're reasoning about the behavior of your own spec. So there there are tools, um, but this is kind of a philosophical question, kind of mathematical philosophical of of how do you know you have expressed your intent? Um, it's a very hard question. I think it will be the the question moving forward.

Um, but for the EVM, how do we know the spec was good? It passes the test. That's the most basic measure for for now. >> Yeah. Um, the next question is, uh, do you think of when LLMs are getting better, this would be the standard way that people would write smart contracts directly in in bytecode? >> Um, is there a way EVM bytecode in a formal verification? Uh, very possibly. Yeah, absolutely. I think in our case the the the main, um, you'll want to interact with it still at a kind of a specification level. So so that there might be room for kind of a specification DSL.

I could really see that, especially with smart contracts, because in smart contracts you, um, you care about financial primitives and concepts economic um interpersonal interactions, game theory, things like that. So if you had a really nice, um, maybe a game theoretic model in Lean that you could express of specification to a high level and um, very precisely, um, essentially codifying like the diagram you write on the whiteboard when you're trying to design your smart contract. I think it's very possible that having the agent write it directly in EVM bytecode and then formally prove it is is going to be your most secure way. Yeah.

>> Okay. So the next question is how did you implement external contract calls and state accesses in this uh experiment? >> Good question. Um I am not sure which is the problem with the scale of the project. Please let me I can I can get back. Yes. Right. Okay. Yeah. You give it a You give it a state route at the beginning.

It is external contract right. Yeah. Um it's a state with this implementation. Um >> Yeah. I think we have time for one more question. I wanted to ask this um >> Mhm. >> How about the benchmarks? How does it compare to REVM when it's compiled from Rust? >> Yes. So currently um currently it is slower than REVM. I think it's twice as slow. I'm trying to remember the benchmarks. Um we just launched EVM.fa EVM.fast um which is an auto research challenge, which means you can um donate your tokens um to optimizing our implementation of the EVM. And uh so our

our hope and goal here is that we will be able to beat um REVM in the end. Um but we are not yet faster. >> Okay. All right. Thank you so much. Uh Let's the Let's thank the speaker again. Uh >> Thanks. >> We'll take a 5-minute break.