Ethereum's ZK & Formal Verification Endgame with Alexander Hicks

Transcript

in practice snarfy the ethereum layer one isn't something that's been announced as of yet you know this is the opportunity to announce it so it's really interesting because I spent a bunch of time quite a few years ago now looking it welcome back to the rollup in today's episode Robbie sits down with Alexander Hicks of the ethereum foundation to talk about ethereum's ZK and formal verification endgame following our recent podcast with Justin Drake about a the's road map we set out to understand other key components of that discussion in further detail real-time proving formal verification and building a more resilient smart contract environment for ethereum were the topics that we discussed we also talked about the foundation's ongoing efforts to apply formal verification to

zkv Ms as well as a 20 million doll ongoing developer bounty to build formal verification within the evm we learned about the importance formal verification as well as the key balance between cryptographic and economic security hope you guys enjoyed this episode and let's jump right in after a quick word from some of our awesome Partners vertex Edge is now live on say Network say users can now trade 50 plus spot and per markets with the unified order book liquidity of vertex Edge across arbitrum blast mantle and SE the next 6 weeks 850,000 say tokens will be up for grabs as trading rewards every

single week exclusively on join vertex on network now on vertex Edge that's vertex protocol.com welcome aboard on our journey into the singularity this is the endgame roadmap for frax and fractal the new L2 out of the frax ecosystem that is totally based on fractal scaling fra still the modular L2 blockchain built by fra with modular and fractal scaling in mind fractal scaling is based on the mandal BR set of fractal images and it explains how l2s become l3s and the entire app chain life

cycle goes through its Evolution the frax ecosystem is made of some of the top builders in the space and has stemmed from its OG days of the frax stable coin it is now in the LST space the LRT space and this frax L2 joins the existing Suite of fra products including fra Swap and fra lend you can see frax fairy the bridge to go from any chain arbitrum optimism or main net into the fra main net Bridge your tokens and bring your FRA assets into the fra ecosystem join today to get the best out

of fraxel you are still early join today take part in our Expedition into the singularity gmgm what's up guys welcome to another episode of the rollup Alexander Hicks today is the guest from the ethereum foundation Alexander is uh working on formal verification at the ethereum foundation we're going to talk all about that in the upcoming program around formal verification of ZK systems Alexander your first time on the show welcome man thanks for coming nice to be here thanks for having me and um yeah first podcast so funny funny experience I guess and uh you know you you recently joined the the EF um congrats first off

and uh you know maybe we can talk about uh kind of your story you know what what were you doing previous to joining ethereum um how you know what what kind of LED you uh into this space that you find yourself today yeah so it's been a very indirect pass in in a lot of ways I think I as far as kind of blockchains go um I spent a lot of time online as a kid probably too much and so I randomly heard about Bitcoin fairly early on maybe 2011 2010ish uh which would have been when I was kind of 15 16 and I always had an interest in computers I spent far too much time online um so that kind of comes with it um but I didn't get involved um at that point uh obviously I

was far too young to actually buy Bitcoins I didn't have any kind of credit card or anything um and I ended up going to study kind of physics and then math at the University um but I always still had kind of an interest specifically in kind of computer security things and I was doing my masters in Mass I was applying for phds in Mass I'd actually accepted an offer to do PhD in Mass um but I was getting kind of less and less I guess committed to doing it and So eventually actually um I had this offer I sent him an email I said look guys I'm not going to come um and and then I had a few months to decide what I wanted to do instead and and I was looking out of the tech and everything and for OB for a few reasons

one was I had an interest in it obviously in terms of you know finding a job it it was quite attractive and I was trying really hard to not go and work for a bank which is a very typical outcome if you do a PhD in math um and through essentially a massive coincidence um one person who I was in touch with when I was doing my masters her husband um was a guy called Steven Murdoch who is a kind of very very amazing security researcher um he's the original creative the tour browser and and done a lot of cool work and yeah so he was he was her husband and so I'd mentioned I was interested in doing a PhD in computer security and I had an interest in that uh he was looking for a

PhD student at the time um so long story short is I applied um got in and that was my Pivot into into Tech in computer security related things um and and I'd also done a bit of um formal verification at that point as well but on Purely on the mathematics side and so I kind of came in um to do this PhD and this was right at the time where I was at UCL UCL had a lot of really good researchers who had started working on blockchain related things right at that time so you had Sarah Mel John um who done some work on denormalizing bitcoin some of original papers on that um and and was kind of is an excellent

cryptographer George dessis who was starting to do some blockchain related work as well and he later went on to to be a founder of chains space they you know he was at meta when they were doing the their own kind of blockchain project which was very shortlived and and now he's at s um you had obviously Yan gross of gross 16 fame um he was doing kind of purely cryptography but obviously gross 16 went on to to be kind of one of the most important pieces of work for for blockchains and and everything ZK related um and so I think because of that there was OB a lot of other PhD students who were doing work on blockchains obviously Mary maler is a cryptographer thef she was there at the

same time um Patrick mccy who's at JB from Foundation now was there um sarahi who's now at scroll and was at PR as before was there and so I kind of got to talking to a lot of people who are working on blockchain related work work and that meant that naturally I find myself doing blockchain related work as well um that's that's kind of the way it goes when you're doing a PhD you kind of just talk to people and and find interesting projects that way and so my T is actually isn't necessarily blockchain related um blockchains do show up but they're not the main topic I just use them for for certain things my thesis is just on transparency and trying to make systems more transparent um but then I also had a bunch of papers on on blockchains and decentralization

and some kind of game thetic aspect of blockchains and so I was interested in that and and that means that I've kind of been around at least the kind of academic research side of of blockchains for since 2017 um more or less so quite quite a long time now um and this was also the time when eum was the new thing on the Block it was really interesting it's always had OB good Comm good academic Community during research uh related to it and so that spared my interest in in assume you know more specifically I think Bitcoin I always thought was interesting but maybe the kind of digital gold side of things was less of uh was less Min interest than it is for other people the kind of decentralized computer side of things was was a lot more interesting I thought

um and there were OB eum now I think maybe you know some new chains are more experimental but certainly the time stre was was the one project it was really experimenting and pushing things um obviously was you know even things like proof of stake and and new ideas around decentralization and smart contracts and that was really cool um but but yeah so I did my PhD i' done some work that was related to ethereum and after doing my PhD I was looking for work and I also wanted to go back to doing something a bit more mathematical and a bit more proof-based and rigorous and I guess partly for a bit of a change and to kind of get back to some of my roots in in mass and I was very interested actually in not only blockchains but also kind of

prediction markets and Ai and my was actually that I S um there was a lot of issues with with a lot of AI tooling and I was looking at it in the sense of you know I kind of want to do want to prade in prediction markets and and I mean I was and there's a lot of work that goes into this which is actually you know scraping the internet for a lot of information about what you're what you're trying to predict and trying to understand it and this is something that LMS should be good at because they're just trained on all the content that's online especially when it's content that's maybe in in different languages and it's a bit harder to get a hold of um and there's these kind of basic issues around like reliability you know like hallucinations aren't as bad as

they used to be a couple years ago um but you had this sense of you know there's a lot of like llm magic happening and it would be nice to be able to kind of certify the outputs that you're looking at um and so I was thinking a lot about this and a lot about essentially kind of form verification related to Ai and trying to formally verify the outputs that you get from L&M whether that's code or was you're prompting it for a question and you want to check maybe the chain of reasoning that's been used or or how it's arrived to a certain conclusion and and things like that which is now you know that's its own kind of field of research which is very active um but immed I was looking essentially at form verification and AI related things and and still obviously interested in

blockchains and then Justin Drake posted this tweet that was something along the lines of you know if you love AI in ethereum send me an email um so I sent him an email and and it turns out that um I guess you know kind of ly cois is there again I ticked a lot of boxes because I mentioned form of verification I mentioned AI I mentioned blockchains and this is exactly what they were looking for because you know vitalic and and Justin had dreamed up this idea of trying to formally verify ZK VMS and one that's a really interesting project by itself two it's a huge project which means that to try and scale things up it'd be really nice be able to use some

kind of AI tooling there um and and that meant that they were looking for someone who had an interest in AI had an interest in form verification had an interest and understanding of blockchains and and so I kind of you know fit essentially um quite well into that and so so I started talking to Justin started you know obviously kind of working a bit with him and and then just ended up ATF um and now and now we've got this big project that just launched um a few a few weeks ago on trying to formally verify ZK VMS and and that entire stack of of software that you know at some point I guess a lot of people are going to rely on to to transfer funds and store funds and and we want to make sure that that's as

secure as possible I think this is unfolding before our our eyes this transition from optimistic to ZK is something that we've heard a lot about there are projects that are starting to deploy and then there's the the entrenched large uh rollups that are currently optimistic but planning for ZK and have already started to incorporate some ZK into their docs into their Forward Thinking vision and their road map and we're we're starting to hear more and more ZK types of of language and implementations coming out of some of these optimistic uh powerhouses so so I think uh absolutely um maybe we can touch on some more of that that uh that

early stuff later on down the road because I think a lot of that is really fun and tend to agree on on a lot of the thesis but let's talk about formal verification in general and how it relates to ZK VMS because you know I think that is the consensus view this is the the the the direction in which we're heading um and something you mentioned to me when we first spoke was that you know the the the idea is unchanged the the Global Financial system this is a a global Ledger and there's trillions or quadrillions or more dollars you know potentially at at stake here um on these ledgers and so it's important that these are secure systems and this speaks to the computer security background that uh

that you know you you went through and experienced in your kind of formative career so so let let's talk about ZK um or let's talk about formal verification in general and then dive into how it pertains to ZK and then ultimately how how it uh impacts ZK rollups yeah so form verification is is a big topic um it's just in and of itself it's a big topic it's something that's been going on for decades at this point um and it's something that touches quite a lot of things so in practice um it's both an interesting Cal subject right how do you check that something is actually correct and and that has it roots in kind of the

very origins of um theoretical computer science and even going back to mathematics and you know what is a proof and how you check that a proof is correct and and so on and and even you know kind of logic and applications of logic but it's something that's also quite practical so if you're taking you know a plane um there's likely some formally verified code running in there because obviously the cost of failure if you're in a plane is quite High um and and it applies in a lot of a lot of other cases um if you're running Google Chrome uh the Google SSL library has some formally verified code in there there was there was generates to generators to Tool called fat crypto um so it's here and there and and you do use formally verified codes you know if

you're using regular devices and and browsing the internet without necessarily realizing it but a lot of code isn't formally verified because it's really hard and the problem that you're dealing with is is toold um your goal is always to try and you have a you know try and have a specification for your software and what your software should be doing and then trying to show theual code that you have matches that specification so that's inherently hard because one you don't always have a good specification a lot of the times you have code no specification um and two it's really really tedious because you know a lot of people have some familiarity with the idea of a mathematical proof uh which you might

have done in you know high school or if you've studied any kind of mass at University you might have done some proof-based courses and so we all know that writing proofs can be tedious and and difficult even if you're a mathem I and that's what you do day to-day um it's never an easy exercise and for software it's even harder because you're looking at an artifact which is code written in some programming language which isn't naturally amenable to to formal proofs and you can have bugs at different stages you can have bugs in the code itself you can have bugs that are introduced by the compiler um it's very easy for for S to sneak in you know regardless of program expertise and and essentially you know pass a certain

threshold if you have thousands and thousands or even millions of lines of code you'll always have bug in your software maybe it's critical maybe it's not but but you will have bugs and so Translating that code that you have into something that's formal enough um in a formal language something like C or lean or using automatic logic solvers like smt solvers is difficult in itself and then once you've done that you're still not done because you still need to write the proof and the proofs that you're doing that have to be checked by a computer are really really tedious like you're far more tedious than writing a proof on paper because you really need to do every step um and make sure that every step is in there so if you think

of you know if you're trying to do some basic mathematics on paper you can skip a lot of things like you know that you know if I give you two integers you know a plus b is equal to B plus a and that's obvious and you don't think twice about it if you're doing it with an interactive proof assist since you have to specify you know you have to find the LMO that you're looking for and and you know call it explicitly to be able to do that kind of really basic step and when you're looking at a proof with a lot of steps um it's very easy to get stuck on on kind of simple things that would be obvious and and for software which is even more complicated than than math in a lot of ways you start getting into using specific Logics and so people work

on you know things like separation logic to to isolate you know the kind of side effects of code and and make sure you can look at you know some local portion of the code and and not have to worry about the rest you have um H Logics to to look at you know where is there something if you have the state um before you run a program then you run a program then you have another state how do you prove that you know the state that you get at the end is is what it should be having run that program and and then you have for cryptography for example we have to reason around probalistic programs and that's also something that's not it's not obvious how to do um it's something that people figured out obviously in the last few

decades and then riding the proofs is really really hard and and for example if you look at there was a a really cool project recently from from ZK sync they were forly verifying their uh their verifier on on chain for for the rollup um and this was a couple months of work for one smart contract that's you know it's well understood you know it's a it's a fairly reasonably size smart contract the kind of cryptography that you're verifying is is fairly well understood um but that's still a few months of work by a few people and and so it's just inherently hard to do which is the which is why you you end up with you know less code formly verified than what you would like um and and there are

many ways also to tackle these problems there are a lot of different techniques uh people in some ways can be quite tribal about how they approach things uh both in terms of you know some people prefer different languages to to do this some people prefer to do things you know by hand Some people prefer to do things with more Automation in practice you kind of meet in the middle because if you use more automation things break when you give it when you you try to do big problems and so you have to Define you know sub goals that automation can solve and if you do things by hand at some point you want some automation because otherwise you'll never be done um so so yeah it's a really big um it's a really big Topic in itself it's a big topic of research you know people still

publish you know many many really cool papers every year on this um and and it's something that's constantly improving um things are constantly getting better things are constantly getting you know easier to verify automation is getting better both through you knowly more computation but also through better methods and and even on the manual side things are getting better with better languages so you have you know things like lean which are you know very new and exciting these days is is you know doing making a lot of waves and and getting a lot of people excited um and and obviously other languages you know kind of Co and Isabelle and that have been around for a long time and have you know um have resorted in in a lot of really cool projects but we're but we're still on at a stage where

where form verification is exactly what you wanted to be which is taking any potentially critical piece of software and being able to verify it um The Hope is that we make progress on that end because as software is only getting more critical as we're kind of embedding technology in in more and more things um we've talked obviously about you know ZK VMS you have potentially billions of dollars you know depending on on a few um on a few kind of software artifacts and you can't have them not be formally verified and if they're not formally verified you can't really stand up and say Hey you know trust the code not humans um that's that's quite unreasonable and a bit responsible at some point um but even outside of that

you know people are relying on maybe something like pacemakers for health um that's the kind of thing that should be formally verified as well because if something goes wrong you quickly run into you know potential critical health issues um so so yeah it's something that really has very direct applications to a lot of things despite the fact that it looks quite abstract and theoretical um from a from a distant view I guess and so it's really interesting to get into um and it's really interesting to try and get into the hands of more people as well um there's such a big gap now between formal verification and developers and that's part of the issue that's why a lot of the times we don't actually have you know good formal specs

to to actually work with on on the formal verification side because developers are so far removed from formal verification and because specs are not inherently useful for them if they're writing you know the high quality code that they're writing you you have this this natural Gap that emerges and so there's a lot of things that you can fix actually by trying to you know get a better blend of you know developer experience and form verification uh while still obviously working you know purely on on making form verification itself better um and and something else that's also quite cool is because a lot of the code you're working with is depends on optimizations and again with ZK VMS they're getting faster and faster and that's because

they're getting better and better optimizations it's not only about hardware and Hardware improvements and using gpus and the more you push things and the more you optimize the bigger the chance that you have maybe bugs that are introduced and potentially also they become harder to a it and so the necessity of form verification is also that auditing is inherently limitted you can just make a mistake and once you get maybe you know really big circuits with an insane amount of constraints um they're really optimized it's really it gets even easier to make a mistake if you're doing an audit and that's where formal verification is is really critical and and plays a role not only in act correctness but also in

actually allowing you to push optimization further and get more performance so I think a lot of times there's a single narrative that's focused around security and the correctness of code but I actually really think that formal verification is something that allows you to get not just correctness but better performance and some teams like the the AWS automated reasoning Group which is a massive massive group in in industry uh I think it's maybe 100 or 200 people it's more or less unparalleled in that sense they have a lot of really cool work done where they sped up the the speed of cryptographic operations for authentication within AWS and things like that and they've really I think pushed things on on the side of you know

performance through formal verification where they can deploy code that they would otherwise never deploy because it looks like really hacky assembly um and and you would never want to audit it and and I'm hoping that we can get to to the same to the same level for us with ekk VMS and and actually be able to push not just correctness but but also performance together and and getting better systems overall um so so so that comes into play as well but um but it's always still kind of going back to the basic idea of what your specification is what do you want your code to do and how do you show that your code is doing exactly what you wanted to do and won't have unintended behaviors um whether it as for bugs or you know just things that

aren't specified well um because you know traditionally if you speak to people who look for bugs and code and look for exploits the first thing they'll say is you know you read the documentation you check which part of the documentation looks weirdly written and that's where the bugs you know are hiding and that's the first place that you look because if it's not well understood you know even at a high level by the developers you know that's where mistakes happen um so so it's really an exercise in in you know specifying what you want from your code and and being able to check the the it is so so in that sense it's not in that sense it's not so abstract um it's really really practical it's just once you get into actually trying to do it that you need to get into the Logics the necessary and

and using the required mathematics to to actually get results um but I think everyone can understand what it means in practice to to formally verify things yeah and to your point it's so complex because the mathematics behind it is so is fractal because you know you get to you get to a certain part that you know you sort of just take to be true but you can't just take anything to be true and and so once you once you you know get into it uh there is a proof but then you know you end up finding yourself well you know can we just assume that 2 plus two is four or do we have to prove that too and it goes down the rabbit hole sequentially as as you have to prove deeper and deeper uh some of some of the

most basic assumptions so you have to be you always have to be realistic as well right I think one maybe one interesting thing to point out is you obviously always have caveat in terms of what assumptions you've made and you know even if you have a large software base software code base you know sometimes you'll you'll form to verify critical pieces of the code maybe the cryptography and leave the rest and and you always have to be clear exactly about what you're actually showing you can't just say it's an abusive language to take a piece of s and say this is formally verified you should always qualify exactly what you've verified and and how you've done it and and what the caveats are um because you do have yeah you do have assumptions and and because it's hard you do have to be practical and you have to stop at some point and

and that's still a human Choice that's not a that's not an automatic choice and and so you have to look at what your resources are what you can do in terms of Maintenance and and how much you can invest into it and and that's where you that's where you decide you know where your limit is yeah and and so you know all all this is culminating in in the program that that you're leading uh at the EF uh this is uh an a program that is um going to uh put a lot of resources behind formally verifying some ZK VMS I think there's quite a few teams involved and if this isn't something that's been announced as of yet you know this is the opportunity to announce it so um so yeah you know please uh that was a great overview of

formal verification uh May dig into a little bit more of of the implications there but you know tell us more about the program uh what what is it um how can people get involved um and then ultimately you know we'll get into some of the downstream effects of of what it means once these formal verification uh tooling is available to to zkv M researchers and developers um and then and then you know kind of the life cycle of this program and and uh what it means welcome to the ignition Mantle's newest campaign to liberate the growth power of Bitcoin fbtc ignition has officially begun with a total token supply of over 2,000 fbtc with a tvl of over 150 million right now you can go on

the fbtc website to see all of the featured campaigns staking opportunities and liquidity pools where you can utilize fbtc on chain today for some of the best yields available on l2s the ignition Sparkle campaign can be found at fbtc docomo yeah so the program is the program is really really interesting so the the basic idea is quite simple and this is that ZK VMS are becoming increasingly popular they've shown that you can take any arbitrary let's say rust code or any code from some language that compiles via llvm and you can run it on a zkm because it has a general

circuit for risk five let's say and it can be wome it can be something else maybe obviously Caro for example but letic was was risk five and so yeah it's it's in some sense kind of magical you go from having maybe ZK EVMS right now for the rollups where you have to do your circuit for the evm when the evm changes you have to change your circuit and and it's a bit messy to maintain to a nice risk five ZK VM the RIS fire visor is the instruction set is is quite stable um once you have a circuit maybe you change it for optimizations but you're it's at your own will um and you can run any kind of you know rust code and obviously Russ code that includes

the evm written in Russ for example so you can do a ZK rollup on top of a ZK VM and and it and it works you know more or less out of the box um it's probably e much easier to set up than a ZK evm and and traditional ZK rollups so it's very magical in that sense but obviously there's a lot of cryptography there's a lot of you know interesting work around the compilers and there's a lot of really nice software engineering goes into it and that means that these things are quite complex and so going back to this idea of if we want to use blockchains with with the basic principle that we want to trust code and not humans um then you need to be able to trust the code and if the code is a really interesting but quite complex software artifact um maybe you shouldn't

just blindly trust the code and so if people are going to run rollups or other applications there that are really important you know financially and holding a lot of user funds you know we don't want the user funds to get lost and you might look at it from the perspective of the is foundation you know our main concern is layer one but if a lot of rollups are running on ZK VMS and then they blow up for whatever reason because you know some bug just gets through then potentially you know you lose a lot of user funds maybe you're back in the same situations when you that the D hack you know quite a few years ago and maybe you need to think about forking the layer one and that's not a that's something that we would like to avoid obviously um we've had that debate once I think forking was the

right choice but if you start having that debate too many times you know you kind of lose the point of of having blockchains really and so so we want to make sure that these things are are safe and there's a longer angle as well that I think we'll probably get in later which is you know if we want to snarfy the evm and the layer one itself you know potentially then the lay one itself starts to look a bit like you know the evm running on top of a on top of zkm um so there's there's some long-term angled as well which I think will help us out in in the end but at least in short arm it's really about making sure that what people are using to transact on ethereum is actually secure and we can actually you know stand up on stage and say this

is fine you know you can leave your savings or some portion of your savings on this and there's an insanely high probability that this will be fine and that you'll be safe and that you won't lose um your money and this also works for insurance right at some point if someone develops some kind of insurance mechanism for in case there are hacks you know maybe you have two different rollups and you have insurance across different rollups then then you're going to price that insurance on on the likelihood of there being some critical bug um that can affect us the funds right so so it's all about kind of safety and and makeing sure things go in the right direction and so so yes so we have this project um it's now officially launched it's been in in the works for

for a few months um but as of kind of earlier in September it's launched you can go to verified dzk vm. org and and there's some details there the details for now mostly around uh mostly there for the teams who will actually kind of participate in in help in informally verifying everything um as the project evolves I'm going to put a lot of time into writing documentation and making things as accessible and clear as possible for for everyone um both s that people get a sense of you know how good the work the people are doing in this project is um but also sort of there's maybe a bit more awareness and appreciation around form verification because if that happens then there'll also be better incentives for ckvm and

rollups to formally verify their code um you see it now you know if you go on Twitter they're they're very proud to announce when they've passed an audit which is great and ideally you'd like them to be able to tweet that they're very proud to have formally verified you know whatever part of their code base and people can see it and and and be enthusiastic about it um and there are some there are some longer term plans uh around that kind of user experience side of a formal verification um but for the project itself um yeah it's a big project because there's such a big um software artifact that we're looking at there's a $20 million budget um it's a real investment there's you know all of the teams that we can get to

participate will be participating we'll be getting obviously paid to to do it um and the budget is good enough that we can we can accommodate that we can accommodate you know really in-depth work and that means that we're also trying to make sure that beyond the lifetime this project which is let's say two years um the things carry on beyond that so it's really trying to Kickstart a general effort for formal verification around ckvm in and more broadly in this ecosystem um there is already obviously some efforts going into smart contracts and and so on but we want this to be as big as possible and and to look at the infrastructure itself so there'll be a lot of effort into developing better tools and better maintenance procedures for formally

verified code bases and so it's not just a one-off effort to take you know some version of the code formally verifi it once and then hope for the best um because I expect the code to keep changing you know for the next few years um that means that we get better performance um do we get maybe more usability do we get maybe kind of more support for applications um more functionalities client side proving you know down the road um these are all things that we can improve on or ZK M can improve on I guess that's their job and and I want to make sure that whilst they're doing that and whilst they're pushing updates and making things better um they can also still um remain formally verified you know within the

lifetime of this project and and Beyond um so so there's a big focus on on tooling and and maintenance and documentation that will that will come and and hopefully that means that also people have an easier time following things and and learning more about it um so so yeah so the project is started now I've started getting uh Grant proposals to to address some of these things particularly around the the circuits and the AR metalizations and formally verifying the evm itself um that's obviously a big part of trying to make sure that things are secure it's not just the zvm it's also making sure that the evm that people are running is is actually good and in matches the the kind of formal specification that we

expect from from the evm and and doing that is actually you know quite hard because DVM is is not that small and and there's obviously kind of around the formal spec side of things we have actually several formal specs plus the Pyon execution specs and there's you know some work that needs to be done in checking that these are all actually the same and that we don't actually have multiple formal specs that disagree with each other um that'll be that'll be an interesting question um and so for the kind of circus and rization um we want to make it easier not just to write circuits that we can check for correctness but also to just actually write correct circuits in the first place um it's really um it's not very efficient if you write circuits that have bugs in them

and then when you try and formally verify them you find bugs and then you do it again and then maybe you find bugs again and so on what you really want is you want it to make it you want it to be possible to write you know correct circuits you know from the first go in a nice environment um in a way that's easy and accessible to not just someone with a PhD form verification but someone who actually you know is already writing circuits for example um because you already have really talented people writing circuits and if anything we probably need more people to be able to write circuits um because this will mean that we can actually scale um scale things to to more applications um ckvm do a good job of having you know one circuit that works for a lot of things

but there always be a question of having you know more pre-compiled and maybe circuits for speciic applications and obviously you had that whole debate already in in a past episode um and I think ideally you know we get to a point where where it starts to be much easier to write you know correct circuits from the get-go that easy to formally verify making sure that evm is formally verified continuously because we'll have we'll always have new OP codes coming um the layer one is not stagnant right it's still going to change and the evm is still going to change for the next few years um and so yeah so so it's a big effort to kind of Kickstart things we want to make sure that by the end of the

project we have a formally verified ZK evm which is a formally verified evm running on a ZK VM and at all of the existing ZK VMS um with that's you knowly the RIS zero team uh stinct valer Nexus uh powder uh more that I'm kind of forgetting off the top of my head uh we want to make sure the they will benefit from from the work we do um in a way there not just a one-off effort but in a way that that runs in the long run and that that means that when this product is done they can carry on um Withings because they're they're all committed to to making sure that their code is secure and and verification and so we just need to make sure that we can get to a kind

of nice point where where things can move forward um forever and and be maintainable yeah and the main motivation here is obviously the ZK VMS formally verifying the ZK evm making these these systems safer for people to put their money into but to your point a little bit earlier in the podcast formal verification has far-reaching implications beyond beyond blockchain and and the software systems fi Financial software systems so so yeah I I I think uh you know could do us to the ethereum foundation putting resources behind something uh that is obviously going to help our specific niche of the industry but could have far-reaching implications to you know like you said pacemakers and hardware and and you know

very important pieces of of infrastructure uh Beyond blockchain this great Bas way as well right sense of we're we're trying to drag in people who do form verification and who don't do blockchain related things into this as well um because because then we also benefit from a lot of the expertise that is actually already out there and and that is already doing you know really cool work yeah so here's the website it's a verified uh- zk. org um and it's a project by the ethereum foundation to accelerate the application of uh formal verification methods uh specifically to ZK EVMS um you know you went over uh the overview of the project to apply uh this this uh formal verification to ZK EVMS

you know kind of the motivation here again is is you know making these systems safer um especially since we anticipate this transition from optimistic systems to ZK um some of these ZK systems are already in production today um and so there's a few different tracks here there's the evm track uh to show that an evm running on risk 5 correctly implements uh the evm spec um and then you have the cryptography track as well and so uh what's the best way and then you have these stages right um for first uh different applications and then stage one and stage two um and so okay here we have uh kind of the the

grant process for anyone who's who's listening that wants to get involved um you know uh I imagine that this is this is open to pretty much anyone building the ethereum ecosystem or with some pre-existing knowledge in uh formal verification submit a grant proposal um and then uh and then send it to this email here verifi dzk evm at ethereum.org um and the the review process is ongoing it has been for about a week or two now so um so yeah this is open and uh how long how long will it be open for for team to apply um it'll probably stay open more or less indefinitely in the sense that if

someone has a cool idea I'm always you know they're always welcome to to get in touch and and see if we can if we can get some work done um on it and get some funding for it um obviously at some point there are at the moment there are some you know suggested uh projects which are there um these at some point will have you know grants approved to to work on them and so at some point you know it'll be kind of pointless to submit a grand proposal for that um but but yeah I mean we're getting suggestions and proposals for for different Tooling in in different tools um and we're always open to these um and then at some point we'll also transition to stage two which will just be a different Focus once we feel comfortable with what we have for for circuits and

arations and and some work going on with formally verifying the the evm um then you know we'll also have more of a look at uh the cryptography and the implementation of the proof systems um obviously requiring us to also get uh a formal spec of the proof systems and and I have some Grant proposals to to address that as well um so yeah it'll it'll essentially always be open what will change will be the focus and maybe some you know specific projects that are explicitly advertised um but anyone who has good ideas is is always welcome to to get in touch and and I also expect that you know part of this uh project should be that we'll get some work done which will make it maybe easier to D

circuits and things like that but then we might need to extend these things right maybe we want to have support for more ization schemes maybe if there's some you know we we'll have a library of you know formally verified cryptographic protocols so for the commitment schemes and the iops um adding to that library to support different commitment schemes different IPS uh and even you know the different specific Fields people are building on um whether it as something like vas for example these are things that people will be able to contribute to um to that work that'll that will start soon um and so there always be ways for people to contribute with you know bigger or smaller projects um and and including building on other people's

work awesome uh couple questions here as as we sort of come come to a wrap [Music] of carte is your home for app specific rollups at the Forefront of developing new tools and platforms that enhance the capabilities of blockchain Technology carty enables applications that are flexible and built to scale build on a full Linux environment and use traditional software libraries but in blockchain development go to cars.io that's cars.io to learn more about building your own app chain today you know we mentioned uh kind of

that previous podcast which which was sort of it it was positioned as a debate uh between uh General ZK VMS and custom circuits and a lot of this formal verification work is going to to you know make it easier to to write custom circuits and so do you have a particular side of that debate that you you find yourself uh leaning towards more the custom circuit or more the generalized ckvm side I'm pretty agnostic I think for some applications custom circuits will always be useful and you see this now with pre-compiled right if you look at pre-compiled they're abely essential to the performance of otherwise General VMS but they're essentially custom circuits for certain you know for small bits of you

know hatching or arithmetic operations and things like that so even if you have a general zkm you'll still need specific circuits for some things just for performance reasons so you know if you look at sure you're doing a roll up as a an evm that runs on a zkm then at some point maybe you have an evm pre-compile and I think you know probably Justin has probably spoken about this um you know at some point that if you want to snar if fire the layer one maybe you have an evm pre-compiled inside the evm you know some something like that um what that what do that mean in practice snarky the ZK or snarfy the ethereum layer one so I think the biggest difference is in terms

of consensus where currently you know every the nodes in in a part of the consensus protocol reexecute the computation that's required by the smart contracts and and the different transactions that they process and that's pretty bad because competition you know as competition kind of grows within smart contracts and you know if you look at people who are doing maybe AI computations right people on decentralized inference networks you absolutely can't have every night you know redo the kind of AI workload um that would be completely insane so so you're going to have to ideally switch to verifying proofs instead of instead of re re-executing computations um

that's the first step and then once you do that and you're looking at okay you can have ZK rollups now and they submit a proof to the layer one and in the layer one you know you verify the proof instead of rerunning the the computations as you would for an optimistic rollup with a fraud proof system and so that's already a start but then you start to think you know sure if you're um suggesting a new block and there's a state transition for for the block for the layer one itself then the easiest way to do that is actually to just you know produce a snar that that state transition is valid and then people start verifying you know snarks of evm of layer one state Transitions and things like that um and then I think that's the direction that things are going in in terms of snark ifying the

the evm it's just making sure that as much as possible you're not rerunning computations you're just verifying proofs and obviously with the assumption that you know these proofs are are much cheaper to verify than computations um but especially as we get to a world where people are maybe running insane computations on some decentralized Network and rerunning these confrontations is actually not you know kind of a reasonable idea in any way then then it actually becomes not just an improvement in terms of what we're already doing but also something that allows more applications to run on top of etherum um or or any other network um so that's the idea there and and yeah I

mean at some point you know is there going to be a big difference then between a ZK rollup and and and the layer one itself um things start to get much closer I think there'll still be room for both for for scalability reasons to support different applications but but yeah the lay on itself will probably look a lot more like a a chain of you know proof verification um rather than a chain of you know re executed computations um to keep things cheaper make it more scalable and support more applications yeah and o overall this is so you you said something a bit earlier maybe towards the beginning of the podcast which was you know around around computer security and and uh kind of what what led you to

formal verification and I think it made made sense because uh that that blockchains and uh ethereum was sort of a natural Landing point because uh I tend to think about uh blockchains as uh the coordination mechanism for uh the for cryptography and computer security um and so you know because there's a lot of value that's at at stake here um it has to be really secure and we see the incentives coales around around some of these systems so uh to that to that point you know we we continue to see more and more value uh ACR to these ACR to these systems

and uh because the we have like this coordination mechanism with all this value at stake uh you know we we've kind of gone from bitcoin's cryptographic proof of work security mechanism to more of ethereum's proof of stake cryptoeconomic security mechanism but as we progress it almost seems as if we're kind of coming full circle and going you know more again into the cryptographic security uh but but you know with a combination of cryptoeconomic as well so maybe to kind of take take us home here you know how do you balance uh from a computer security perspective cryptographic and cryptoeconomic is there is there a a a balance to both is

is there one preference to the other generally how how do you view this uh from from a security systems perspective it's very interesting because I spent a bunch of time quite a few years ago now looking at precisely the section of both and and how they related because obviously we have these very fancy cryptographic mechanisms and these are very strong so if you you know if you've got encryption um you know it's meant to be essentially unbreakable unless you've you know really messed it up in terms of the implementation or specification um but maybe it's really expensive to run and maybe if you make some assumptions around the economics or the rationality of hpin in the network you you get to maybe not use certain cryptographic

mechanisms that are expensive to use you get to maybe be more scalable um and so you always have these these kind of trade-offs um in terms of pure security nothing will ever beat Pure cryptography um in terms of running a real system where people do obviously have Financial incentives um and and even non-financial incentives right people might care a lot about decentralization and sensitive resistance and and things like that and and even for kind of you know I I say this in terms of people you know it's one thing for maybe one user to have these incentives but if you're looking at you know people who run validators parpa in consensus um now that you have maybe major institutions who are kind of

you know running things through ethereum and and with stable coins and things like that um you're talking about incentives for potentially kind of you know not just the average user but big institutions and and big players that have also a fair amount of kind of power financial means uh and you know kind of there's there's a bunch of politics to get involved into this and so on and you can make some assumptions around kind of their behavior and around their incentives in the economics there but that's always I think based on waiting for better cryptography and waiting for better formal models that give you stronger guarantees um so I think we've seen this move forward in quite a few

ways um yeah because you talked about kind of I think you mentioned Bitcoin is being kind of very much on the kind of cryptography security guarantees type of type of thing but actually Bitcoin there's a lot around you know the miners and the incentives for miners which are really purely economical um and and you make some assumptions around you know if the price of Bitcoin doesn't go up and the and the Bitcoin rewards you know halves every every few years you know is the hash rate for that secures a Bitcoin Network and this keep going up because the hash rate might become more and more expensive in terms of dollars which is what you buy your your machines with and has to be outweigh by the rise in price

of Bitcoin and so you know it depends on your feelings around whether Bitcoin will keep going up but you have these kind of inherent you know economic ideas at the very basis of it regardless of security of the hash function for the proof of work um algorithm and and I think for ethereum there's always been kind of a lot of openness around experimenting with economic ideas and I think maybe for a long time there was a bias towards thinking that you could get a lot of efficiency out of relying purely on economics without too much cryptography I think that's maybe shifted back de way in in the past few years um and I think there's also there'll also be a bit of a renewal in terms of the kind of cryptography we use as people start

thinking a bit more seriously around future proofing things for you know the kind of postquantum World um because we're getting to a point where you know I don't think Corum computers are right around the corner but maybe in the next 5 to 10 years you start to to see things you know get a bit more serious and so that means that around now you maybe have to start thinking a bit more about what you're going to do and that requires thinking about the cryptography um and so that'll push things you know forward on on the cryptography side and and we'll also I think we'll always progress towards cryptography and better cryptography that's more adapted to the problems we have but then when we get newer problems and we don't have cryptography to consult them we'll always then rely on economic mechanisms

and and reasoning about incentives um and it's always useful to reason about incentives because that's what allows you a lot of the time to actually identify what the problem is and allows you to figure out what the cryptography that you need is um so so both will always be around um both will always be useful and and I think both will always actually relate to each other in in some way because of that yeah absolutely that that that sums it up um Alexander thank you so much for coming on um I think this was uh this was this was a great overview and and hopefully uh we reached um a certain amount of builders that are interested in formal verification and participating planning to participate in the program um I certainly learned a lot about formal verification and and how uh

the EF and ethereum is thinking about this when it comes to the ZK rollups and ZK VMS in general so uh yeah really appreciate you coming on man and maybe we'll do this again and hopefully it's not five to 10 years but hopefully we'll do this again when maybe quantum computers around a little bit closer and uh we see we see uh some more formally verified ZK systems out there in the wild yeah I think it'll be uh it'll be fun to see what results we get and and how quickly we can tackle all these problems and then and then yeah we can definitely talk about things again once we once we have some results to show for it awesome thanks man appreciate you coming on Cheers