ZK-EVM, Optional Proofs & Lean Execution: Scaling Ethereum with Zero Knowledge

Transcript

Introduction & slides overview

Thank you uh everyone for being here. Yeah, I'm Cody Gunton. I'm on the uh ZKVM team at the Ethereum Foundation. Um these are this is a link to my slides and this is a QR to my slides. There are some links in there that you might want to follow up on. So feel free to uh pull that down now if you're interested. Yeah. Seeing some action. Okay, cool. Um yeah, so I originally was going to talk about something a little more narrow, but then I thought it's good to give more of an overview of the the project. Um, so we'll get to the question of specifications at the end and some progress I have there. But let's just start with what it is that we're doing

ZK-VM asymmetry: low-power verifiers vs powerful provers

and how we're going to do it. Um, so I like this frame for what ZK uh VMs do, which is that they let us leverage this um a certain asymmetry where you can have a network of very low power nodes checking the work of a bunch of very powerful nodes in that network and they can do so with a small amount of data. Okay. And so our application of course is Ethereum. We're interested in uh applying this paradigm to uh allow a testers to stay lowowered while allowing at the same time the network to scale.

Okay. So a priori if you just did the normal thing what you do is you re-execute all of the transactions at every block. And um then if the number of transactions grows then the requirements to do so also grow right you need more data and you need more compute to do that. But what we'll do is we'll have the attesters run verifiers for these ZK proofs and then we'll have the proofs be produced by these powerful entities um who are you know kept in check by the attesttors and they're only going to need a small amount of data to do that work.

What a virtual machine actually is

So here's just a picture of what a virtual machine does. It's a silly picture maybe but I don't know pictures are nice. So it's just an implementation of a computer in software. Yeah. like you just write down the rules of a computer in your favorite programming language and then you can say what that computer would do. You know, if you actually built a machine that did it, that's a virtual machine. So the program runs inside, you have a physical machine with a virtual machine inside of it and you know, it can receive inputs and churn outputs according to how a real computer would do. And the kind of extension of this diagram to the paradigm of ZKVMs would be like this. I actually don't know if Oh, sorry. Can you see? Great. You can see my mouse. So it would look like uh I'm going to try

to talk into the microphone more. Sorry. Um so yeah, we still have a virtual machine which is this gray box, but it's running inside of another environment in the computer which would be the ZKVM prover which sort of observes what the virtual machine is doing. But you know this bit of it's the same. We have inputs program outputs in a virtual machine. It's just that the prover kind of watches what's happening and puts out a proof, right? And then to check that work, you take all of the inputs and outputs and you shove them into a verifier and it makes a decision about whether the outputs actually came from the inputs based on the proof. And this is what the work of checking looks like.

Adding a ZK prover around a VM

So um it's slightly different. The the in and the out may be different here. Um you'll see on the next slide what I'm talking about. So specializing it even more to our situation, we're going to have a ZKVM prover. the the virtual machines that are running inside of the prover um could be other things but they tend to be risk five virtual machines right 5 is a uh an instruction set it's an open- source instruction set that uh is um I think growing in popularity and over the next 10 years we'll see more and more in real computers um already you can buy risk 5 laptops but that's a it's an open standard um and we like that sort of thing and it seems to work quite well so then inside of that is yet another

RISC-V + EVM inside a ZK-VM

virtual machine, the Ethereum virtual machine. That's now the program. If we look back at this diagram here, right, this program right here, this is now a another virtual machine, the EVM, which we we know is uh the core engine of Ethereum. And so what we're going to do is we're going to have a prover observe the execution of the EVM inside of a risk 5 environment. And then it's going to transform the state of Ethereum um given a block. And it's going to do so with this add astation, which is a proof. Okay. And I mean there's nothing new in this in this here. You just take all of the inputs and outputs except that here you actually only need some um tree roots. You don't need the full state to do this verification. Um sort of the magic of hashing in Merkel trees

makes this possible. So this amount of data, it's just sort of a a shadow of these little gray boxes here. uh it's a small amount of data and you plug that in and then the verifier the atttor node can decide uh whether that was a valid state transition or not without having um very much in the way of computational resources and just to be clear I'm not talking about replacing the EVM with risk 5 that's a a sort of loosely related project you would do that so that this step here could be more efficient but it is not in any way required for what we're working on that would be a much larger scope um so Yeah. And that's part of what we call lean execution.

Merkle roots & small verification data

All right. So, yeah, ZK EVM, that's when you choose a ZKVM and you choose an EVM implementation. That pair is a ZK EVM. The E is for the Ethereum part. Yeah. And there are lots of candidates. So, these are some screen grabs from someh uh that Justin has given Justin Drake. So, here is a table he maintains very diligently, very detailed um table of of the ZKVMs that exist. He presented this at the event we had in Argentina in November and also now he's tracking guest programs. So any row in this table and any row in this table roughly speaking uh comprises a ZK EVM and so we have a very large design space even with stuff that's already built um to say nothing of you know optimizing each

What a zkEVM really means

component. So yeah um here are some links to the uh some YouTube playlists if you want to watch the ETH proofs calls or the um the talks that we gave in u in Argentina. All right. So, how will we ship this? Well, we're going to do it in two phases. The first one is called optional proofs. And that is because, well, it's a very big change. Um, and it's uh if we're not careful, which we are very careful, um, it's dangerous. So, we're going to launch it in an optional phase where we can get a lot of data, iron out bugs, see how the network performs, understand these provers very, very well. And um the downside, well it's not necessarily a downside, but this does not allow us to scale Ethereum because

it's optional, right? So if we did scale Ethereum with optional proofs, the nodes that do just only use the proofs would or sorry that um don't only use the proofs that do re-execution, they would not be able to keep up with the chain at some point and we would lose a big part of our economic security. So we're not going to do that. And then later on we can make these mandatory once we're very confident in how this works. And then we can start to increase the gas limit. Okay. So how will we ship? That is how it's in phases. We have an EIP for the optional proof phase AD25. And uh there's a link in my references. So this is this is kind of a skeleton last I looked. Um it's you know it's under construction, but there's a lot more in um the specs repos and I link to uh the

The Optional Proofs phase explained

most recent stuff there if you're curious. All right. So, who is shipping this? Here is a list of stakeholders. We have the ZKVM teams. We have existing core devs. We have some new guest programs, new core devs coming in uh to build like um something that's really ZK friendly. We have Justin Drake and the ETH proofs team. I'm sorry. Did somebody Oh, okay. Um we uh we have my team here, the ZKVM team. Um we have the snarkification team which is working on I mean a lot of stuff but for our context uh formal verification like very strong security um uh tools for for the for shipping this. Um we have the

Why Optional Proofs cannot scale gas yet

cryptography team which is looking at the theoretical side of the cryptography. Panda ops is going to build you know monitoring and build provers and and work on the infra side of it. We have the rig robust incentives group uh working on the proofer incentives and we have some grantees also um working on this and so here is a lot of the decisions are made um collectively on this uh git organization the ETH act applied cryptography team um and you'll see in here a planning repo there's also a link to that at the end and there's quite a lot actually there's yeah what is it here 25 repositories and there's a lot going on here and we have very robust discussions where a lot of people give their green check marks to

EIP-8025 & shipping plan

or don't if they they don't agree um to the uh to the initiatives that we propose. Um and we also just started this week just two days ago this breakout call um for the AD25 uh optional proofs EIP. Um so on that call I presented Oh, okay. Yeah, one more slide. Um, so here's what here's another screen grab from our planning repo that we have the plans broken down quite granularly into these projects. Each project has a group of many stakeholders, you know, more than a dozen people in some cases who are all uh responsible for um shipping this and making sure that it's it's correct and

Stakeholders & working groups

aligned and and it's a it's a very good upgrade for us. And so this is one way that the projects look. You can look here. You can even see the I I I took this screenshot last night and yesterday Kev, the lead of my team, um uh merged the our updates. So, we're giving monthly updates. The the pro somebody from each project will will merge an update to show progress on on the initiative. And I uh presented this on Wednesday. So, this is a security focused road map. And it's sort of temporal but in a not a very fuzzy way but kind of a fuzzy way because some of these things already have strict deadlines like this well not strict but I mean proposed you know we we make requests for things um there's no but they they have deadlines that

have been published um like this sound calc integration this and these proof um security and size initiatives those um requests uh those like um deadline requests from the security team or not the security side um who maybe I didn't mention the security team on that one slide but we have a team who are also working with us um of course but the cryptography team um has published a blog post asking for these by certain times um whereas some of these are a little fuzzier but we do have this target which is hegatas so the fork after the the current fork under um construction glamsterdam at that point we want to be ready to uh launch optional proofs we need to wait for hegata for this to be a reasonable thing to do because there will be repricings

Planning repo & roadmap overview

in hegata that will allow the provers to keep up with the chain um to get rid of some sort of pathological not really realistic use cases where proving is much harder than re-execution. So the prices are off for that. Um but yeah um a lot of what's on here is uh like for me the things that I work most closely on are the security of the ZKVMs and there are a lot of testing initiatives that are just you know tiny little specs in this diagram but there's there's a lot each of these bars is has a lot behind it. Um, and I just wanted to call that out because I really think about this security question very holistically and what I'll talk about next is rather specific and formal to do with specifications, but that's just really

Hegeta fork & repricing requirements

one piece of the puzzle here. All right, so that's sort of the end of my overview. Um, so now I want to just dig in a little bit to some of the uh specification initiatives and explain what it is that we need to do in terms of specifications and what progress we have now. um because I think that the yeah it's it's kind of a cool um initiative we have. So we need to know like what are we putting in in the protocol? ZK is a very interesting field. I I started doing ZK in 2021 and I mean the number of significant papers that have come out since then is is pretty dramatic. I'd say the pace of research is is slowed and the pace of it's become more of like an implementation focused discipline but

Why security is holistic

there's a ton that's happened and I mean the ZKVM teams have have been very impressive in terms of what they've built. They very good performance in these systems and something that you sacrifice when you move fast is some of the you know dotting your eyes and crossing tees in terms of writing everything down. I mean a specification usually you know in the ideal world comes first and then the implementation follows. In practice, this often is not how it works and and that's I think that's acceptable. Um, but what we need to know now is what's what's been built is the cryptographic protocol that's actually built by a ZKVM a real cryptographic protocol. Nobody has just built a ZKVM using this the papers. They took the Fry paper implemented that exactly and that's what's there. There are lots of optimizations at the

Specification challenges in ZK systems

protocol level and it's a sort of like ship of thesis. you changed this, you changed that. Somebody knew this was secure, somebody knew that was secure and they didn't write it down. And now what you have doesn't really that closely resemble what's in a paper unless you're an expert and you sit down and read it, which is what we need. So we need to write down what the proving systems actually are like that are what what were intended like to be implemented. Um and um yeah so that so we need to know that that that those proofing systems are then secure like we need security proofs like you would have in a paper for the thing that's actually uh was was intended to be implemented. Um and then we need to know that that thing was actually what was implemented. So you need to then read the code somehow and

Whitepapers & formalizing real implementations

make sure that that's what's there. Um and also if you're implementing risk five machine to emulate uh you know inside of your prover the um the EVM then you need to know that risk five was executed correctly uh or that you know you're you're actually doing a a real computer and not a computer that just returns true all the time or something. Um and uh yeah similarly for the EVM. So these are all things that need specifications. Um and let's talk a little bit about the steps and toward towards these specifications. So um we have a call this is a link to a blog post from the research team asking for white papers this year where they want um something like an academic paper describing the the proving systems and

not just the proving systems like in a narrow sense but in terms of how they use uh what are called continuations or recursion. and the sort of like macro proving system that composes a bunch of smaller pieces into something that um you know can run on a cluster of 16 GPUs can prove a bunch of chips can compress the proof to something we want to send to Ethereum and so on that is fast to verify there's a lot of it's a big composite system and we need to know exactly what that is um okay but so after we have that so the purpose of that is so that the research team can can read it and and others other independent researchers and can read this and understand what's there. And then next we have this cool initiative called arclib where we have the um

Arclib & machine-assisted proofs in Lean

formally verified uh zkvm uh initiative that is is building this uh the snarkification team is running that initiative and uh they are building this library that can allow you to write down these protocols that I just discussed in the white papers but using the formal programming language called lean which forces you to be you know very careful and als also opens up the possibility to taking the proofs that might be written down in these uh by these researchers and turning them into machine derived formal proofs where you use um software to argue that two statements that a statement is true like

Matching implementation to intention

that the the proving system in the uh in say some spec built up from arlib you know a spec for concretely say the openvm prover to know that that actually is a pound um proving system that's a precise statement um with with certain number of bits of security and you can actually have machines make that proof. They'll they'll take the statement and then reduce it to axioms that are checked eventually by people a small number of axioms in the in the language. Um okay so then um so what about whether the implementation matches the intentions? Well, okay, you can take the white paper and then read the code.

That's a good important thing to do. Um and then sort of so that's we we should do that and we'll do that but uh eventually you can do something similar to this formal check that I described for arlib proving that the sort of model protocol is correct. Now you can think about taking the implementation which maybe is in rust or C++ or CUDA and extracting that like making a lean a a piece of software that turns that into lean and then arguing that the lean is equivalent. Okay. And then what you well you have to trust the extractor but I don't know would you rather audit some kind of extractor thing or would you rather audit the proving system? I mean what it's it's an everything like we want as much security as we can and that

Formal verification of OpenVM & SP1

that seems like a powerful approach as well. Okay so then yeah what about the risk five? Well there's already a spec for that in this um formal description language called sale. Uh and actually I mean we have progress on that. So even this was only this week I think um the uh Nethermine security team has announced uh the formal verification of openVM and they'd previously done SP1. So they are showing that you there's a correct like using machine assisted proving that the uh and I may be I mean I'm not super deep on the specifics here so apologies if I am slightly off to to those teams but what I understand is that they show that the the formal

Formalizing the EVM

semantics and these formal specs are or what are implemented in the um openVM and SP1 provers using these machine assisted systems. So this is very I mean um you know I came in not as a skeptic but as a sort of undecided person on formal verification and I I see I'm being convinced that that it's it's effective and that these especially with AI tooling like um you can accelerate some of the some of the stuff that doesn't really need a an expert human to be doing it and then let the expert human check the work and and focus on what's important. So um yeah it's we see real really significant progress already.

Okay. Um yeah so oh something similar for the EVM. There are formal specifications of the EVM. I there are several I I didn't call one out in particular because I don't know what the state-of-the-art is there. This the snarkification team would know but the same thing can happen. You can prove that an EVM implementation is uh in accordance with a formal specification. All right. So then um in these last minutes I'll talk about something I've been working on. So uh yeah like I just said uh AI can really accelerate some of this um some of this work. So there does not exist a formal written down um specification of the prover that the ZISK team implements. And this gen

AI-assisted spec generation (Zisk example)

generally true. There's there's been some progress recently, but um and uh yeah, this is um a mature prover that's been running on ETH proofs uh that has great performance and um so it seemed like a good target to see about uh trying to generate like a starter that could become a spec, right? So the idea is can I take this complicated code and turn it into something that is not complicated that then maybe somebody on that team could carefully read and say yeah that matches our intention if we had started with a Python spec maybe this is what it would have looked like so we endorse this and maybe they'll eventually maintain this spec right you can test like this is executable so it's a it's a spec but it's Python so it does produce proofs right so I did this um

Python spec producing identical proofs

and I tried to do this in as hands-off a way as I could really um so I'm sort of designing like some agents that kind of check each other's work. It was not super hands-off. I mean, I did this kind of as like maybe a third of my time over two or three weeks. Um, and I had to be very insistent upon certain certain very basic um, premises, I think. But, um, it's getting to a place where I think it's maybe it's it's time for a more manual tuning of this of this spec. Um, and it works. It produces bite identical proofs to the GPU prover of ZISK in several cases like um so that's pretty convincing to me. It also the the verifier verifies real proofs and I have some you know when I change a bite the

Lean verifier built in hours

verifier complains. So the Python verifier verifies real C++ proofs and not just the sort of base proofs that come early in the pipeline for ZISK but even the final proof the one that would go to the a tester network that it's called a vadcop proof in their case. So it can verify those. But again, like I said, I've been hands off. There there may be some dragons kind of lurking where there's some I don't think there's any return truths in there at this point. But um but yeah, I'm not ready to say that it's it's correct either. Um but I invite you all to look. I linked to it um at the end as well. So this has been uh this has been in a good place for a little while. And then yesterday I thought, well, all right, let's see if we can do lean, too. So I made I made a

lean verifier. And once again, it works. It verifies the proofs. This took about 3 hours. Um, clawed code doing its thing. Um, and you know, I it didn't work automatically. I had to iterate on it for over that time, but eventually it works. And again, I can break it. I can change a bite. It makes the proof fail. That does that's not convincing that it's secure. I might have just chosen the one bite that's sensitive, but but I'm I think that it's it's also not totally uncompelling. I think there's a good chance that this is a correct implementation of the verifier, or at least this close.

Machine-checked polynomial proofs (Aleph example)

One caveat with this that's it's missing the um so in ZISK you take the the really complicated risk 5 implementation and um you compile that's written in a language called pill 2 that compiles to some binary expression. I'm not turning that into lean. I did turn that into Python um in some cases but it's kind of like not clear that that's the right thing to do. Do people prefer to read the Python implementation of it versus the pill 2? I'm not sure there's a readability difference. So we need something else for that part for the risk 5 implementation that's embedded in this. But in terms of the actual like stark protocol that logic is what is in the lean um and and in lean I only did the verifier in Python I did the prover as well. So yeah, I mean um maybe that'll become something maybe that

maybe we can prove that this is equivalent to a arc lib spec and then you know um we get more assurances and yeah another pretty interesting thing that happened is that Alex Hicks who runs the uh who's the lead of the snarkification team um and is behind this verified ZKVM project he used this um it's this prover called ALF by logical intelligence I don't know much about it but it is um it's supposed to be designed for formal reasoning as I understand and he said okay I want to give it a pretty non-trivial statement in uh that's relevant to us so like our polinomial commitment schemes in these proving systems use um this theory of error correcting codes and a key

Final thoughts & references

component of or like an important lema in that world is called the polish chuck spielman lema and he gave it he let this thing just cook for eight hours gave it uh $215 $1 and it made a proof and the proof is correct. So, um that's if you trust the lean then you look at the somebody reads the proof statement and they you should think that it it filled that in. So, it can be that we can prod produce a very robust system of machine assisted proofs of of statements like get assurances about our software um using these techniques.

All right. Well, I'm done a minute early. Here's my list of references. And yeah, thank you all for your attention.