Episode 396 - lean Ethereum Part 6: Formal Verification with Alex Hicks

Transcript

Welcome to Zero Knowledge. I'm your host, Anna Rose. In this podcast, we will be exploring the latest in zero knowledge research and the decentralized web, as well as new paradigms that promise to change the way we interact and transact online. This week, Nico speaks with Alex Hicks, researcher at the Ethereum Foundation for the sixth and final episode of our lean Ethereum miniseries. In this conversation, they explore the role of formal verification in the lean Ethereum vision and how the ecosystem is working towards machine checked guarantees across the ZK stack from risk 5 ZKVM

circuits and constraint systems all the way down to compilers and cryptographic primitives. for these special episodes. We also have videos over on the YouTube channel. Links are in the show notes in case you want to check it out there. And be sure to subscribe to the channel while you're at it. So, this wraps up our Lean Ethereum miniseries. We would love to hear from you about what you thought about it, if you liked the video format, if you'd like to see us try something else, and especially if you have some ideas for future series we could do. Before we kick off, three quick points. First, ZK Summit is coming back with its 14th edition. Applications to attend are now open. It will be on May 7th in Rome. So, I hope to see you there. Second, ZK Mesh Plus. Our paid

subscription tier is rolling. We have released a few bonus clips over there as well as some of our exclusive research reports. If you want to get access, please join the paid tier. Third, if you're looking for other ways to support the show, we have donation accounts visible in the footer of our website. Support definitely goes a long way. So, if you do decide to donate, thank you in advance. That's all for now. Links are in the show notes. Now, here is Nico's interview with Alex Hicks. Today, I'm here with Alex Hicks, lead of protocol snarkification at the Ethereum Foundation. This is the sixth and final episode of our lean Ethereum minieries and today we'll be talking actually

about lean for the first time amongst you know other things. Alex welcome to the show. >> Thank you for having me. >> Actually this is really funny cuz I met you five six years ago before doing any cryptography before even knowing about cryptography cuz you were teaching at UCL long time ago now. >> Yeah. Yeah. But like this is this is actually where I learned cryptography was like through the lectures and the tuto tutorial classes that you were running. So it's a nice full circle moment to >> and you were you were clearly convinced to some extent that it was interesting stuff. >> I mean I hope so otherwise I'm just really good at lying for the past five six years.

>> Um I was curious actually what was your story into not necessarily cryptography cuz clearly that dates a while back but at least into the Ethereum Foundation and sort of this ZK ecosystem. It was quite a roundabout story in a lot of ways. So I think I got into so originally I studied physics and then math and I was going to do a math PhD. I had an offer to do a math PhD. I'd accepted it. Um and then I kind of felt like kind of math cical physics academia was you know not looking that great in terms of >> job prospects and just vibes in general.

Um and I had always had an interest in I guess kind of privacy and security and and things like this. I think I I used to tour uh before there was a tour browser when you had to use a client called like Vardio or something like this. >> Um uh not for any like bad reasons. I was just getting DD dosed in like an online game and so I installed tour and uh so I'd had an interest in that. I'd never really thought about doing computer science as a degree because I saw it was just writing code which I thought was kind of potentially boring. I was not aware there was a thing as you know theoretical computer science >> uh let alone I guess kind of cryptography or anything like this. Uh and so at that point when I was kind of basically decided not to show up to do a

PhD in mass I thought well maybe actually I know a bit more about all of this stuff now uh I can see there's a lot of issues with privacy and whatn not obviously you had the uh the investory powers act in UK that was kind of showing up at the time uh and so I thought you know maybe this is something I should get into uh by basically pure luck I did actually find people who wanted to take me on as a PhD student to do stuff related to this and so I ended up pivoting into computer science and kind of information security more broadly. Uh I actually didn't pursue cryptography when I did this because I read a lot of cryptography papers when I started my PhD uh specifically around functional encryption and this was this

kind of no background. I said like okay the math kind of makes sense. I can kind of see like this seems really cool. You could do you know arbitrary operations of encrypted data sounds great. And then someone explained to me that you know IO was basically not a thing and that when cryptographers meant efficient they meant runs in like polinomial time was horrible constants >> and I was like okay this seems kind of you know >> maybe less practical than not a lie but like I thought you know if I'm going from like spherical physics to computer science like I want to do something like practical if I'm just going to do math I can you know I could have just you know stayed there and done that. Um and so so my actual PhD was um >> was around actually kind of transparency uh transparency enhancing technologies

you could call it. So basically logging mechanisms that have some cryptography uh that you would use to provide more transparency for you know systems that we use. Um blockchains obviously figure into this uh because they do basically function as big transparency logs in the same way as you know certificate transparency might be another example and at that time at GCL there was obviously just a lot of people doing blockchain related research uh a lot of them are actually still around obviously I was in an office with Mustafa who did Celestia uh Anna who did Nim Mary Malo who was the lead of the cryptography team for a long time at the EF Sarah Zuvie who was at Protocol Labs uh obviously George Dessis did chain space and then is now chief scientist at three like there's a lot of people who doing

blockchain stuff. So I naturally found myself doing blockchain related research and so I wrote my first paper related to Ethereum in 2017 which was about uh uncle blocks and the way they basically subsidized sudden attacks on on Ethereum. Uh so that was a long time ago and so did did all of this uh so that was kind of neither really cryptography uh nor form verification uh in a lot of ways. Uh there was a bit of cryptography which was you know kind of understanding some of the cryptography but obviously not writing papers about new cryptography. Um but then around the time I was finishing my PhD I thought I wanted to do something a bit more massy again. uh and I'd done a bit of formification in between actually my

masters and my PhD because uh there was a guy in Cambridge called Lawrence Pollson who was the creator of Isabelle which is a proof assistant and he used to basically take on mastery students for a couple months after their masters to have them do mathematics in Isabelle and and get kind of feedback about essentially the UX of doing yeah math in Isabelle. Um and so around the time I was finishing my PhD, there was a lot going on with respect to lean. It was started to kind of get some attention. They had started to do basically interesting mathematics um in lean, which is something that's usually quite hard to do in proof of assistance because you need to build up a lot of libraries to get to anything that's relatively modern and not just redo set the or category for the tens, thousand times. Uh and so I got into lean

basically around the time that I was finishing my PhD. I was doing a bit of I was doing some lean. And I was getting a bit more into the ZK stuff because similarly I think it started to become a bit more practical and interesting in that sense. >> Uh and then I was also just procrastinating a lot with prediction markets. Uh which I'm not which I don't have time to do anymore as Yeah. Um and uh so I was doing that. I was interested in like the AI stuff related to lean was maybe like very early on where it was kind of not as popular as it is now. you had a sense that okay clearly if people are going to generate a lot of things with AI then a proof assistant that checks you know your results is kind of nice and there's an obvious kind of

synergy there and so yeah Justin posted this tweet that was like if you love AI in Ethereum like send an email to this email address um and so I sent an email that said like I'm kind of quite interested in the AI stuff especially with respect to proof assistance and form verification and you know what that could mean in terms of security and guarantees about the code and all of this >> um It turns out that when Justin posted a tweet saying, "If you love AI and assume, send me an email." What he meant was, "We're looking for someone to lead a form verification project." Um, um and >> you're right on the money with your response.

>> So, so I think I think I probably locked out to some extent that like maybe not a lot of people mentioned forification in the email about like their interest in AI in Ethereum. And then yeah, I heard that basically kind of uh yeah, Justin and I guess Vitalic, you know, had kind of dreamed up this idea of obviously with all of the ZK, you had all of the L2s already. Of course, you had ZKVMs, which were barely starting, you know, at the time in kind of 2024, which was zero. Um, you know, clearly things were trending in that direction, which was great, which was, I guess, had been the goal and the road map for a couple years, but it was becoming practical.

There were clearly a lot of issues with the reliability and the security of the software. Um obviously maybe issues with this is brand new cryptography that you're going from you know paper to implementation to production in not a lot of time and you you know you want to feel confident about like what you're doing um and so and so they thought well why don't we basically put in a lot of resources into formification why don't we obviously have this kind of bets that AI is going to turn out to be um useful for this uh and so so I basically found myself uh joining DF in June 2024 uh to basically lead lead that effort uh with obviously as Justin said on his episode quite a big budget and a lot of resources and I guess with the aim of

trying to involve you know all of the teams who are actually doing foration in the ecosystem into this and making it a bit of a community effort and and obviously we've seen even security zk security now we're doing stuff in lean >> um I guess you know partially as a result of that uh and so so that was kind of the idea was you know can we formally verify this stuff can we get people you know to buy in and to commit to to doing this as a community effort where we stop what we've done we're making more efficient use of all the different teams and the different skill sets and uh and can we actually like cover the whole stack of CKVMs which is quite a big stack and it's it's not huge >> it's not obvious that you could actually you know cover everything um but we've

been yeah we've been making progress for the last kind of year and a half on this >> uh which I guess is what we're we're here to talk about now >> exactly that's what we're here to talk about and also to kind of understand what is formal verification because you've mentioned it a few times now. uh you've also talked about like theorem solvers or proof assistants I think you said what are all these things how do they differ >> yeah uh yeah so this is always the the important question is what are you actually doing >> um so I think there there's a there's a generic answer to formification which is basically to produce a machine checkable proof of something of some statement and the statement here could be like a mathematical serum the statement is

basically always a serum and then whether you define that a mathematical serum in the sense that it's from a math textbook or you know something about you know some software or or something else you you have a statement and you have a proof of it uh there are different ways of obtaining these proofs some of these are proof assistants like lean or rock or Isabel or hall four and there's a wide there's a whole kind of family of these which have different logical foundations and different underlying type series and then you have things like SMT solvers um which are a bit different in the sense that SMT solvers are fully automated. You don't need to write proofs by hand in the way that you do in proof assistance. Um, but they maybe have weaker guarantees in the sense that for performance reasons, they tend to be uh implemented in C++. And so

you can have bugs in SMT solvers. Um, and you will typically there are like there was aises from someone with ETH Zurich a couple years ago that found like 300 or 3,000 bugs in in some of the SMT solvers. And these are mostly like edge cases. I'm not aware of like anything that was verified with SMT solvers that turn out to be like wrong because of a soundness error typically because what you verify you have some confidence that it's correct in the first place, right? Um but uh and so you have a lot of these trade-offs of you know how how good are the soundest guarantees that you have. Uh and this varies even among proof assistants. So different proof assistants the way that they work is that you have a statement written in obviously a high level language that you can write and read as

a human. So this is like code essentially >> it it is code. Yeah. So a serum you know a serum in lean or proof assistant is actual code. Um you have I guess the the some people will see hear about the kind of curry Howard's uh thing which is that you have propositions are a type and then programs are proof which is basically an implementation of that type. Uh so your your your proofs are actual you know your sums and proofs are actual code in in your proof assistant and this basically gets compiled down to a kernel language and then the kernel of a proof assistant is basically the core logic uh of that proof assistant against which everything is verified. And so um you basically want this to be as small

as possible. And I think for some of for I think for Isabel and and all four which are based on just higher order logic which is obviously a much simpler logic the kernels are actually very short like hundreds of lines not a lot at all and everything gets you know checked against that. So you have quite a high degree of assurance that like you know there's no bugs in in there no soundness issues. Um for things like rock and for things like lean which are based on um on kind of you have dependent types you have the kind of whole calculus of constructions. Um the kernels they're a bit more complicated. So maybe you're a bit less certain that like there aren't any soundness bugs. Um I'm not aware of kind of importance down of bugs that have taken place but there are like tricky ways that you can prove

you know you can prove false you know with with some tricks sometimes or something like this right okay and actually so your colleague Yoi actually had a bug bounty to prove false in rock you know many years ago which was due to um I think polard inconsistency I guess is uh the reason which is you could get it you could do some tricks to get it to print false basically >> even though you're trying to prove something that's non false like you're always trying to prove True, right? >> Yeah. Um, >> okay. >> So, if you prove false, you have an inconsistency, right? Um, and that that's an issue. So, there is always, you know, where you're doing an SMT solver and there's like some C++ code base which is kind of trusted and, you know, for things like Z3, the code base is like maybe like hundreds of thousands

of lines of code. So, it's it is there's quite a bit to trust. Um but and then even for proof assistance you have obviously the actual kernel uh that you you need to trust and and there are efforts to um basically check the kernel you know with itself. So you have like lean for lean and you have like metop like a recursive proof of the kernel >> with compilers you there's a basic test of like can the compiler compile itself right >> okay >> um and you can kind of think of it at the same time as the same thing you know like can you can the kind of kind of the kernel kind of check its own consistency and so there are efforts to do this um but they're not they're not complete in any sense they're quite far from complete in many ways um but obviously

empirically you know we're not aware of like big soundness issues Um but it but it is you know there's always like a small probability that you know there is a bug somewhere in the kernel and then you can do you can do client diversity right so you have for lean you have different implementations of the lean kernel so there's one in lean there's one in C++ there's one in rust maybe there are more you could run you know you could run your proofs against you know different implementations of the kernel and uh and maybe get high assurance that way as long as the logical foundations are not uh are not completely flawed which is I see not many people kind of dive dive deep enough into the logical foundations of all these proof assistants uh it's maybe like five you know a handful of people certainly not at least I you know

I can't claim to have you know fully understood the lean kernel and uh not a lot of people can for lean there's maybe like one or two people um >> Mario Kro and maybe that's that's probably about it um but it's but it's still a reasonable >> that's a bit worrying yeah >> well yes and no I mean it's a small it's not a big amount of code relatively speaking right so it's still like it is some trusted code, but it's some trusted code that everyone relies on. And so if someone does notice that they've proved false for something that obviously shouldn't be is going to get flagged because every lean user depends on on that same kernel. Um and uh and you do have obviously people who do commit a lot of time to look at at it.

>> So in some way everyone acts as a canary for like bugs in the kernel. >> Yeah. Yeah. So, so we would we would obviously notice, you know, when we're formalizing a bunch of coding theory to prove things about Freud, you know, we kind of have a sense of like we expect this to be true and we expect other things to be false and if we accidentally, you know, prove something that we sort of like this isn't right, we we would notice it because we have some other form of grant truth which is the papers and and some sense that what we want to prove is is correct. Otherwise, we wouldn't be trying to prove it in the first place. So actually this takes me to an a good question which is what do the the theorems look like? You said like we formulate the

theorem and we prove it. What do they look like and how why are people saying like oh I formally verified my rust codebase like what does that mean? >> Yeah. Yeah. So the the serums look I I think quite close to serums on paper. You have a you know you have declaration which is just like lema or serum and then you some serum name. And so you could have you know like a basic example would be you have you know like lema add com to say that like addition is commutative over the integers and then you would just declare uh you know two variables a and b declare them as type natural number uh and then you would and then the the statement itself would then be a proposition which is that a plus b equals b plus a >> and then you would have a proof by steps

in the proof. Um, so it can be quite readable. Um, especially some notation gets kind of ugly, but in the same way that some math notation gets kind of ugly and hard to read and it also kind of looks like code because you you know you're declaring variables, you're introducing variables, you can introduce obviously um assumptions or hypothesis >> much in the same way you on paper. And so I think if you you know if you if you forced yourself on paper to really say like this is these are the variables and this is their types or on paper you might use you know maybe sets rather than types as conventions go. Uh and then you would declare you know like these are my assumptions assumption one assumption two assumptions three like it looks kind of similar to this with some syntax that depends on you know the

proof assistant. Um and then and then the proof is basically a series of steps. uh which again is I think if you do like an introduction to proofs in like a mass undergrad course looks familiar right when you're you're forced to do like okay I use this aum for this and this action for that and then whatever it looks very similar to this and you can see if you put a lean repository in VS code you have like an info view and it tells you at every step in the proof what the current proof goal is and so you essentially basically start with the statement that you're trying to prove and then you you know each step changes the goal until you hit something that is basically you know kind of obvious Trivally true and and that completes the proof and so you can >> one of the nice things about this is

that this kind of reposition as a proof as code is that obviously um a lot of software practices can kick in which is one that obviously you need to like maintain and debug and things like this. Um but also you can refactor and you can optimize and you can make the proof shorter or something like this. uh you can make the privacy depend on different assumptions or use different lemurs >> or more general I guess if you had for specific types and you realize >> exactly and more general helps because more general gives you maybe better automation uh it lets you reuse you know more more things >> can you give us an example of where we do formal verification for code because at this point we were talking about like a basic math property so addition commutes >> how does this translate to verifying

code >> yeah so so when you want to verify code then your your main responsibility actually I more so than doing the proof itself is to figure out what is the actual statement that you want to prove about your code. >> Yeah. >> Um and this can be sometimes this is not too bad. So sometimes you might have you might have a specification for a function that's written in lean uh and that you might have proved something about it in lean or or not and then you have some code in another language um or maybe in lean itself it maybe it's like an optimized you know kind of version of the function um and you're going to bring that into lean. I'll say a bit about how you bring stuff into lean in a second. Yeah.

>> And then you can write assume this the form you know like the spec returns the same outputs on every input as the code or vice versa like the spec implies the code and you can write some some equivalent statement between you know what you're trying to prove against your spec. >> So always comparing code to a spec. >> Well that that's so that's one way of doing it because then you're reducing to like a nice boolean right which is like if spec then code. So something along these lines. And so this this is kind of nice. Um, and this is you can kind of see how that looks like as a serum like if a then b. Um, so it's not too different. This the trick there is obviously you have to get the spec right. If you get the spec wrong, you're in no man's sand. So the specking part

is very important. Uh, more important than writing the proof in a lot of ways. Um, and then there are other things you might want to prove about your code. So you might you know for cryptography or or you know for some cryptography you might want to prove that the code runs in constant time or you might want to prove panic freedom about it or properties of these things which are like much further removed from maybe mathematical properties of the functions that you're interested in implementing in your code and much closer to the behavior of the code um generally speaking and there I think it's it's kind of interesting because then you have another element of trust that comes in which is that you want usually to extract code that's not written in your proof assistant into your proof

assistant and so you have to translate that code >> and because obviously most languages that people use whether that's thrust or C++ python go you know whatever um most of these don't have formal semantics for C for example there is formal semantics for C99 specifically what you mean by formal semantics >> well definfined behavior uh of every part of the language um >> okay >> so there so the semantics Maybe obviously maybe semantics is kind of >> different depending on what you're doing. It's like not a word that like gets used a lot but the semantics are kind of the meanings of of the code. So if you have like a function and you're thinking like what are the semantics of this function is the semantics should be like what does it do? um basically and then how you implement it is basically

you want to check that the implementation produces behavior that matches those semantics otherwise you have you have a bug or you have undefined behavior and then you can't reason about uh about what it's going to do. So when you're extracting code or translating code from any of these languages that people actually use for software development into lean because these don't have formal semantics that you can use as a reference. You can't really do proofs of this ROS code translated to lean is you know actually the same as this ROS code with some some kind of equence relation. You you don't you're not able to do this because you don't have like a reference for like what are the formal semantics for for the R code.

>> So that that's kind of trusted. Um and so you have you can do a lot of testing obviously uh you can do a lot of you know kind of get smart people in the room who understand both languages very well and get things like if you have both of these things you know like their behavior is going to be the same >> or you can write the spec I guess. Yeah, you have to kind of but basically what you end up doing you kind of do semantics for like a subset of Rust and for example you know if you're doing purely functional Rust that's much easier to deal with and to reason about than if you're doing very imperative Rust that might have a lot of side effects like if you have you know mutable borrows if you want to if you have code that returns a mutable borrow

that's kind of hard to like reason about and it's kind of hard to map this like how do you you know do this in lean in a way that kind of makes sense and so all of the tools that we have to translate from some language to lean um and we have some for rust there's an inas there's you know hacks uh there there were others which translate also rust like some SMT uh silver representation you'll see the word high assurance used sometimes instead of form verification which is a much better term because it it kind of translates a bit more that you know there's a level of assurance which is high based on testing and auditing and people using it but but there's no there's no proof of that translation right >> and so what you have instead is you have a proof in lean that the way that you've

modeled your Rust code in lean, you can show something about your Rust code. Um, and so you're trusting the model of that Rust code and then you're trusting the Rust compiler and all of this, you know, that that goes on after. Um, now so that's that's quite a big obviously trusting the Rust compiler and LLVM and all of this is quite a big trusted computing base. >> Yeah, but it's a lot of us relying on it, right? So >> and there are bugs in LVM, right? I mean there was one very funny bug which was someone had an instance for some reason uh once all of their code ended in NLBM IR they had a function which was like f ofx= x - 4 and it had actually just been rewritten for like f ofx= 4 um >> and so you can kind of imagine if you

have this that might happen to like your constraints or something like this. Yeah. Yeah. Yeah. >> That's good. >> Sure. Everything passes confus. >> Yeah. You're going to have some surprise. Um and so so there's this kind of trusted codebase and understanding the boundaries of where your formification begins and ends is really important. Um, in the same way that obviously if you have code in libraries, you might have a library that has like tens of thousands of lines and you might have some core functions which are formally verified and then the rest is not and so you can still have bugs and it's >> ideally you want people to like document things. Well, >> typically if you have a codebase with 10 20,000 lives of lines of code let's say but a lot of those are tests you don't need to formally verify the tests right

you can just stick to the core functionality. >> Yeah, that makes sense. Um but then but then you can always keep going you can always chip away and go further right so you can always think about okay like do you want to formally verify a compiler and you have there is a formally verified C compiler called comsert >> which was this insane borderline inhuman effort that took place in like 2008 you know around these times however many poss you know spent their you know their years on this but there is a formally verified compiler for C um and again there's a boundary the front end to that is not formally verified is just you know once you're in the compiler and basically every pass in the compiler is formally verified you have a proof for every pass every rewrite every

optimization pass all of that is is basically proven against a C99 specification so you trust the C99 spec but obviously the spec is you know like much smaller than the compiler codebase and then you you trust the uh a camel compiler which compiles your camel code in which comfort is written um >> but then obviously maybe a camel as a compiler is like more trustworthy than you know than C >> or smaller or easier to look at. So this notion of boundaries actually helpful, right? Because we keep pushing further like >> what's the latest thing that I trusted and yeah, >> you keep you keep pushing further every time and you you want to keep track. So it's important to kind of really document and keep track of like >> within your entire stack like what are

you assuming is secure like what are your compiler tool chains what optimization because with LVM you have you know like 01 O2 or like different levels of optimizations that you can apply and it might be that you you might trust 01 you might trust O2 or 03 less you know you might trust a specific version of LLVM or something because there there are there are instances of some code that used to be constant time written in C or something and they've put a lot of it into making it constant time then someone updates clank and they added like a smart optimization pass that makes your code not con not not constant time so these are things that come up right and and one of the challenges is that you want to keep track of your boundaries and you want to keep track of how your boundaries change

or stay the same over time because obviously if you're doing you want to verify some Rust code in lean rust is still changing the Rust compiler is still changing and lean is still changing >> um and so you that you do want to make sure that you have like pretty solid basically engineering practices um that to maintain all of all of whatever level of insurance you claim to have uh because the whole stack is is always moving. Um and a lot of this is actually kind of dumb in a lot of ways. Um >> do you say dumb or dumb? >> Dumb. Um >> okay. Yeah.

>> No, far from dumb unfortunately. Yeah, >> but it's an interesting thing which is also like why do we have all of these boundaries that are there that we can't have to keep track of which are all moving in different directions independently maintained by different people which makes this inherently hard as a result. The nice thing would be well why don't we just write code that is correct by construction or something like this right and I think this is something that for a long time is you'll see people mention about you'll see it in academic papers you'll see prototypes you know like here's you know if you want to do like a small purely functional language and you want to build a compiler just for that with the intent of making it easy for me to verify like that's it's kind of doable you'll see people have done this as you

know their PhD or uh you know just one paper or something what's what's harder is like getting something that's like as fast as rough or C++ and heavily optimized for different hardware architectures and different backends and you know and and getting and implementing you know like reasonably complicated algorithms where you can have bugs in the code you can have bugs in the spec right like plunky street had a bug which was in the spec uh when it wasn't doing the final degree check for fry for the fry verifier >> oops and so but it's a noob so this is again like in a large enough library you have empirical studies of like where if you're given like a thousand lines of codes regardless of the language you have somewhere between 1 and 50 bucks depending on the quality of the code like one bug for thousand lines of codes

is considered like state-of-the-art you can put it in like a fighter jet or something like this. >> Um and so if you have like tens of thousands of lines like statistically you know there were bugs basically. >> Um and the same applies for specs. If you have tens of thousands of lines of specs and it's still someone writing them like they're easier to read, you know, than optimized codes of course and it's like you might have like a reference on paper but it's still tens of thousands of lines and you can have human error and things like this and you have you know you know in the context of ZKVMs for example is one of the nice things here about risk 5 is that the risk five spec is quite short. Um if you just look at like some of the ARM specs they're like above a 100,000 lines of

specs. um which is like you know you can have issues right and and they're evolving right >> based on the previous math actually you're bringing us perfectly into what I want to talk about which is formal verification of the lean Ethereum stack right >> um what what is being formally verified what falls within the boundary what is out of it >> tell us a bit more >> uh yeah so this is yeah it's a good it's a good kind of segue into this because obviously it's one part it's one thing where we do need to track what the boundaries are and what we're actually doing and what we're trusting. Um so a lot of the focus right now I guess is whil obviously lean VM and all of this which I guess would have been on previous episodes that haven't been

>> released yet uh but um but will be soon I'm sure um at least at the time that we're recording then you know lean VM is not in production yet. So right now for example we're not formally verifying anything about lean VM specifically. So we're very focused on these risk 5 ZKVMs. >> So you know kind of SP1, OpenVM, Airbender, ZISK J. >> So this is all like the execution layer stuff. >> Yeah, the execution layer the stuff that's like on these proofs basically. Um and and here we're doing we're we're trying to cover different parts of the stack basically in parallel. Um so if you go from the ground up on the side of the actual like ZKVM and specifically the like rest five component of the VM.

So here what we've done is we've extracted the official uh specification for thrive which is written in a language called sale. Uh we've basically now have a lean backend for sale. So sale can can emit lean code and so we have the we have the entire risk spec and actually other specs that are in sale which includes I think some ARM and some x86 and things like this but for we have the entire risk spec that can it be extracted into lean. So that includes every extension. So whatever extensions people want to use in the future we have specs and therefore we see specs what we can do is we can then actually >> is that back end part of the boundary or is this something >> that back end is part of the boundary.

Yes. >> Okay. >> Because again like the spec obviously for S5 is kind of there is some basic checking there's some like you can apply some SMT solvers in sale or in lean you can write like some lemurs that like um you know this function that's going to take like you know a ve bit vector of like this lens is going to like just take a bit bit vector of this lens and nothing else. You can do basic sanity checks like this, but obviously the spec is whatever the risk 5 foundation decides it is. And then the implementation of that spec is whatever the people working on the spec in Cambridge and sale have implemented it as and then and then the back end for that is you know again like a you know a mapping from basically sale to to lean.

Now luckily I think the two languages are like not too um dissimilar in like the underlying logic that it's I I feel pretty happy and confident with it and then it passes you know there's a test suite and you can pass you know the official test suite and things like this um but it is but it is that part is trusted and but there's an interesting discussion right which is like is this is it better to trust this back end or would it be better to trust like a handwritten risk um and so actually what we have is we have a handwritten risk which is nice >> uh which is nicer because it's bit blastable uh which kind of helps with verification and we've shown it equivalent to the extractor sales spec.

>> So we have some sanity check here that we have an extractor spec and a handwritten one and they're both equivalent. So those proofs cover the pure instructions the instructions that have side effects like of the load and store and things like this. So with this spec uh which we which we're trusting you know to some extent then obviously what we're able to do is then we're able to get the constraints for the ZKVM risk 5 circuits and we're able to verify these constraints against the wrist 5 spec. >> I see. And how are the constraints map mapped into lean? Uh the constraints are mapped into lean. Uh currently mainly you pass them off of the a from the source language in which they're written and then and then you basically print that back to lean >> and again part of the boundary or not

>> part of the boundary. Yeah. Exactly. Um because obviously you know if you take someone might have written their circuit with plunky street or some other rust DSL and obviously again you hit this if you don't have formal semantics for rust you suddenly no formal semantics for like those DSLs. Um and so you just read off values from from the a um now luckily this doesn't feel horrific right uh one because obviously this is uh the a is still reasonably high level not much has been done you know to these constraints >> by the way the is kind of like almost like a binary of what the constraints are or >> uh so the the is kind of once you take your high level code and then you try to represent it as a uh basically as a tree

operations. uh that that's the a and so if you have like a loop or something you know you might have all the different values of >> of the loop and so so that gets extracted and so it looks kind of buggy actually that's the main thing um the the main thing is it's hard to the constraints are like kind of ugly um and I'll I'll I'll say in a second how we can do this better okay >> we've got this boundary so we extract the constraints into lean and then so we have a bunch of extracted constraints into lean which we're trusting match those that are generated by the rust code uh when you do actually run it through your normal you know compiler and and you deploy it in production. Um, and you can you can kind of check this if you want, right? Which is that you

could actually run your regular things through the Rust compiler as usual and just check that the constraints are the same. So that this you can kind of test actually fairly well. And because the constraints are not something that has like they don't have like an insane amount of churn, like it feels pretty reliable that like you're not no one is doing like a commit to the constraints every day where you need to like retest this and so on. So that that feels like it feels kind of okay. Um and then the proofs that you do is you have proofs that are basically of the form that you know the spec implies the constraints and that the constraints imply the spec. And so you show that obviously the uh one that the constraints are satisfiable. Um so you are going to be able to generate a witness uh and two

obviously see that the constraints are sound in a sense that obviously they don't allow um they can't be satisfied by multiple uh different witnesses. >> Do we also need to check that this witness actually satisfies the lean spec or like sorry not the lean spec the respect. Yeah. The problem is with this is that the ZKVM teams have been hard at work optimizing the witness generation so there's not a performance bottleneck and so whilst you could in principle have circuit DSLs where the witness generation and the constraints are coupled and you'll see this in circum for example or even actually with spunky street right >> but in practice people don't do this in production they have completely decoupled witness generation from the constraints and so when we're extracting constraints we're not extracting the

witness generation logic and so we're only showing completist in the sense that like they are satisfiable. We're not showing that the witness generation that the ZKVMs actually run produces a witness that always satisfies these constraints. >> Interesting. >> We are trying to resolve this. So you have all these boundaries basically. So you have these proofs in risk 5 and you can find like detailed reports. There was one done for the the open VM 5 constraints. The work to verify this was finished um earlier this month. there's a very detailed report in a repository there which maybe if there's thrown out or something we can put it there that goes into like detail and you can see that the proofs and so this all feels solid but again you have boundaries right >> and so there's an interesting question like well how can we improve on this um

because one goal with all of this formation stuff is not just to do it once it's also to try to make it actually like kind of easy to do and economically sustainable and not cost like a ton of money um and so there were two things one is you could just write your constraints in lean And obviously uh you have DSLs like clean OCK lean which are doing this right uh and this actually turns out to work reasonably well uh you can you know lean is a good functional programming language so you can write you can write these kind of things and then the proofs uh if you've written your constraints in lean are much much nicer by a factor of 10 to 100x I would say wow >> I mean one of the first uh examples that was in in clean was obviously like a

catch pre-ompile >> and in the proof there soundness and completeness of each permutation like 10 lines each and then uh a proof for the you know composed you know full round is like 70 lines for sounders 70 lines for completeness um so that's actually pretty good right and that's a reasonably optimized catchback pre-ompile this I don't know if it's as optimized as the PL3 one whatever >> but but that's really good compared to the planky 3 catch where actually extracting those constraints into lean doesn't work because if you put the constraints in a file is about 1.4 4 GB and if you try to open a 1.4 GB file in VS Code, it crashes. Um and so we did actually verify the plunky street ketch

in rock. And the way that this was done um by formuland was that they actually basically extracted the Ross code from uh Plunky Street to rock and then they basically checked that that was generating the exact same constraints as the Rust code would on its own. And then that obviously let them do basically proofs about like the functions and the high level description on the program itself in the same way that you might do in lean with with a lean DSL um rather than trying to extract all of the constraints you know in one and do this. So there's a lot you can do for proof ergonomics and for the proofs to be easier um to do and obviously it's easier to maintain because proof this another kind of maybe dark secret is

like proofs break not in the sense that like they're not sound and like the soundness is compromised >> but in the sense that you have like a bump to like the version of lean or something and then there's a dependency in massive where like someone tweaks the definition of something in massive and then it breaks your proof and then you have you just fix the proof it's not a big deal. Actually, this is a good point. Is there like an ecosystem of interdependent proofs? Cuz obviously, if I'm using basic math theorems, I'm going to use it from someone else, right? I'm not going to write it from scratch. >> So, is there like a canonical math library that everyone uses?

>> Yes. So, there there's this big library called Maslib, which has at least like two years ago, it was well over a million lines of code. Uh, and codes there being just like mass mass with statements and proofs. So by now it's probably like a couple million. >> It's fair to say that it roughly covers all of undergrad mass that you would ever need. So it's fairly extensive. >> Okay. And so if this changes then every proof you've written needs to be changed or you need to like somehow bump it up. >> Uh not every proof but like every now and then you get I mean sometimes someone changes like a file pass. So at some point a couple months ago they moved a bunch of serums about matrices from like one file pass to another and so that broke a bunch of our proofs. Um

but it's just you change the import and it's and it fixes itself and then you have other things like someone might change a definition you know things like this um and then you just have to like fix your proof and so it's not that the proofs are not sound it's just that you know there's churn in the libraries and in dependencies and you kind of address them. The nice thing is obviously when your proofs break it's very precise you have like within a proof you might have a 100 lines or whatever one line goes red and you know exactly where it breaks and you fix it. So it's that's it's kind of okay but it's an interesting thing that like you have to know that it's because it's code you have to maintain it right um or you can obviously you can leave a repository you know tanked for

like a version of lean and not bump it to newer versions of leans and and then it would break right if the code is static and the dependencies are static it's >> it's fine um but it but it is a sync like and so if you want to kind of keep maintaining proof of software that is you know whether that's constraints or some other kind of software where there is churn in the software and And you want to also maybe keep up with new versions of leans because you get better automation and other like maybe helpful lemas get added to mass lil that like solve your problem or just other features get added to lean which solve your problem which actually does happen quite a lot luckily for us. >> Um then you know there is a bit of churn and maintenance and it might take like

you know 30 minutes a month or an hour of months you know where you fix like a couple proofs uh it's it's a good way to understand proofs that you haven't written if you're responsible for maintaining them I guess. Um but that so you you kind of have some churn but it's okay. It's not it's not the worst and it's not a soundness issue in any sense. the the biggest soundness issues tend to be if you've like verified some code you know at a specific commit hash you know in the source repository of the code and then obviously if you change the code and you haven't you know done a new proof or something and that's something that I think is maybe more concerning because >> um a kind of a practical limitation which is which is kind of annoying is you you don't really have like something

in CI that extracts your constraints back to lean and then runs all the proofs again and verifies that the proofs are still fine one because um obviously kind of running the extraction and then building the lean file in CI can be kind of long and you know might not work out in in terms of just length and resource allocation in CI and two because it depends on like how robust the proofs are to changes. So if you have a proof which is extremely manual um where the proof is extremely if you want kind of tailored to that specific constraint then if you change it a bit it might break it will it won't break in like drastic ways like the constraints will still look the same >> but you still have to go into the proof and change it and >> you have to go in and change it and it

and it's and it's and it's kind of annoying but you have proofs which are increasingly automated. So you have decision procedures for like statements about polomials over finite fields right and then if you have if the proof goes through some automation then actually the proof might actually hold up the changes in constraints um and so increasingly we're seeing more robustness in the proofs and we're obly working to have more robustness in the proofs so that they don't break as much actually automation is a good point and one of the last things I wanted to talk about you mentioned earlier an inhuman effort which made me think a yes inhuman efforts actually we're at a point where in human efforts are probably really good. How is AI and LLM participating in all this like proof systems kind of stuff? Uh yeah. Well, so as of recently

they're parting a lot. Um they we're probably fairly close to it. I mean >> there there's two things. So there's one thing which is that um a like so AI I think for people who are doing things around AI and formification or people in formation who are looking at AI there's always an obvious synergy which is AI is basically good at producing large amounts of outputs and proof assistants or SMT solvers or any kind of you know thing that checks that is machine some machine checked you know process are very good at handling large amounts of outputs and telling you if they satisfy some kind of property. Um, and so there was always a sense that well, you know, if you are going to have these otherwise unreliable models that can output things that look like plausible proofs of

statements or things that, you know, codes that you might trust or not want to trust, um, why don't you just put that into your proof assistant and then the proof assistant will tell you if you can trust it or not. And if you don't trust it, you just rerun the thing until you get some output that satisfies it. Uh, and that seems like a nice thing. It took a bit of time to like materialize. Um, but but it's kind of it's kind of there for some things, right? So for proofs in particular it is basically there. Um so the very first episode was Justin you know he mentioned it in January you know I launched um a proof run with using like a specialized model developed by logical intelligence um which is specialized you know kind of mathematics and software verification and things like this and in particular

basically can be stable for like multiple hours and so that took 8 hours and it proved polish spielman the form that appears in the proximity gaps paper in 8 hours at a cost of $200 in compute which is really nice because I think by comparison If you gave that to a human expert which is familiar with the coding theory as is defined in arib and you know the proof itself they would take at least a couple like they would take a couple hours but they would cost suddenly more than $200 because they might change they might charge more like $200 an hour and take a couple hours if not maybe a day or two or something you know may maybe less maybe more like there's different kind of different levels of expertise and competence but but there was a bottleneck which is kind of human time

to do all of these things like even if a lot of these things were you know felt very doable and we had high confidence were doable there was a bottleneck which is there's just a lot to do so you know to do to to get kind of formally verified specs for fry that is like an executable fry protocol where we show that you know you have a statement in the paper which is like this construction has like some soundness property and we want that to be in lean in the form that when we say this construction satisfies soundness that construction is an actual executable piece of code it's not like an abstract function.

>> Um but that required us obviously to one write the specs which took quite a bit of time. We had to do a lot of abstractions for like Oracle frameworks and things like this which which Guang was working on but also we we had to do actually coding theory from scratch because mass lied basically linear algebra and everything you need but it didn't have any coding theory beyond like coming distances and and so that that's a lot of work because it's it's just a lot of material and so we were able to get you know all of the statements written down and we had some of them actually you know definitely had like some issues some of them were stated but like too general artic structures or you know typos and things like uh as you would expect. Uh but but now the nice thing is obviously we made a

conscious bet to like basically not prove everything as we went along so that we could go faster and like getting to getting a f and on the assumption that like proofs would just get easier either with better automation and lean or with AI and things like this and then it's kind of worked out because now actually we have all these statements we actually have a spec for Freud and then we have like AIs which are able to do like hard serums you know like polish spe um which is which is really cool but also for a lot of simpler serums we've had a lot of firsttime contributors who open PRs and who have like a proof of you know some statement or a couple of statements. Um a lot of these are increasingly AI assisted. Um we even have like we have some AI in like the

way that we manage the library. So like I have a script that scans for like missing proofs in the library and then opens GitHub issues and documents them you know with like the proof from the reference paper that that thing is taken of. And so we've had a lot of people who've kind of opened PR and say well I followed the outline proof in like this issue and I used like you know claude or you know codeex or whatever and like here's the proof and then >> and if it verifies then we're happy >> and and if it if they haven't changed the statement I just need to check that it builds and I I just merge it. So that's kind of nice. >> Definitely from our side we've seen Claude getting much much better at doing this and yeah my colleagues have been having a lot of fun yeah

>> proving things in lean from papers like >> Yeah. Yeah. And so that's really cool because it really takes away one part of the job. The part of writing specs is still, you know, it's not solved or you're not letting an AI like do this automotimously. It it's still the most important. It's where you can get it wrong, especially for things where like the specs can feel a bit arbitrary where, you know, for things like cryptography or pro cryptography that has like provable security. You know, if you write down a protocol and then you prove something about it, you at least have a sense of like if you did actually run some if you run this or if you verified something against it, you know, maybe I don't know, it happens like it's not actually fry, but it's still a secure protocol. So maybe you've

discovered something new, which is fine. Whereas obviously if you're doing like a hash function or you're doing like fetch from here and you have like a spec but you can't really prove that it's like you know good in some in any sense then then obviously you know you want to have some oversight on checking that this actually is like what you want expect it to be. >> Um and so so there there's still a lot to work on like yeah doing specs and writing specs and getting better abstractions and still actually like library management is something that obviously you know takes time and and effort to do correctly. Um but but the proof part of it now feels kind of solved. Uh which is which is extremely exciting.

>> So it sounds like you made the right bet. >> It sounds like you made the right bet and it's been one of the nice things as well is because the proof part which previously would obviously be quite tedious because sometimes it feels kind of pointless like why are you proving >> in a proof assistant something that's been proven on paper you know like years ago that everyone feels fine that's been you know whatever. Um and it can be a bit of a bottleneck as well in trying to get people to buy into like doing things in a proof assistant. So we've been thinking like how do we get cryptographers to just like implement their new cryptography directly in lean so that we don't need to like go through the whole deal of having to formalize it and translate it and everything. And I would say that like a year uh a year and

a half ago 2 years ago it'd be very hard to kind of convince anyone to like pick up lean for that purpose. But now cuz we're able to say you know like you know if you just write the statements down which is a much easier thing to do than obviously doing the proofs. Yeah, we had a very fun example of this recently which is that we have we have like a spec for like a single round of sum check in our lilib >> um and we're working on making it executable. We have like a computable polinomal library um which makes it executable but it's not it's not like the full protocol as you would run it. Um and we had uh Andrew Zaitek who is a research engineer in Alexandro Kes group at UPFL who's worked on some check who's implemented it in Rust and things like

this >> started kind of looking you know at lean a bit and he was and got into the idea of trying to write like an executable sum protocol in lean you know as a general kind of functional program um and I had a chat with him in December I think he'd also been looking at it already he talked to Kuang before that and then And but you know it hadn't it wasn't done at that point and in January I get a message like oh okay I have it here here's the repository there's a some tech protocol you can run it you know um it's it's computable it uses our computable polar library um you know there's a bunch of proofs that are there for soundness there's a few lemurs which are missing and I see this email on like Friday evening and I just do a couple

proof runs I go to bed I wake up Saturday morning and I'm like hey here's PRs with the proofs that you're missing and then it's done right and that's kind of nice because it means if you're Like if this is your first experience with lean and you might otherwise think like a I've written the program and I've implemented it like I feel this is secure. I just don't know how to like prove this cuz it's just kind of annoying to proof things >> in a proof assistant compared to doing on paper and now actually you just like click a few buttons on a web portal and you get a proof. >> Um that that feels like that feels really nice like that's like a big you know a big boost. And so I think you know the the the things for us kind of um moving forward are going to be much

less kind of trying to deal with you know all of these boundaries that we mentioned um and trying to actually kind of embed lean and other tools like in solvers like directly into the way that people do research and software development u and that includes you know we kind of like you know can we get people to you know kind of write down the spec for their protocol in Arclib given that we have all the prerequisites like If you anything that's coding theory based like everything is there now you would be able if you do like an improvement on were you should be able to state it in our clip um and certainly if you can automate the proofs you should be able to state it and get proof much sooner than anyone can peer review it right I think that that that would be

like a goal same as like if someone does like the proximity gap stuff like I feel like we should be able to like do it in lean verify it in lean before it's peer-reviewed I think that would be like a nice a nice thing and same for circuits right if if you can do like a nice lean DS yourself with circuits. Just write your constraints in lean. Write your w generation, you know, in lean potentially and then you can just prove things and it's just much easier to prove things. >> It's lean is a good functional language. If you like functional languages, you can kind of use it. >> That might be a big if. >> Um big if. Yeah. But it's good enough for some people, right? And like for critical software like it's okay to not have everyone write this code and it's

the way that it's done, right? There's a huge centralization issue with like everyone uses Pony's 3. So if there's bugs in Funky 3 like multiple ZKBMs can be affected, right? Um and so you might as well if you're going to do that, you might as well do do it in >> put in the effort. Yeah, absolutely. >> And then and obviously the next step after that is because we talked a bit about, you know, the boundaries is always, you know, the compilers because these compilers are like huge things and LVM is like this huge, you know, kind of massive IR that is hard to do much about um uh because it is just huge. And so the next boundary for us is really kind of like well can we just do things in lean natively and we save ourselves of extracting a lot of the stuff into lean

>> and then can we write actually compilers that are like kind of limited and easy to formally verify and which actually output you know hopefully actually more performant code than you know the rest compiler mind. So that's the next that that I think is the kind of next thing because you have um for cryptography specifically I'm not talking about programs in general for cryptography specifically you don't need your compiler to do that much you're operating on basically you're doing finite field arithmetic you're doing operations over polomials so you need optimization passes related to this you need like mongomery reduction or barit reduction you know all of these things but you don't need everything that you might find in LBMI you have a lot of optimizations which operate at a reasonably high level because they're

primarily like mathematical in nature rather than like learnable software optimizations. Um and you have things like you know mutating in place inside an array which you might not do that much of. So the compilers that you need for like a proof system for a verifier for you let's say for a verify because then you can run it on CPU and not rely on GPUs you don't need that much right and you have these compiler frameworks like ML which are based on this idea of having these small dialects that have a couple types a couple operations and you just have standardized data structures and a standardized way of lowering from one dialect to another all the way down to you know assembly or whatever hardware back end you want.

>> Mhm. So you you have these compilers that you can write which might use four or five ML dialects and that's it at least back then and then you have like hardware backends which would be unverified and we now have ML data structures which are reimplemented in lean and which are asymtotically fast >> and so you can write a compiler in lean with data structures which are proven you know memory safety and all of that is is proven. Um, so the next step for us is basically kind of like compile from Arctip specs to, you know, whatever hardware back end via a compiler that we're going to write in lean and which we're hoping is going to be faster than Rust.

>> So we're bypassing research on paper, bypassing coding into Rust, everything goes into lean directly and we have fast executables and we're happy. >> Yeah. because then you kind of go full circle to like the idea of lean VM is to kind of minimize a lot of these assumptions and to have actually like you have a tiny Iser it's very easy to formalize um you have you know specs and you have like a compiler in between which is which doesn't need to do much right because you have like yeah five you know five instructions you know and so kind of compiling down to that from arc lab or some kind of DSL like the scope is >> not too bad like it is actually possible to just like formalize this and then you and then you get you know you get to this thing of like how do we minimize

boundaries and it's like having a kind of lean stack that you can actually provide assurance for as a whole that that's the end goal I think >> well looking forward to it >> Alex I want to thank you so much for coming on the show thank you and I'd like to also thank the podcast team Anna Rachel Henrik Tanya and Hector to those of you catching us on video thanks for watching and to our listeners thanks for listening