Reducing the Trust Surface

Transcript

[music] [music] Thank you everybody. Thank you. Thank you for introducing me and special thanks to Justin and Kev that make my life so hard. So now I have to actually explain what is formal verification. So I imagine all of you have heard the buzzword of formal verification. uh Derek will be with me. I'm going to try to be a little technical. I apologize for that, but please uh bear with me.

So what is formal verification and how is it reducing the trust. So this is a still a bit informal but idea we are hearing more and more about bugs uh found by AI agents and we see everybody know like this oppus models coming better and better model and I'm sure you have seen in the last even few days people are finding bugs in everywhere things and even worse every time there's a new order there are new bugs being found. So the question for you as a developer how you protect

yourself against a new bug and the only way at least or at least [snorts] to to prevent against a new bug is coming with a proof that at least the new model will not actually find the bug. And this is actually what formal verification is trying to do. And as you can see probably I'm probably one of the oldest people here. So I can tell you that formal verification used to be something that every time you say you are working formalification people are saying you have to go out of the room. So now it's kind of the opposite. Formal verification is becoming something that everybody is speaking about and formal verification is is becoming like this

because of the AI and AI is doing actually two things for formal verification. It make it necessary but it also make it easier. There are many many things I mean that we can do with formal verification and we actually only touching the surface of it but the idea is formal verification can do many things for you. So it can actually go from the uh informal spec to formal spec. It can also go from the spec formal spec to the bug or to the code. I have here tried to explain how you basically do some kind of a gentic loop where you basically take the spec. You can think of intent that you even

explain informally and from this intent you can go with the agent into the the code. But the interesting thing once we have formal verification we can actually check that the that the agent does what it's supposed to be and there are a lot of excellent formal verification system in particular people know about lean or SMT or others or walk or or HOL or anything. The idea is that these these tools you can use them and every time you generate the code you can actually make sure that this code satisfies the specification. So this is an agentic loop and if the a if the formal verification tells you that the code is

not right so the agent can try again. So this actually gives you a possibility to find bugs and also to prevent bugs. And this is why many people and you have seen in the previous talk are actually believing that formal verification is actually will help us to build a more secure code. So I'm sorry I wanted to give you just one technical stuff. I want to also give you a little of introduction and I think there will also tell you about what the EF is doing about it. So if you I want you to take one thing from this lecture is one principle that we use in in uh in formal verification I'm sure it's

something that you have in high school or whatever it's the idea of mathematical induction and actually mathematical induction is what drives formal verification in many tool including us and it's a very very simple concept but surprisingly I found out that many many people get it wrong and it's funny when I ask people and I I have taught this class everywhere in the world and everybody say they understand it and you show them that they don't and they still think that they they they understand it. It's a very very simple concept that a lot of people get wrong and I'm not even sure I don't know why.

Okay. So I don't have actually a better good ways to explain it but the only way I can explain it with with a very very simple even trivial example. So the idea is uh let's say basically takes from the literature is basically this idea that you want to come with a inductive hypothesis. Okay. So you want to prove a property and instead of proving the property you end up actually proving stronger property that is inductive. Okay. So you want to find something stronger which is inductive. And let me just show you a very very very simple example. And if you get it I think you get this idea of

sort of formal verification. If you don't get it don't worry. So here is an idea. You have a ball and you are playing this ball. Okay. And the ball actually can go, you see that the ball actually can go from A to C and for B to D. Okay. And basically you see A can move to C and C can move back to A. Seems trivial. Okay. And what do I want to prove? I want to prove a very trivial property that the ball doesn't get to B. Seems like a right property. You all agree right?

You all agree is it inductive? Everybody will say yes but it's not. So this is a very trivial property that when we are trying to prove it we can actually not prove it by induction. Okay. So that's a [snorts] very very simple and of course you can go in a complex system and see that. So what happened is that we ended up finding defining it mathematically as a series of numbers and you see here we start with x0 being eight and then you define the next number and then you're proving a claim by induction you say for every number it's not d in the basis it's true but the induction claim is not

true okay so basically if and any element neither either reachable or not reachable it's not deep you want to show that in the next element it's not deep and the system will give you what we call a counter example to induction. So it's basically telling you that there is a way that you can go from B to D. You say this doesn't make sense the system never reached this state and you are absolutely right but that's the beauty of induction we don't actually reason about the exact state we are reason about the claims which are based by the induction. So in some sense the beauty of formal verification that we can also forget about things. Sometimes formal verification alo is also could be easier

than testing. In some sense we are thinking about the properties and how do you verify such a property by mathematical induction. The idea is that when we don't know how to verify something we verify something stronger and verifying something stronger is often easier. Okay. So in this case I made it stronger. I tell you that the ball cannot reach B and the ball cannot reach D and this is actually something easier and now it's inductive and the system you can prove it with lean or any system that you want. You ended up strengthening this and actually surprisingly we are getting some example that LLM is

doing that too. We are finding out that LLM agent are actually knowing how to strengthen things. Of course there are technological solutions that people build uh but but in fact LLM is actually getting better so in in getting induction claim and actually this one I tried and actually the agent is also able to actually strengthen this claim. Okay. So I promise this was the sort of technical I want to give you a few case studies that people apply formal verification which are very relevant to the Ethereum ecosystem. There are many other examples and I'm sure with the age of LLM we'll see more.

Okay. So the first one uh which I was uh part of course the uh a lot of people did it before me but together with academics in uh in in in Microsoft research uh we have actually developed a system for reasoning about distributed systems. Uh basically these are open source systems particular IV IV actually is an open source system. uh I think it got now the 10 years test of time award. So it's a system for verifying distributed systems. Why do we want to formally verify distributed system like consensus and other? Because what we are seeing even though this

system are simple we actually find cases that it's very very hard to test them. So maybe a very very interesting idea is an acade academic system called Ziva which was developed and formally verified and then 10 years after people found that it's it's wrong. So we actually want to avoid that and we want to formally verify the property and the interesting thing about consensus like like Ethereum and others that the concept of correctness is simple. The corness of correctness is that all the nodes agree on the result and that there is a termination. Another thing which is interesting about uh distributed system at least you think of the design that

actually is performification and we ended up actually showing that in a system called IV and later on actually recently it was written into veil into lean. So the idea is instead of reasoning about the concerns of implementation we can reason about the design and in fact reason about the design is much easier than implementation and from there we can derive the executable implementation. So that's great but I want to warn you in fact it's not so simple because once you reason about complete implementation like get or rest it gets way more complex because the inductive claims remember what we talked about this idea of inductive reasoning when you are

reasoning about things that break the abstraction it is much harder to reason so in fact this is where we still need research so if you want to verify consensious protocols and we see and And I'm sure we have seen and it's not just in blockchain. We see companies like Google and others. We are finding many many uh bugs in in protocol like HCD or any protocols which are consensus algorithms. So this is where we going to use formal verification. Formal verification of the design is easy but formal verification of the implementation is much harder. We need more research. We need more LLM. But I think this is the way because it's very very hard to find these bugs with

testing and I imagine that in the future and I know that in fact Ethereum is doing this is we're going to see case that that people actually we go from the design into the implementation. Okay. So that's the first case. The second case which is very interesting and that's also what Stor was involved in many other companies. Thanks to vitalic we have this concept of smart contract which is beautiful but because it's a short code which is actually explain everything in the code. So basically this is amenable to formal verification and why is it amenable to formal verification because there are natural properties like solvent C and others we came with working with

excellent protocol like lido and a we can actually specify the properties of the protocol what it does using mathematical reasoning so that's great and actually the interesting thing that we found is that the earlier you do it and if you seek for example if you look into a v4 is a case that the or even more for you see that these are the cases that the formal environment were written before the code is written. So this actually gives you a huge benefit even if you just write this environment informally you can actually get a huge benefit by writing the spec and then you use system to reason about it. There are a lot of tools which were developed and

all of them are open source and I encourage you to use them. SMT checker by the Ethereum foundation uh controlled by uh runtime verification satur by Sata all of them are open source you can use them. So uh in particular auto prover actually also built on LLM. So it's easier to use it actually find the spec you can also use it as a skill. So it's a it's a basically a skill that you can use to get your formal verification and to get your system formally verified. It's integrated with the STO approver and will be integrated with lean. So you can actually use it to simplify the use of formal verification.

The the story here is scaling and what we think is mathematical induction is a key. But a little bit of warning, you have to have your modular code. If you take a code which is very very complex, inductive reasoning becomes hard and then formal verification also becomes hard even in the age of AI. Okay. So I want to give you a little bit uh of a bad news. Formal verification can go wrong. Uh one of the most interesting computer scientists is Kut and Kut actually has this a very beautiful quote that say don't trust this code. They only formally verified it. Okay. So, I think there is some

truth in it. You need to be worried when you're working on formal verification. And some level of paranoia is good. And I'm not going to scare you, but I think I want to give you sort of four things. Each of them you should worry about. And you I will give you my own solution for that. You can take your own yours. Okay. So there are actually four problems that can happen with formal verification and each one of them is interesting. The first one is what get you into New York Times. Okay. Is soundness. What does it mean soundness?

You have a bug in the system. So for example, everybody knows and I think uh Justin mentioned that uh we can prove conjunction with AI. So somebody was able to actually disprove the collage conjunction with AI. And how was this done? Because there was a bug in LIN. Okay. So they use the bug in LIN. So basically due to a bug in the system, you can actually verify something which is not right. And of course I can tell you with Sattor, we build this very huge software. This can happen. There's a bug in the software that lets you conclude something wrong. I actually worry about it less because even though of course lean is worried about it and there's a

nice postmortem but because this is in my experience the the lowest hang things that happened to us most of the time it's not the problem but this is something that really really people care about what do I worry about I worry about other things and I think we should worry about them more in the future so the first one and actually this is bad and it will be worse We are reason and as and mathematician we we are trained to use about reason about model but in fact there is the real life for example this is the program. So there is a mismatch between what we are proving about and what is executed. And this will be more with the

AI. You come to the agent and you say, "Oh, you have this very complex code. You read that in C, C++, TypeScript." You say, "Verify it in LIN. I've seen it myself. It verifies it in Lin, but it verifies a model and then it verifies beautiful theorem, but in fact it has nothing to do with the with the with the call. I'm having the solution that we took in Shatura it's expensive is basically verifying executable code and many people are doing similar things it's an expensive solution we verified the low level there are other solution people are thinking about automatic extraction also in IV we developed this idea of refinement checking so there are other

solution but this is definitely something you should worry about the other thing that you should worry about and this already happened you verifying something under certain assumption and in fact if these assumptions are wrong then you are in trouble. So this is another thing and you can do some kind of testing. I personally believe in mutation testing. So this is another thing but in fact what I want you to take the the worst thing that happened and this is most of the bug that we are missing after formal verification is the fact that we didn't write get the right specification.

This is the worst thing that can happen and there's a joke that say formal verification make sure that you have the same bug in the code in respect. So I think this is what you should worry about. We are using mutation testing but the other ways of course rewarding people for for finding bug in the spec. I think we just already said that we have the spec. So rewarding pe uh rewarding the community for finding bugs in the spec is very very useful. Okay. So [snorts] I want to actually before I wrap I want to actually tell you something which at least for me was surprising and it's something I as you can see I work in this field for a long

time and I work with this field for AI in the last year. This something which I found surprising. I'm not sure it's right but I want to actually share with you. So there actually three challenges in formal verification. Okay. And let me explain to them each one of them is interesting by itself. First one is writing the informal specification understanding what you want to prove in the system. The second one is going from the informal to formal. You use a whole logic like we use or TLA it doesn't matter or lean writing the spec. And the the last challenge which actually I spend most of my career is the how do you go from the formal spec to a proof or to a bug and there are different

technologies using dependent type SMT it doesn't matter static analysis so there are these three challenges how many of you think that the third challenge is the hardest interesting you are all right how many of you thinking that the second one is the hardest Okay. Few. How many of you thinking of the the first one is the hardest? You are right and I was wrong. Yes. So in fact the first one is by far the hardest and it was very surprising to us. We are work again maybe in few years it will be different but what we are seeing when working with agent we are working with frontier models. The frontier models is

very good going from informal spec to spec. It's pretty good into going into any open-source tool but in fact it's it's h it's very very hard with with understanding the inform aspect and this is where we human still has advantage. So coming with the inform aspect is the challenge. I'm I'm wrapping. Okay. So I wrapping before I get the egg there three takeaways I want you to take from this uh introduction to DX.

So first I think I repeat what Vitalik say code security we actually want to use formal verification I think it goes well with open source I think agent will help I don't think you need PhD everybody can should be encouraged to use form verification also I heard people say uh wait until the code is is is is done no run it as early as you can before you write the code with the agent everything the second thing and I think Ethereum is doing it and Derek would already explain we want to verify the whole state. We want to verify that. But the third thing and I think

this is actually where I think we as a community should change. We should change our mindset. We should try to understand that the biggest and the hardest problem is specification. And every time when somebody say you formally verify that try to check what they have formally verified and try to check the specification. And we need and this is where we as a community need to find some kind of FV methodology some kind of methodology to understand what was formally verified and even reward people if they have a good spec and and this is a critical paradigm shift. So thank you everybody. I'll I'll I'll have Derek explain it. Welcome, Derek.

[music] >> Right. This great. Thanks, Mully. Formal verification has gone from being the the subject of academics and esoterics to screaming right into the mainstream in the last who knows six months. Um, so it is my job in 10 minutes to try to convey the amount of incredible work that's going on in the Ethereum ecosystem and around informal verification. Um, it started with us kind of experts and it has just been blossoming and blossoming.

Um I think with uh the advent with with AI being so powerful at finding bugs um formally verifying everything is more and more becoming an existential problem and we need to be formally verifying everything that we possibly can. Um, so what I want you to take from my 10 minutes here is um that formally verifying things are is very very important. But the good news is that agents are good at it and people smart people are coming in uh to do it and it's actually not as hard as you might uh think. Um so we started um our formal verification

work I guess in the last 12 months was initially focused on um on Ethereum scaling roadmap uh with ZKVMs and we have had three tracks that have have proceeded to grow greatly. Um I decided to not make my slides particularly simple because I want to convey the kind of dense amount of work that's happening. these three tracks I'll I'll explain them and then I'll kind of um show how the work of formal verification is is spreading in all other uh directions right now. Um first the first one here we we were caring really um a lot about uh the ZKVMs um in particular the circuits. Um so the

circuit for ZKVM is the analog to a chip um for uh an execution environment like a risk 5 or ARM or or whatever uh your machine uses and um ZKVMs which are so important to the scaling road map um implement risk 5 in circuits and it's a great place for bugs. So we started with this huge kind of dense wealth of work um from academia um to industry to uh bespoke DSLs. Um and the key I guess uh takeaway um is is that uh well yeah I guess we made a lot of progress um on on formally verifying uh these these

circuits and that led us to the next project which now that we have circuits that we can trust um we need to implement the EVM in inside of these circuits and we started thinking a lot about okay how do we implement the EVM in a safe and secure way. we started thinking about uh existing implementations of the EVM and then um this year has been so unbelievably wild that um about halfway through the year we had this kind of insane brainstorming idea that well what if we tried to implement the EVM directly in risk 5 assembly with no compiler no intermediary um and that that

brought us to this um massive agent-led um project that was initially totally experimental um but this um but actually very successful and um I have a link for you if if you want to follow um it will very soon hopefully lead to the fastest and the most secure um implementation of the EVM um formally verified endto-end direct directly in uh uh initially in bite code and now in a in a very low-level language. Um so this is an auto research competition that is live. Um we would love this week if you

want to participate please um yeah uh please uh please visit the link and um and your agent will help you get started. It's actually a great first project uh for formal verification. Um then um underlying all of this we have the EVM, we have the circuits um and we also care about the cryptography and of course cryptography underlies everything that we do on the inter internet. Um and it's becoming more and more and more important that we have secure uh cryptographic protocols and secure implementations and they're very good targets for formal verification. So in the last 12 18 months we've been working on this vast ecosystem of libraries of

formal specifications for um different aspects of cryptography. We started with snarks and it has just grown and grown and grown. Now we're doing a lot of hash b hashbased uh cryptography. Um and um I guess this this the scale of the work we're getting more and more uh collaborators and people interested in formal verification that are contributing um to to these specifications and we welcome more contributors and more collaborators. Uh so please please find me if you're interested. Um this um once we got all of the uh once we kind of had the fundamentals in a

good place, we started to really care about a lot of the code that ships in the wild is in Rust and um we were doing a lot of things kind of at the assembly level and um we're using this theorem prover lean 4, but we started to really care about the pipeline of getting Rust code that executes in the wild and how do we reason about it? Um there's this uh pipeline that we're using called um hacks or anas that lets you translate um that lets you translate uh rust into lean and um uh we have started to use this on core cryptographic libraries including plunky 3 uh lean VM uh work on that has happened um there's quite a bit

of work just um on on on these proof systems and the associated cryptography. Um, but this method has the problem that you have to trust a translation from Rust into a formal environment into lean. And so we started thinking well we were successful at formally verif at implementing the EVM directly in assembly uh using agents and formal verification to show it correct. um can we do this in a more general setting? And I think in the next six or so months, you will see us um as a community, and I I really need to emphasize how much of a community effort this is, um start to gain scalable

tooling that will allow us to formally verify risk 5, x86, and ARM code directly from any compiler um directly in uh in lean. So if you've been paying attention to the news, lean is of course everywhere and everybody's kind of talking about it. Um and um that that's the tool we use. Um in a f in a later slide I'll show you how you can learn more um about lean. So this has been the kind of core work we've been doing at the Ethereum Foundation. But um what we have found is that there have been a lot of people in a lot of different ecosystems um who care about secure code and shipping the

high most high assurance code possible that they can um get into formal verification and it really is doable. I need I I just really need to stress this. Um installing lean and starting to use it is um it will take you less than two minutes to get it to get it going. Um so we've been seeing things in consensus in postquantum data uh um um we've been seeing things um with hashbait cryp cryptography um and um we have this new library that has just started within the last week called ETHIB um that uh you can check out that we will be aggregating the core formal primitives

of the Ethereum ecosystem and that is very much intended to be a community project. So again, we're looking for more collaborators. Um I have I've I've just taken eight, I guess, of um some of the most interesting projects and I've converted them into QR codes. So maybe choose one of the QR codes and visit it. Uh if you're curious and just kind of get to know the different um crazy work that is happening. Um and um I have good news for you. If you're interested in formal verification but you don't know where to start, later this week I'm running a workshop on formal verification in lean Thursday at 4 p.m. And so if you're around and you're interested, please come. We would

love to introduce you to formal verification and how you can um get started. And here is um on the right hand side here, this QR code is a link to a Telegram chat uh for all things formal verification at DevCon. This week we have so many things going on. Please come along. Even if you don't know anything about formal verification, we're all here to learn and we would love >> [music]