zk(E)VM Formal Verification

Transcript

So this will be a very quick talk so that we can all go to lunch on time and also has time to talk a bit. Um so yeah as Justin said I currently lead the ZKM for web application effort and generally I'm obviously interested in trying to get a fully formally verified stack at the end of today which will be one of the topics of this week. So I normally mention this uh at the end of my talks but I thought I would just mention to start the day since we're rushing up time. So I think one goal with All of this is primarily that we're not interested in just formally verifying things for the sake of it and then saying okay this is formally verified let's freeze it let's never touch it again um the expectations that will continue to move very quickly because a

lot of people do a great job on engineering on the research side and so beyond being able to formally verify specific artifacts that we're very interested in right now we want to make sure that we're establishing good methodologies and good tooling which can actually be used and which are robust and applicable to um a lot of different verification efforts in the future to make our lives broadly easier. The other thing is also that there's a belief on my side and I think probably a couple of people who working on this uh but foration and kind of formal reasoning and automated reasoning uh about code and specifications and all of this actually has some potential benefits on the engineering and research side as well. Uh you can think of a mental model that you know writing things down helps you with your source. Implementing

things implementing [clears throat] things in codes helps you reason a bit more about your writing and then you know reasoning about your code with more replication will probably help you know upstream all of this. uh and we can probably find ways to either maybe simplify things or find things which are over complicated which can be then you know upstream and and simplified level and hopefully also if we get actually good tooling and good integration into development workflows we can get much closer to having maybe a faster development workflow that doesn't require as much auditing and other manual tasks which take up a lot of time and have to be constantly repeated and also not proof.

So the big focus The last year also there's obviously been this big ZKVM for replication project which has three main tracks. the ZKPM track which is trying to assert that you know when you have the constraints and the witness generation uh these work such that you will only produce a valid proof um if the constraints are actually satisfied um and which also amounts to the actual computation that you're proving to being valid um there's a lot of work going into this we actually have some very nice results so we have some risk five circuits which are starting to be fully formally verified against the official risk five specification in lean there's a bunch of work using some key solvers as well which have been integrated into GCI and then we're trying to unify

things a bit with LGK which is this family of ML dialects uh for circuit specifically but there's still quite a bit of work to do in terms of both trying to unify things and trying to make the way that we verify these circuits much more robust particularly in terms of extracting constraints into proof assistance or SMT labels or SMT encoding and being able to preserve some of the structure from circuits to make proofs much more automatable uh which currently not very automatable. We've got the EVM track and this is basically checking that if you take some you know solidity code that's been compiled through the EVM and then you actually lower that to risk five whether you're interpreting it or compiling it you know one way or another uh that we actually verify the risk five assembly

um for this in a sense that the risk five assembly should execute in the same way as a formal spec of the EVM should uh there's difference here the main challenge here is again scale and handling this over the multiple R compile targets sm use and then beyond on that for different EVM implementations once they become you know more supported uh by by CKVMs and then the cryptography track which we'll have a bit more of a focus on this week and Quang will talk about next is around checking that the implementations of proof systems are verified against executable specs uh which are actually validated with formalized security proofs so that typically if you read a paper and it says this construction has run by run with these parameters the construction should be you know an

actual program that's running in in lean which is actually executable and and so on. Now for all of these basically we have progress going on. Uh there's more than I can fit into a 15minute talk. Uh but we have common challenges. One is scale for all of these. So ZKVMs there's multiple circuit DSLs. There's multiple circuits uh pre-ompiles. If every ZKVM starts to have 20 plus pre-ompiles that's about you know 120 pre-ompiles uh total for all the ZKVMs you might be interested in. uh there's a question of auto pre-ompiles and how to verify disc and run compilers in general for for circuits the EVM track similly there's multiple ZKVMs who all use different ROS compile targets at the moment which

produce different assembly and then different EVM implementations that will be coming um online soon as well as to the question of how to move beyond the EVM and to the kind of broader clients um and and verifying some of this we obviously saw some bug in rest recently which was quite critical and it would be nice to be able to catch these and then similarly with cryptography where we have a huge backlog of photography to formally verify uh and uh and it would be nice to get move on with this and to find out you know in the future once we've actually done for some check and some others use now if someone comes up with a great new IO can we formally verify it before peer review uh does its job that would be a nice a nice call to try and get in done in less than a month

would be good now uh this week we've got three sessions uh one will be on arclave. I'll let talk about this in a second. Uh like I said here, you've got a validation of specifications to stunning lean and then a verification of rust implementations to stunning lean via tools called hacks. We've got another session on end to end verification which Julian will be leading. Uh the goal here is to look at how do we actually cover everything that's really required uh for for ZKVMs on Z1 and beyond. And we've seen obviously you know we've got all the lean VM lean zig and lean xyz's uh consensus obly we're not touching at the moment but it would be nice to get to that if there obviously a lot of interesting changes coming and then

compilers is something that DARPA was going to bail us out as a verified R compiler and then Trump happened uh so now it's on us to get that done uh and then we'll also have another session on encoding for people signatures which would be a good practical example of how do we move beyond what's currently going on with the verified the KVM project uh into other parts of the scope that will be part of end for verification. I'll hopefully leave it here. I think I've watched it enough and I've talked fast enough and then I'll let Kang have a bit of time and hopefully we can all get to lunch at a reasonable hour as well.

Thank you. [applause] And I guess any questions? Any questions while we wait for conf to get set up? >> I guess I have a question for you, Alex. Um, in terms of timelines, do you agree that the three to four years is sufficient to end to end formally verify everything?

>> So, I think by end of 2026, we'll have the ZKVM part of things done up to things like CUDA kernels we're probably not touching unless we have a breakthrough in terms of how to address that. Um so we should have let's say formally verified verifiers formally verified risk five circuits and pre-ompiles or auto pre-ompile compiler that should be okay. Uh formally verified uh EVM lo 5 should be okay in terms of at least specific examples of EVMs and potential caveats when it comes to uh interacting with the the blockchain itself and the host and

composing different op codes. We'll see how we make progress on that. And then for cryptography, we should have formally verified specs for proven as verifiers for all proof systems which are used. And then that should free us up to deal with the compiler stack uh in 2026 2027. Hopefully if we do something domain specific seems doable and then consensus also seems doable for the specs. Varification of implementations of consensus might be a bit tricky because there'll be another issue of scale and different angles. I think that mostly covers it and at lem stack. So that should be fine and we should be able to reuse kind of most of

what we're doing for themselves. Thank you.