Formal Verification in Lean

Transcript

[music] >> Thank you. Okay. Thank you so [clears throat] much for coming to this workshop. Um I guess just so that you know whether you are or not in the right place, this is meant to be an introductory for some for for for anyone who's had either very light contact with Lean or almost no contact with Lean at all. What I would really love for this workshop to do is is to be kind of a hands-on introduction where you write your first proofs in Lean and you just get a very concrete idea of what we mean by formal verification, formally verified, and what this theorem prover is that

everybody has been losing their minds about uh Lean. And so [clears throat] I have a code base um that um okay. I will show you the QR code in a second. So uh plan for the next hour or 50 minutes, I guess how much time we have. Um for uh the first bit I will just talk a little bit about formal verification, um what it does guarantee, what it doesn't guarantee, and I'll introduce some of the basic terminology that we use uh for example TCB um to to talk about code that's formally verified. Kind of what does that mean?

Um then we will look at programs and proofs in Lean together. Um and we have some simple exercises that we will go through together and then we'll talk a little bit more about the nuances of the guarantees of formal verification and then we will have questions [snorts] and conversation. So I would love for this to be interactive and so at any point um I please feel free to raise your hand or interrupt um or ask questions um and I would yeah I I'd love for this to be interactive and um and very doable to kind of follow along.

Right. So if you would like on your own machine to do some in Lean. I have this repo. Um, the QR code. Let me make sure goes to the right place. Should do. Yeah. Um, so this Okay, is this QR code working for people? Yes. Okay, phew. Um, so this is just a repo on my personal GitHub. Um, and um if you want to follow along on your machines, uh feel free to clone this.

Uh Lean is easiest to use in VS Code. Um, and there is a Lean language extension. Um, Oh, I don't have internet right now. Um, if you search Lean, it should be very quick to install. Um, or if you already have it installed on your machine. Um, Yeah, and this script should help you get started.

Yeah, that's completely right. Um, yeah, let me just Um, if you don't want to run the script, which I completely understand. [laughter] In fact, maybe you shouldn't run the script. Uh it is not. It was [laughter] Oh, it just gives a small donation to my wallet. It's just a small donation. [laughter] The uh Let's see. What you should be able to do if you clone this repo.

Um, you should be able to to um Where am I? Um, if you go lake build. That should actually just build it. Yep. And if you want to go lake build workshop. Like that. Um then that should build the code for the workshop. So yeah forget the script. Don't run the script. But uh lake build work uh lake build if you just do that in the in the repo root.

That all that does is compiles the lean files and type checks them. Um And fun fact. These slides are written in lean. So maybe uh so so these slides type check um and uh it just goes to show that you can do a lot of cool things in lean. Um Okay. While this is going on while while you guys are getting set up.

I'll just talk a little bit about formal verification um and then we'll dive into some examples. So uh what is formal verification and what does it and does it not guarantee? Um I guess the classic pitch for formal verification is that anytime you're writing code um you will write a function and you'll write tests about that function and the idea of all these tests is obviously to gain confidence that your function does what it purports to do. This is a of course a very very simple example and um the tests are you know seemingly trivial but but I mean well we've all had experiences of

writing a function that seems trivial and then testing it and realizing that we made a silly mistake um [snorts] and then we've also had experiences of writing a function where the its compliance to our kind of spec is intuitive um and and unclear and the way we gain confidence is that we write a bunch of tests. That's kind of how we gain confidence that our uh code matches our specification. So, in this case, um we have some tests and this is great um but you the problem with writing tests is that you have to think of all the clever edge cases and you can only write a finite number of tests and there's this pragmatic boundary. And um all three of these tests that I've written here they could

in principle be expressed as kind of a one thing that I want is that I I want this max function to uh to be a max function I guess. So, maybe [snorts] I can um like I could express all three of those tests with this um this proposition here which is just saying um given any two natural numbers A and B um A is going to be less than or equal to the max of the two same and also B is less than or equal to the max of the two and then max [snorts] in A and B is one of A and B. That that I would say is a specification of the math max function. And instead of writing all of these tests for the max function, it would be very nice in our programming environment if we could um just state

this theorem and then we can then we don't have to write the tests um oops. Um so the great thing so that's where formal proof comes in is that if you're able to get your program into a setting where you can reason about it formally, then you can do that instead of there are certain classes of tests that you just don't have to write because you can write a formal proof about them. Um so in that case uh the statement so this is kind of um this is Let me see if I can move this. Okay.

This is what the uh the form of a theorem will take in Lean. Oh, I don't know why it usually Of course, it's not working right there. Oh, well. This is the the the form that it should take uh that it does take is there's a theorem keyword in Lean and you give your theorem a name. So this is called max spec and then you write and this is the exact proposition we just looked at. So A is A is less than equal to max A and B, B is less than equal to max A and B and max A and B equals A or max A B equals B.

And then um and so here here is the statement of the theorem or your specification and then you have this by keyword and then after that you write your proof and what these are these are tactics as what they're called and their ways what what um what Lean will do is so these tactics construct what's called a proof term that the Lean type checker like the Lean kernel then checks to be a correct proof and um the interface as we'll see shortly is um it um it will show you the there's this interface in VS Code um that's kind of the standard way of doing proofs like this. Um it will show you your proof goal and then these tactics allow you to

manipulate the proof goal um until you can uh write a like a trivial proof. Um so like I said we'll see all of that in in a second. So in this case what this proof does first it unfolds the definition of max. That's what unfold keyword does. Then it splits the goal into all of these disjoint um goals. So it'll split it into three and then there's this Omega keyword that does um basic like comparisons, arithmetic and stuff like that. So there's this nice tactic that will be able to reason um just about like basic algebra. Um yeah.

The by is a keyword that tells Lean that you're about to start writing the proof. Um so it it's it's sort of like this is um so in in Lean um like um there's the there's the so-called the Curry-Howard correspondence um where proofs are programs um and types uh propositions and so uh are things that you can prove. So this is something of type and the type is this thing you want to prove and it's defined as and then this is what constructs the proof term. So that's the by keyword.

Um, the cool thing about Lean as a programming language is that you can have proofs and programs in the same setting, same file. Yeah. In this case it will be a a user defined. So um defined here. So we had a function that we defined. Yeah. Sorry? Oh yes, sorry. Nats is a is a natural number. Yep. Um, just like zero and successor. Yeah.

Um, so right. So anytime you have code that is formally verified um it will it will have to have uh the so I I should caveat there are other ways to formally verify code um and this is Lean specific. So everything I'm saying is Lean specific. Um, and anyway so anytime you have code that's formally verified in Lean you have at least you have these four components to it. You have your implementation. This is the code that is running and um this is written by the developers. And then you have a specification and in particular you have a formal specification. What that means is it's just a specification written in

Lean. And um so whereas this proposition here we might call that an informal specification because you write it on pen and paper even though it's pretty formal. Um, a formal specification is written in the theorem prover and that's that's what formal means. Um, and um then what you then you have a proof that says that your implementation um satisfies your specification um which is precisely what we saw right Um, this is the proof.

Um, and then you have Lean um that will check the proof. It has a type checker and um it will um yeah, it it checks the proof. Um, and so if you have your implementation, your specification, and your proof and the proof is checked and the Lean can compile it with no errors, then you have a formally verified piece of code. So in particular, the max function that we just saw is a piece of formally verified code. Um. So I mean um that immediately I think formal verification has this reputation of being sold as you know the most I mean well it is highly secure if the spec is good. I guess is is the summary there.

And so it has this reputation of being kind of this bulletproof thing, but um when someone says formally verified, it could mean that there's just one small theorem proved about the code base. It could be mean that there's this huge exhaustive spec and a lot of work. So you know not all formal verifications are created equal. Like um the more theorems you prove and the better your spec is, the more secure security you get from your formal verification. Uh yes. >> Yeah, I had a question on how uh what's the availability of auditors to check the still trusted part here?

>> The um the still trusted, right. Um right. Well this is kind of nuanced. We'll talk a lot more about the still trusted components um a little bit later. The I think the best way to go about it. So I guess this the specification in some sense is trusted because you've had to with with formal verification, you have your program, you have this description of what it means for the program to be correct, and maybe you just had a bad description. Um and so in some sense you trust the specification and and and the quality of formal verification really rests on the quality of your

specification. So that itself is of a philosophical question. How do you know that you have described something correctly? Um, and there there are kind of lots of levels of analysis there. It kind of depends on the setting. If it's a smart contract, maybe you have a clear idea in game theoretic terms what you want. And so maybe you can specify clearly in that way. Um, if it's cryptography, maybe you have a paper that's published that you can look at the maths and and and um and verify um that it the maths are what they should be. Um, but there are lots of nuances to specification. And I think that is in some sense now that AI is so good at writing proofs, in some sense that is kind of the core of the problem.

There's another Yeah. >> What if the implementation is in another programming language? >> Ah, yes. We'll come to that very shortly. Um, and let's see. The model is same thing. Um, and then the tool chain. There are some ways to reason about the tool chain. What we do is um in fact I think this is um this is Yeah. I'll I'll talk about it in just one second. I I want to emphasize though that formal verification, I think we've had a little bit of a marketing hiccup in in the field where um maybe to be concise, maybe to um to really display the value that we can add to the formal verification. Um, sometimes it's seen as something that's advertised as

like a silver bullet will just solve all your problems. And if a code base is formally verified, then it's like you know gold standard secure, which can be the case. But the best way to in my opinion to think about formal verification is a method of reducing the trusted surface that you have to audit. Um, so you can establish real guarantees in formal verified code bases, but there's always a boundary of verification. There's always something that is not covered by your formal proofs. And it is best practice if you really care about your code base to understand that boundary. That's where you Once you have your proofs, you should put all of your attention to the boundary of verification and make sure. Um, and so that's where this concept of trusted computing base comes in.

Often called the uh TCB is um is is what people will colloquially call call it. Um it is all the things that you rely on to uh if you believe the proof, if you say this is this is uh correct, there are a list of assumptions that you do have to make. For example, the lean kernel, this is the thing that checks all the logic of the proofs. It is small. It is trusted. There have been bugs recently, and this is actually something that happens in all the theorem provers. However, these bugs truly are edge cases. If you're if you're writing straight line normal uh proofs in lean, you almost certainly won't encounter a bug. Um and what happens in the lean

type checker, if there's a bug, what it means is that you can um you can derive false. And uh if you've taken logic or anything like that, in logic, false implies everything. So, if you can somehow derive false, then you can prove anything you want. And of course, if you're formally verifying code, um that you don't want to do that because you've just invalidated all of all of your work. Um but you do need to make sure an agent hasn't done it because the COA to cut corners. Um also, when you're formally verifying something, um there will be some there there will be some axioms that you likely have to assume. Um so, if your code interacts with another codebase, you'll probably have to axiomatize what that interaction like assume things

about the other code coming in or messages coming in or assume something about the environment, assume something about a pre-compile that you're going to call or something like that. And usually what that looks like is you summarize what you expect the behavior. You essentially specify the behavior of these other components that you're not going to go formally verify because again, you can't just you can't do every last thing. Um and those will be kind of the axioms. So, that's part of your boundary that you have to trust. Again, you have to trust the specification in some sense. You have to believe that what you've described is actually good. Um and uh we'll talk we'll we'll talk more about this model, this transition. If your code is not in lean natively, you have to bring it in to lean in some

sense. And so there is this transition that is trusted, which is kind of an issue. And then also if if you're for example formally verifying Rust code, you will trust a compiler. Even if you're running lean code, lean has its runtime is not yet formally verified. And so there have been recent bugs in lean's runtime. So even though it's a functional programming language in which you can also write proofs, you know, not everything is covered is is all I'm trying to say. We can establish strong guarantees. We can. Like formal verification is very useful, but it's important to know that it is not like the only thing, right? We should still

be it should be one of of the suite of things that we do with our code to secure things. Yes, back there. >> Do you see a spectrum between like just using type systems and full-on propositions as proofs? And can you get some of the value that you would get in lean like in a nice well-typed language? >> Oh, yes. I think types I mean the strength of lean one way to think about lean is it's a functional programming programming language whose type system is so strong that you can state and prove any

theorem, anything that you want mathematically. And then there is a spectrum from any an untyped language to this, you know, maximally typed language in some sense. I think that's why Rust is so powerful is its its power is it's in in the type system in the borrow checker. Like what a type system a good type type system does is it it codifies the logic of the programming language um in a way that you can interact with and in a way that um establishes some guarantees about how how the language runs. Um and so uh yes there there is a spectrum and and I think

one reason why um up until now people haven't just been writing all their programs in uh in something like Lean or Rock or something like that is that there there are tradeoffs and um maybe you need more access to low-level details or something like that so you're you want more manual control, you might accept a slightly weaker type system in order to do that um and anyway so yes there is a spectrum yeah. Um okay um and then maybe why do we care about this now? Um why is everybody so obsessed um with formal verification? From the

Ethereum Foundation's perspective we are doing a lot with uh ZK VMs and um trying to scale through them um cryptography and um for I mean anything we do on Ethereum we need high assurance. Uh smart contracts are the same any contract that that holds high TVL um you just need um high assurance and now that AI is so good at finding bugs we need high assurance and formal verification is a is a way to get there. Um tools like Lean have really matured in the last um few years and they're getting better and better and better especially with more attention on them.

Um and as we'll see Rust can be translated into Lean um in some ways. And then maybe the best reason as to why now is that AI can write your proofs for you. It used to be it used to be the case that um most of your time in formal verification was spent arduously going through proofs you know um and it was a huge amount of time um sunk into that um and AI is just really good at writing proofs. It's kind of one of the perfect applications. So, um so now what that does for us is that informal verification really the bottleneck is not so much writing proofs and it's much more about um writing a good spec and reasoning about that spec.

And that's kind of the main um bottleneck and that is a skill that you can start learning today. So, um let me make sure okay. Uh right. Now let's look at some concrete examples. Are there any questions or comments before we go into uh go into something more concrete? Right. So, Lean is a programming language. So, we can write programs in Lean and I have some very simple examples that kind of mimic something that you might see in a smart contract. This is not a smart contract um at all. It's just functions that you might kind of see and

they're meant to be illustrative. So, they're just simple functions. So, we have this function uh total supply. It's written in a functional style. So, if you're unfamiliar with functional languages, um uh we can kind of go through that a little bit right now. Um but so you have this function called total supply. So, this def keyword is keyword for writing a new function. The name of the function is total supply and this is the function signature. Okay, all good.

[laughter] Okay. So, we have def the def keyword introduces a new function. Total supply is the name of the function. This is the type signature and so what it will take suppose you have your supply in a list of natural numbers. So, it will take a list of natural numbers and then it and then it will return a natural number. And what does it do? It just aggregates um it just kind of goes through your list. So, what what this is if you're unfamiliar with a functional syntax, it pattern matches on on the input. And so it will take a a list. That list will either be empty or it will have the form uh it'll have a head and a tail. And so if it's empty, then um then the function returns zero. And then uh this is

recursive. So if there's a head and a tail, it will take the head and then we'll add it to the total supply of the tail. So what it does is just kind of takes all the heads, adds them all together, um aggregates them as it goes. So we have a function maybe this is something you might see in sort of a smart contract world. Um and it's you know written in Lean. Um so we also have a function mint. Um so it will take this balances, which is your list of natural numbers. It will take a new natural number, which is the amount, and it will return a new uh list of balances. And this just appends the amount onto the list. So in Lean, there's this um in the programming setup um there is this eval keyword.

Maybe I'll show it to you actually right now. Uh Part one. Part Yes. Okay, so here's the code that we're just looking at. So we have mint here, and then it has this eval keyword. I'll actually just show you what programming environment in Lean looks like. So you have this is this right hand window is the info view is what it's called, and it just gives you information about your program. Um so if you're defining a function, it will kind of tell you what it'll tell you um what is it expecting.

So it says um so expected type is natural number here, and so zero is a natural number. Anyway, so it gives a lot of rich and useful information. In this case, you can run this eval keyword and the uh the the um LSP will um just kind of run it. So we can say total supply of 10, 20 and 12 is 42 etc. Um oops. We're not yet. Um Right. So we can have we can have programs and then we in the same file we can have theorems. So we've gone through this already, but I'll just kind of show it to you kind of in the wild. Um in the very same file you have a theorem. And

here here are some examples of theorems in Lean. Um and so we have we kind of formally verify these these two functions. Wow, that's annoying that the slides go all the way to the end. Um Right. So this is as good a time as any to introduce um the notion of induction and then we will look at concrete proofs and you can write some proofs with me. So um Lean Lean's type system is um made up of what are called inductive types. And what that means is that you um their types that you can define in a way

uh with with kind of a discrete number of generators. So um and they're useful and I'll I'll mention why they're useful in a second. So for example, the natural numbers are an inductive type in that you have generator one which is zero. And then you have this function on the natural numbers successor, which for any natural number you can take its successor and you can derive any natural number can be expressed in terms of those two generators, zero and then some number of successors. And the nice thing about that is it takes an infinite type and reduces it to a finite number of uh generators or in the case of proofs a finite number of reasoning steps. So lists are also inductive where they're generated by the

empty list and then the append operation. So any list can be described in um any list at all can be described in terms of a finite number of um appends to the empty list, which means that if you want to reason about all possible lists, then um you have to all you have to do is establish whatever your reasoning about on the so-called base case which in this case is the empty list and then on the inductive step which which is kind of like dominoes um you establish it on the the um on like the zero or the null case and then you you say if it's true for any case then it's true for its successor or for its its kind of

iterative um uh kind of recursive uh state and so so if I want to prove something about all lists I first prove it about the empty list and then I prove a proposition that says if it's true for any list then it's um true if you append something to this list and then that establishes whatever you want to prove for all possible lists. So this is induction. It's a pretty fundamental uh proof style um and it's hard to cover in you know two seconds um in in a setting like this but it's worth thinking about it. Like I know the first time I encountered induction it took me a little while to kind of wrap my head around it um but um it is important for proofs in Lean. Um your agent knows it very well

and can teach you all about it. Um so um let's just look at some theorems about lists. I guess it's probably what we should do here. Right. Um I'm you know what I okay I'm going to just show you this proof here. Um so so this is an example of inductive proof. Okay so I'll I'll just say so um so we can prove very simple theorems.

This one isn't the most useful theorem but um we can prove something like the total supply of if you have 10 20 and 12 here equals 42 that is pretty trivial. All Lean has to do is kind of unwrap some definitions. So there's this keyword called RFL or reflexivity, which tells you that Lean is just like this is trivial and Lean can solve it. Um in a slightly more complex case um you uh want to prove that the total supply behaves with mint as you would expect. So here's theorem total supply mint given a list of balances and an amount um that you're adding. The total supply, so this is what the theorem says, the

total supply if you um if you mint this amount on these balances is equal to this total supply of the balances plus the amount. Um so all that is saying is that after you mint um the total supply after you've minted goes up by the amount that you minted. Um this theorem is slightly more complicated. I'll show you uh as a proof we step through. So uh we have this by keyword which says that we're about to start a proof and um Lean won't be able to um solve it immediately um and you need to unfold some definitions.

So if I undo this like Lean um it it gives me an error. So you need to just unfold some definitions. There's this keyword simp which is very useful. It just simplifies the um your your proof goal. Um I should say I should say here um just a a view on what's happening in the info view. Um you uh in in this right hand side these all these things in yellow are the things that Lean has in context. They're things that you can take for granted or that you assume. So they're either things that you assumed in the theorem or there's there are things that you have proved in the theorem that you're able to use to write a proof with.

And then everything after this blue sign here is what you still need to prove. So it says what this says is that I have a balances um which is a list of natural numbers. I have an amount which is a natural number, and um I still need to prove this statement that says the total supply after minting is is this total supply before minting plus the minted amount. So in order to do that, what I'm going to do is I'm just going to simplify um the definitions of mint and total supply because if Lean just unfolds everything, it should be pretty trivial to see. So once I have simplified, then I get something I of the of the form here amount plus total supply

balances equals total supply balances plus amount. That is not so obviously true that you can give it the RFL keyword, the reflexivity keyword because Lean doesn't know necessarily that you can commute addition, but there are some really nice tactics like Omega that does this for you. And so Omega will will understand will um will um apply the commutativity and then you have something that's tautologically true. It's just um and then so now we've we've given it Omega and now Lean is very happy. It turns green on the right-hand side and says goals accomplished in a very encouraging way.

Um and then this is an example of uh an inductive proof. And so what we want to prove for all what we want to prove um is that for all possible um supplies um like lists of balances, for all possible um the total supply of the concatenation is the total supply of each individually added together. So this is a this is a possible specification for total supply. In order to do this, we need to induct on um on well we'll first induct on um one list and then um and then that should should give enough give us enough information to prove the theorem. So again, what

induction does is splits the proof into first you prove it on the empty list case um and then you prove it um when when the uh when when the list excess takes the form x appending excess. I realize right now I don't have um we probably don't have time to go into this in detail. Um induction worth looking into is unnecessary for this current exercise, but the these um this repo has um has more examples and and so um more more things that you can go through as exercises if you're interested after this workshop. Yeah.

Mhm. >> So if you have an invariant that says that the total supply is the sum of all user balances, then why do you have to add on the you know function about the mint or about the total supply append? Because isn't it just the same thing or is this just for demonstration purposes?

>> Mostly for demonstration. Um it is very possible that you could use uh like the theorem of of that it's So I don't think we proved that total supply we looked at the definition and inferred that it was just the sum of all the balances. In principle, you could prove a theorem that states like that, but it's not always easily applicable. Um there the devil's always in the details. So won't always be obvious. You may have to massage your proof goal before you can apply that theorem. And sometimes it's just easier to basically prove the same facts, but in a slightly different concept again from scratch.

>> So what you're saying is basically at the start you had like a a a a definition of what you hoped that this would do and this would be like something that you would use before you start coding and then this is like these later proofs are something that you would have after you have an implementation to go and verify. >> Totally. I I think that's kind of the workflow. You start with a intuitive or written description of what you want. Um you express it the best you can, and then you prove um you prove those things like these facts. Um, Well, certainly this is a fact that we would want to be true of mint. Like that is kind of a canonical property of mint.

Um, Great. So um if you're just getting started with proofs in Lean, a handful of tactics really goes a long way. Um, and we've already seen a few of these. So, RFL is reflexivity. And what that means is RFL is a proof of anything of the form x = x. So, anything just glaringly obviously true, there's always a proof of x = x. And that is RFL. And um Lean is pretty good if if it's basically x = x, but some syntactic sugar Lean can often decode that.

Um, decide um is Lean um if it's like it's decide is is uh so named for decidable problems, I guess. Um, so there are some like just kind of basic problems that you can just solve. Uh, decide is the tactic that does a little bit of reasoning. Um, simp is for a kind of simplify. It will look at known equations in in the code base or or known equalities of your things, and it will try to rewrite them to make them simpler to go with. Um, omega does linear arithmetic.

Um, Yes, intro. Um, so if your theorem has so for example uh I guess we'll see. Um, in intro if you have hypotheses, sometimes you need to introduce them into con context. Um, cases is when uh for example if you have an if then statement or if you have um like an and statement you're trying to prove, cases lets you break that up into cases. It's actually another form of induction uh or like a simplified. Induction is the big kind of general uh really useful one. Um, and then there are some really cool automation tactics. One of the the one keeps getting iterated on and

that's really getting more and more sophisticated is called grind. Um, grind, there's a similar tactic in whole uh or in Isabelle called sledgehammer. Grind is just um Lean has a big body of knowledge and um it will look at things you've already proved and if it can synthesize the proof on its own, it will. It is deterministic and there are ways to kind of fine tune it, but it's a pretty good if you're trying to write a proof and it looks like this is obviously true, but what do I do? Like what is the precise tactic? It's always a good uh to try simp and grind. Um, often those two can just just knock the simp grind Omega.

Often that can just satisfy simple goals for you. Yeah. Well, yeah, so it doesn't always work. I mean like you basically Yeah, basically. Um, the only downside is if your code base is large, grind can be slow. Um, and so you may want to optimize. Um, but yeah, back in the days of handwriting proofs, it was like most steps just try grind to see if it works. Um, and then if it doesn't, then you then you keep working on the proof. Right. Okay. If you have the code base um and if you want to do it by hand, we'll also do it here. Um, there's this file workshop part two exercises and um let's just take a few minutes and

just take a look. Um, I'm going to put these tactics. So I'll open the file here. So there are some exercises um part two exercises. And these are unproved theorems that um that I don't give give maybe give them a try if you have a machine. I'll just give you um and decide with our time constraints.

how to do this. So maybe what we'll do is I'll I'll just go through um one or two of these examples um and then there are loads of other examples in this codebase that if you're interested keep in continuing to learn to do to to go to lean. So um so we'll we'll likely use these these uh here. So let's just see. So um total supply um what we want to prove here is a theorem that says total supply of mint where you have the empty list um and you mint seven equals seven. So we have already seen this in in a theorem that we've proved and in print

we could import that theorem and just apply it. Um and the keyword for that is like apply theorem name and that will work. In fact I think I have the theorem in my context. Um so uh we already proved this theorem when we proved uh total supply mint um but this is a special case. So we can Sorry.

I I realize that I'm jumping around a little bit. So we can just apply a theorem we've already proved. The keyword here is apply and you call the theorem um and that will do the work for you. And at the end it says um achieved. But let's let's try to do it without. Um so lean um it's almost trivial if you just have the definitions unfolded then it should basically go through. So what we'll do is we'll just do simp um and we'll simplify um mint along mint and we'll also simplify along total supply.

And at that point the what this so that actually solves the goal. And what this is saying is that lean once you have unfolded the definitions of mint and total supply in this case, it's able to infer the rest. Um there are various other ways to do this. Um and it would it's worth trying out. Also I have found that agents are very good at like um if you if you ask an agent and you say this is an example give me three or four ways to prove this or kind of explain it to me, agent is very good at doing this and they're very good at writing proofs and so yeah yes.

>> So if we have very concrete theorems and we check all of it with humanize and let Claude to prove it, do we have to read those proofs or do we have to consider however messy Claude makes the proof? >> Um yes so so if the code base is large, messy proofs can really slow things down. So you may have to optimize proofs. What you need to check in general, you do not need to just read through the entire proof yourself. Um you don't need to check it at that level of granularity. What you need to check is that um it hasn't introduced an axiom.

What used to happen in the early days of like AI proving uh this happened a few times um where we try to get an agent to prove a theorem and what it would do is it would assume the theorem in a different file like kind of hide it away as an axiom and then it would import that file and then and then prove it by that axiom. And so that happened more than once which uh was frustrating and kind of hilarious and it doesn't really happen anymore. Um so you need to make sure something like that doesn't happen and you can sweep your code bases for axioms. Um so in in uh we won't we won't get through this entire tutorial but this these slides are in the in the code base that I showed you at the beginning And um it will go into more detail on things

like that on how to check your axioms and how to uh make sure that it hasn't like derived false or something like that. There are ways to do this. If you're sure it hasn't introduced axioms and it hasn't exploited a bug in the lean kernel, then your proofs are just good to go and your attention should go onto the spec. Yeah. Um right. So there are more examples um along these lines. And we have just a few minutes remaining. So what I want to do actually um if if you want to continue on this tutorial, um please please do so and also please let me know uh in some way if

if I can help. Um I uh there are more complex examples in part three. Um and I want to talk for a few minutes about Rust code um or other language code. So we care these days a lot about Rust um and we want to formally verify code in other languages too like C and Go and you know all the panoply of languages that people love to use. And the the main question about that is um how to get the code from your source language that is great for engineering into a formal setting where you can prove. So all the examples we done so far everything is written in lean.

Um there is one solution to this for Rust and this is going to be an active area of research. Some languages are harder to formally verify than others. There are these tools called Hex and Anias. Um and what they do is they take your Rust code, they compile it down to an intermediate language that they can then interpret in kind of a lean context and then give it meaning back um and they essentially are importing your Rust code into lean. And the idea is that um you have your Rust code and um if you run Hex or Anias on it, then you'll get lean code that has the same semantics. Then you can reason about your lean code. So there that does introduce a trust um surface uh

with the extraction, so you need to keep that in mind. However, uh it is shown like it is been very useful for us in terms of finding bugs. There's this uh cryptographic library that we use in Snerks a lot called Plunky 3 and we started formally verifying Plunky 3 with hacks and um just in the last few weeks found several bugs that have been there for a long time and um that's just through the extraction process. So it may not be perfect and there are lots of caveats there, but um you'll see the kind of proof of its efficacy cuz you will almost certainly find bugs if you start doing this.

Um there's so much more to say about this. Um maybe we should like uh maybe we should have a framework where you can compile down to bytecode and then decompile from there. That would I think be the ideal in my opinion, the ideal situation if we could do that. Then you could have any programming language you like. You get the executable um the binary, you decompile it into lean in a formally verified way, then you can reason about it, then you don't have to worry about compilers and all of these things, then you can have any language you like. That is my personal ideal. Uh yes. >> How does Satoru work? Uh it works with Solidity, right? So you have your spec

and I can't remember what language it is and then your Solidity and then it runs it's like all algorithm to to make sure the code matches. Does it also do something similar to this where it takes a Solidity and then tries to port it into whatever language they use? >> So it's actually um it's a different form of verification paradigm altogether actually. So they have this specification language called CVL, which is Solidity with some logical primitives on it so you can state things and it will compile Solidity down to the bytecode and then CVL down to a very low-level piece of code and then it translates those mathematically into these uh like a constraint system that a solver um if a solver can find a solution to the constraint system then your theorem is proved. It's it's it's they're called

SMT solvers um and it's totally different from theorem proving. So you don't actually write the proof. You have this big gigantic solver that like kind of grinds on it. Sometimes it will time out um and if it doesn't time out it will either give you say that your theorem is proved or it will give you a counter example um which you then kind of decode. So that's um useful but different from Lean. Yeah. Yes uh in the back. >> Okay. So earlier I asked about the spectrum between like propositions as types like you're doing that you demonstrated here and like more conventional

um typed programs [clears throat] like you write in Rust. When you're modeling a Rust program especially using like an ESN hacks um how do you bridge between like the kind of models that you would build in your old fashioned typed program in Rust and the kind of you know nice semantic like denotational models that you might build in Lean. And also I'm just curious about your experience with that like what kind of feel it gives you for that spectrum.

>> Yeah. Um what we find is that um you know we have these big libraries of specifications that we want to formally verify Rust code against. And what we're finding is that those libraries are engineered differently from from the code that we're trying to verify and so there there is a fair amount of kind of bridging you have to do where you basically take the generated code and then you uh re refactor it in a formally verified way. So you refactor and you say this refactor was was secure etc. until you get to a state that you can do something with. These are kind of these bridging lemmas and then it goes up which thankfully it's great that we don't have to do that by hand so much and the agents are very

good at that because um so much work in in the previous times. Exactly. Yep. It you know what? It kind of all comes down to compilers in the end. This what this is the unexpected lesson I'm learning. I think we're running out of time um and I don't want to go way over time. I see there are more questions. Um I would love to take more questions so maybe out the hall or in here or something. >> In the very start the code base which you showed can you show it once again?

>> Oh yes yes yes. This is my bag yes. Here it is. Um and then my X and Telegram handle is the same as my GitHub handle. So if you want to reach out please do. >> All right. Thank you so much.