Formal Verification for Ethereum’s Next Scalability Era / FV and LLMs Together

Transcript

Hello and welcome everyone. My name is Peter Robinson. This is the Ethereum engineering group meetup. Today we've got Molly and he is going to talk about formal verification of the new era of Ethereum scaling. So before you present your slides um can you like give us a bit brief introduction to yourself please? >> Yes, thank you very much Peter. I'm really excited to be here. I've been working on formal method in the last three decades. Uh I am uh I'm really passionate about this field. I contributed key techniques which were later integrated to Microsoft device driver and other things the Facebook uh

system. I'm really really interested in uh providing key techniques that make for verification work. uh in the last seven years together with uh my former student Shelley Gman we started seta and STRA is trying to make formal verification a standard for developer in Ethereum for zero knowledge and this is a contest of here I'm really really excited to after working in this field for so uh long to make this thing available to every uh coder so the idea is we think about it as almost complimentary to testing and other method which has been used and the formal verification has been uh really a

a very good field and the idea I want to bring it from the ivory tower into the fact that you don't need a PhD to use formal verification that's my dream and I can't tell you how much I think we need more to to go but I think we made a lot of step there >> well that that's a an amazing aspiration for having people do formal verification just like they do testing. That that's amazing. All right. Well, look, I'm excited to um hear your talk. So, um I I I think we agreed earlier that at the end of each section, you're going to pause, ask for questions. So, people save up your questions or put them in

chat if you like. And um >> I'm okay. I don't know if Peter if somebody wants in the middle of the section, I'm good, too. >> Okay. I'm I'm good feel I'm very very interactive. I've been interacting for students in all my career as a as a professor. So please feel free. I'm I'm easy with question and I'm also I'm not offended by any question and there's no simple just ask me anything related that I can help and I will pause in the middle of this section as Peter mentioned.

>> Okay. Brilliant. All right. will please present your slides. >> Okay, thank you. Okay, so can you all see my slide? >> Yes. >> Uh, fantastic. So, I'm going to talk about the formal verification. But in fact in the last 4 months I have been learning something that I should have learned way earlier that I learned when I was still in undergrad is how to actually go into machine dive into machine learning. So I'm really excited about combining formalification and LLM.

We are doing a bit baby step but maybe I will be able to talk in this meetup some other times tell you how LM and formal verification can work together. So formal verification as I mentioned is a big field of computer science a lot of results. This is an explanation the idea of having mass reasoning about program and providing proofs. One of the thing that and the one one place that formal verification was used is hardware verification and one thing that people observe in the hardware verification what we observe too that it's useful not only for proof but also for bugs and ina we have been using formal verification to find hund prevent actually 100 bugs before deployment. So that's a big

benefit of it. It's a it's essentially a very very massive testing method that you can use on your code before it's deployed. Formal verification like many field of computer science has kind of a interesting history and I think this is very similar to what happened to machine learning. So it has originally even if you look into the island touring regional work actually it mentioned formal verification and then there are these giants I'm not going to talk about all of them they're very they are giants who actually they've developed the field actually I mentioned Patrick Kusau which is here in New York next to me but many of them these are giant of the field it actually established key methods that

are now the basis of all the technique of formal verification and what happened in 1979 like it happened. There is this one article that I recommend each of you to read. This article is is beautiful even though it's not technical. It's explaining all the reason why formal verification would not work. Okay, it's a very short article. Uh there's two version of it. This one the anyone who's interested in this field and has the gut you should see and actually this result this explanation why formal verification will never work.

there was uh uh I actually tried to understand and they they are valid criticism but this actually where I started my career and I always like to work against I decide because at this time formalification was not very popular okay this article actually did very bad formalification especially in in academia it basically make people think that this is not the right thing to do but then what happened a lot of people my colleague and many others techniques like yax v3 daphne uh lean 4 all of these techniques came and and also we came with algorithm like I came with algorithm for interprocedural and here you see a nice

quote of Bill Gates actually quoting of algorithm that I develop basically that it scales formal verification so we see that formalification is getting way more scalable and the way I like to think of formalification actually this is come in the context of one of the client that sat has a which is one of the biggest learning protocol that basically formal verification is is almost something that allow you to know something about your code. It's go to this unknown. It's go to unknown. It's able to it's it's like testing but usually testing you test for some bad behavior you are familiar with.

But formal verification is supposed to actually test on on behavior bad behavior that you are not are familiar with. and a lot of quotes here is the Vitali quote that basically formalification is a way to increase trust in the code and I think I'm going to be able to show you examples and a lot of people see that you increase trust in the code. So uh as as Peter mentioned I'm going to talk about uh it's a brief talk but I want to cover five things in this talk and each one of them I've done baby step and I love to elaborate. So the first one is what tools are available and I'm presenting here a very very uh small thing specifically to web three talk a little bit about our approver which is

now open source and it's available people are changing it talk about the benefit of formal verification but also mention I I spent some time in industry and what are the challenges in formalification and finally what I'm working on what sat is working now is how to use and I think there are other people working harmonic and other companies how to use LLM to make formal verification more available to a lot of people. Okay. So these are uh this is a comparison of tools. Uh take it with a grain of salt. I'm not presenting everything but these are the three main tools that were used in web tree. Uh uh and actually all of them can be used

outside web tree. So K is a mature tool developed at the University of Forbana Champagne and and it's uh basically used this technology called matching logic. The interesting thing about K is that it can be used for arbitrary thing. You can use you can prove passer and it's actually not specific to web three. You can do everything with it. The user has a control but the problem is K and we have seen it. It's very very hard to use. So it's been sort of used in a in a in a in a very very small crowd and also the the size of the proof the artifact of the proof is big also it's unable to find actually bugs and also it's hard to

get it into the sea. The second tool that I want to mention and I think it's basically a revolution of the industry is lean. Lean is a very recent tool. I think it's 2013 if I'm right by one person Leonardo de Muro from Microsoft now at Amazon. It's actually give you a version that is also called interactive term proof. It give you high high control. Also the effort is medium. The proof size is still big. It's unable to find bugs but it's very useful. People have used it now in mass. People have used it to solve open problem in maths like the oiler problem. It's a very useful tool in Stor. We try to build something uh and uh which is more

catered to where developers and more ethereum specific even though so we actually make it much easier and this means that the user doesn't have the control at the moment we are so so supporting EVM Solana VM web assembly now we are also with the foundation we are supporting Ziki AVM the idea is that the user is not as powerful as lean but it actually the effort is much lower and we are very proud to see people auditor security researcher there's a 100,000 rules written in the sora so the specification is easier there also it's very good for bug finding it's almost like a fuzzer and also it's integrated into your CI okay so question about these tools

before I go and dive into our own tool uh I I apologize that I haven't there they there are more than 20 tools so it's not like I don't want to say these are the three tools and they specifically I want to mention the tools like rock and Isabel which are the most uh and and also if I'm talking to people in Australia the the project is self which is one of the most interesting one in so a lot of things in formification but I presented the thing that we see are the questions here >> yeah um so and it's an interesting one the choices of you know EVM SVM Wom ZK EVM because I know um one of the directions things are going in is to

have ZKVMs that offer risk 5. Um and um I I guess it's it'll be just another language that you might add later on. Um but yeah, I mean it seems like a great idea though, the idea of having lowering the number of things you can change but making it easier to adopt. That seems like a very good idea. Yeah. And also the the bottom up versus top down. So we when we started these people were telling us you're going to design your own language. We said we we said there's no way people use it. So when we started this project solidity programming language was not well defined and we decided to we we don't

want to care. The EVM is well defined. we're going to handle the EVM and we ended up finding bugs in the solidity compiler itself because we we ended up uh uh because the EVM and and and from a verification perspective we make the problem harder because the the we need to reason about the executable and we cannot draft the compiler. So we actually at the moment we are verifying the the version of the executable code. It may look like a mistake and it's definitely a mistake if you want the user to be in the loop. But since we don't have the user in the loop and we only write high levels back. Uh so so this is a decision we made. It's a it's a decision also for modification is about risk and the question is what risk

are you worried about? So if you're worried about risk that the hashing is not perfect then the tools like lean or K will be more useful. We are worried about user mistakes of programs. our our customer, our programmer, they're less worried about bugs in the EVM itself or in the or in the risk five machine. Okay. They're more worried about mistake in their coding. So this is what we decided to attack and and I I imagine the there must be also bugs in the in the ZKVM itself and you can so these are complimentary techniques.

>> Okay, that makes sense. Thank you. >> Okay, are there more questions? Okay, thank you. So how does the Sora prover work and for that matter tools like Daphne work in a similar way? You take the code and you take the spec and you compile it into equation. The difference if you're familiar with Daphne that in Daphne you're writing the spec in the code and in in sto you're writing the spec outside the code. This is intentional because actually the code is written in a low-level language like EVM and the spec is written in a very high language level language and also the fact that the code changes and the spec doesn't change. So it's a decision we made to to make the spec very

powerful and to allow you to have the code which is executable and then we get a mathematical constraints and then there's a solver and the solver either find a proof and the proof usually say that this mathematical constraints are not solvable together or it finds a a a solution he finds a physible solution which indicate a violation of the of the spec. Okay. So that is the idea and and uh we use tools like Z3 which is also the basis of lean and others but we also use others we contribute to them. So simple example this is a transfer and let's think of a simple invariant that the total is equal to the sum of the

balance. It's a very simple invariant and then you see we we encode it as a mathematical formula that describes how the change how the balance is changed by the operation. And then we give it to the invariant after. And we prove by contradiction. It means that we we ask the solver is there a solution that you start from any state that the total is equal to the balance and then you execute any uh transfer and then you get to to a violation. And what the solver is able to do in fact by kind of mathematical reason which is automatic. It's able to find that in fact the balance before is equal to the balance after. and then it's able to look into the environment and it's

giving you a mathematical proof of contradiction. So this means that this environment can never be violated. So this is the ultimate testing and this is the idea. Now if you take a program here with a bug, here's a program with a tiny bug. Everybody knows this bug. But I just want to say does anybody see the bug here in this code? It's a it's a tiny bug. It's a it's a again it's not the bug that you you can probably find this kind these kind of bug with easier than formal verification but does anybody see the bug here so it's it's violate this environment that the total is equal to the sum of the balance sorry to put you on the spot here but I >> yeah could it could it be that um if

balances from is not greater than or equal to amount then balances from could end up being below zero and it might get limited to zero. Is that it? >> Yeah. Yeah. This is one of the problem. But this actually taken care of by the semantic that or or by any equation. This is one of the problems. Not what I'm hitting but this is one of the problem definitely and we can we can find it or but >> in in the chat um ill um said um if from equals to then there's free money.

>> Amazing. Amazing. Thank you very much. Exactly. So this is the idea. You write this environment. You see you write the state change and then you see the solver actually found this. Okay. So it's interesting the f solver finds it. And I know people are using sometimes the approver to do bad things. We cannot prevent it. It's our but the idea is that you find that people are submitting bugs in immunifi. That's great. So the idea is that the solver found here behavior and this is a coroner case and you see it's exactly what it find that L is if L is transferred to itself there's free money. So that's an interesting bug that will and again I'm not saying you can I can show you many more much more complex bug that we found we recently uh

and we find them uh we can find them before deployment we can also find them after deployment by running the EVM we check we compare the spec to the two so we have verified a lot of protocol and people are using it you see some client are using it on their own some client rewrite the spec Ideally we like of course to to make all the spec written by people but it's an issue of skills and and and thing writing formal spec is hard but we are getting better we are getting better okay but these are a lot of client that are actually using this I think it's a success for this field that actually people are able to use this almost on their own so as I said the beauty of tools like

storaa unlike lean and others that is integrated into your CI You actually write this environment and assuming that even when you change the code you you you the environment remains the same you you can check this and be and we see we see developers integrated into the CI almost like a compiler right the testing tool and you run it on every commit every time you have a commit you check that the environment are maintain so for example here the sum of the balance is is maintained Okay. So, do I do you have question about the tutorial prover before I go to other things? There's a lot of tutorial.

There's beautiful tutorial by RSK. There's beautiful tutorial by C3. Uh I the questions about the Stor uh uh before I continue to talk about the the high level properties the question about the Satar prover. There's a lot of also examples. I had a question about the satu and especially because I had people are are are familiar with Daphne I can explain that there are the the similarities but more difference than similarities other question >> uh yeah I have one question um so I'm trying to understand I'm familiar with Davney I'm trying to understand if the sector approver is then more like the

tap compiler that can that is used at every step of the I mean every time that I change for example the source code or is it rather for CI >> you can do it wherever but there are big difference between Daphne Daphne you have your own language that you are verified the Daphne language here we are verifying the executable language second difference is in Daphne you write the spec with the code you write loop environment and things like this in SAR you cannot write loop environment okay the ether because we decided that we don't want to have access to the You can handle recussion of course then you can write environment for recussion but loops we do just bound it we just bound it because our experience says

that most bug that you have is because you have we have inductive reasoning but it's not in inside the code it's outside the court so we made certain decision also the sata prov is is massive like the the daphne is 10,000 line sto is more than half a million lines it's a massive engineering effort so we reason about the code we we try to make it and also the formula that the Z3 is handling. Z3 is handling in the in the set. So it's a it's a huge effort and also in terms of running I mean I'm not it's it's much more expensive we run it on the cloud but it's scalable to work on on on huge thing and find complex thing and it's you don't and in

particular if one methods is calling another method what's a prover will do it will actually infer the behavior of the other method you can of course it has the gadget of of deafne if you want you can emulate deafany we can write things we can write environ But we our intention is that we we don't want you to do the same effort as Duffy. Okay. So we we the idea is to make it as as almost as easy as testing and also the fact that you write high level environment with high order function with things that allow you to write things like you can say for every function I do this thing. So we we uh uh yeah it's a much it's it's a very different and and when you work on it

also we have people who who have been they say it's it's a it's a different it's a different it's a different effort to to work in defined and also we are it's it's it's yeah I don't know if I answered right but I think you should try you see you see yourself actually you should try yeah I think we yeah okay thank Yeah. Okay. Great. Are there more questions? Okay. Thank you. So uh uh then I want to sort of talk more high level and uh uh formal verification uh I think when we started the field I

think the the everybody I I don't know I I I am I'm senior but not that senior but I believe the the story was proof but we figure out quite uh and I think this I mentioned the hardification formification is bugs and we are very very fortunate to find bugs and the nice thing about formification and I show you and you can people see you can find tricky bugs with formal verification another thing that is unique for us which is actually a comparison to Daphne and others that we are interested in code changes so the we are interested to to find bugs in code changes uh uh also about the idea here is that

this is what we see with our client even the ability to write formal spec by themsel is useful. We are seeing that we coming up with with interesting mathematical property and of course this is the original one is the only method that offer mathematical proof of security and last but not last the branding. We see actually that code which is formally verified is more secure. We also see even insurance company we see people are looking at formalification especially in the hardware but now also in crypto that say that something is formally verified.

It's not bug free but it's more secure. So just to give you examples about changes. So these are you see for example this is oil but it's not the only one there's more recent one. So basically one line of change and you see that actually 200 million loss and of course the the biggest story of the nomad beach. So these are small changes and this is actually what the app prover is trying to prevent the case that you change your code in a small way and find the other are the questions about the benefit of formal verification or uh I'm going to okay okay so let me show you one of them but I think we can show

others but the the one which I'm really uh excited about but there are other thing which I excited is the rare box. Okay, these are rare bugs and this is actually the something that even I learned. I didn't know how much you can have. So when we started STOA, we were uh introduced to uh at that time was the most interesting uh landing protocol which was called compound. Are you guys familiar with compound? No. So compound is is a landing protocol. one of them and basically we came to audit the code after all the best auditors and we run this tool that our tool was baby step and the tool

found a bug we did not believe it's right but we were smart enough to tell the founders and actually this bug allow you to take all the money in the code okay and it was so this is the idea so how do we find these bugs of course you can do manual auditing and other thing but the idea here you write high level property in this case you see I write invariant solveny and it says the underlying balance is greater or equal to deposit okay so rashio if you compare it to daphne this is something that you write uh outside the code you see and the the intention of this is to say that this is for every API code so this is actually you say and and this is a

property that you want to check okay it's a for every so you don't write in the code. Actually, sometimes you even don't have access to the source code. Okay. So, you you only write this thing and then you check this property. Okay. And you check this and the prover check this property on every of basically it checks it every time that that so it's like a global environment. This is a property that always and of course there are you can make it inductive like Davney and others but the idea is you want to make this tool automatic. Okay.

And you see here a snapshot of the tool. It's a hard to see because I put it from the snapshot from the and I apologize, but if you run it, but you see here the trace. You see actually that it goes from a green to a red essentially it give you a trace. It's a it's a and it's interesting. It's a trace that if you want to run it concretely, I think you're going to have to have zillions of operation. It's very very deep bug. But the tool is actually that's the beauty of formalification also in Daphne it doesn't start from initial state it start from an arbitrary state it start from an arbitrary state that satisfies the invad into a state which is violating in the same thing that we have seen in the beginning part of the

lecture so it find this bug okay and this bug is tricky okay and if you want to look into the code uh I wouldn't judge it but in fact here the the the the bug is actually interesting The idea is the developer here was not aware of something that actually this is already accounted. It's a it's a it's again I'm not an economist but the idea is there is financial there are shares and there assets and the relationship we ship with them has to be maintained. Okay. So it's interesting this is this command is the the developer mistakenly didn't understand that this command is actually redundant. you should not be there. But if you run testing, there's no way

you're going to find this bug or you will, but you need I think tons of iteration if you wait long enough maybe. Okay, so that's the idea of it. And when you fix it, the interesting thing this is testing cannot do. It can give you mathematical insurance. It doesn't tell you that this code is correct, but it tells you that this code maintain the solveny. So every time you start with something satisfy the environment, it's it's a it's a it's a if you start from a state that satisfy the environment, you end up all you also end up in a state which satisfy the environment. So the environment is maintained. And this is the idea. This is how we work in tools like prover. We write some necessary

condition financial or other and then we let the prover find a violation. Does it make sense to especially for people people are familiar with Daphne? It shouldn't be very very foreign. It's a It's like Daphne but it's much more high level. It's much more high level but it's like Daphne. It's inspired by Daphne and you're familiar with tools like lean. It's like lean but you don't write the proof. You only write the spec and the proof is done in internally. Okay.

I'll continue. So I'm almost to in the end. So [clears throat] I want to actually uh tell you something about uh again I've been in this field uh quite a while. I think the field is making progress but still even I mentioned that we have 100,000 wolves which is amazing but I don't know the quality of them and we have seen cases that people even with the prover have proved property and after that people find bucks and the idea the reason for that and of course with other tools as well if you don't write goods back your your the then the issues how do you write goods back how do we come with these properties the

other problem that we have seen and it's kind of weird that the saturator prover finds very interesting bugs but sometimes it takes us a hard time to understand the knowledge of the bug I already mentioned compound that the tool found a bug but we didn't understand fortunately the compound developers were able to understand so how do you diagnose the f result if you're familiar with tools like Daphne and lyn this problem is even worse there and the the the last thing that happened is how do you scale it formal verification is useful not for tiny code it's useful for complex code and we have one solution that uh Satra came with and many other teams are doing the same thing we solve

all of them with hopefully I'll be able to tell you more but the ideas that we are building this open source tool called AI composer and I think a lot of teams are proving other thing the ideas everything we do with with with LM so for example the property of this solvency we have been able to to get use the LLM and interestingly if you even look into charg it's pretty interesting you point to the manual of the sora prover and there's enough think and it does well it doesn't replace us completely but it does well even more interestingly what happened when the prover finds a bug I show you this trace but it's hard even for us to

understand what it means but what you do You you take this trace you convert it into a transition system you and then the LLM actually find explanation of the bug for human it's amazing actually I I I was not a believer in for inm but I I see that uh I was completely wrong okay I was completely wrong it's very interesting the LLM can take tools like Satra or lean or Daphne or all of these tools and push them to another level and people are already doing it with and without And we are now using it for coding agents. We are developing actually new codes with the prover. So the idea is you you actually infer the spec and then you actually then basically what

happened when the when so it's kind of weird. You ask the LM to find the code. It does it produce the code but it produces with with buck. You ask it to to find a spec it produce the spec. It produces with bug. to ask him to produce two of them, two of them together, it does a better job. Sometimes solving two hard problem, it's easier than solving one hard problem together. It's kind of interesting. We also use the LLM to scale to larger system. So the idea is we we work on the on the module boundary instead of the LM breaks the system into components and then it applies the the proof at all level. I think it's very interesting. It's a it's a very

interesting uh domain for formal verification. I I speculate that in a few years we're going to see with the formal verification in an in a completely different place. Other questions here. I I have another question. Well, maybe please let me know if maybe this will be answered later. But so you mentioned that for cera the the specification is separate to the code and possibly even written by people who doesn't have access to the code.

So, how do you make sure I mean I guess that doesn't allow you then to to verify I mean to know it to even know what kind of things or yeah doesn't give you a lot of things to to work with to verify right the small details about the the business logic let's say uh if uh it's very possible that they will get lost in the assumptions in the manual in the mind of the programmer, right? Um, so what does Stor rather go for the bigger details of the system? Uh, do you know what I mean?

>> Are you are you referring to in in formal verification we sometimes talk about soundness versus completeness? So soundness means when I prove something, is it correct? And completeness means that there must be something that I will not be able to prove. So which one are you worried about or or is you're not worried about either of them? >> I Yeah, I think it's different. It's more like for example in the example that you gave about this um uh the the example that you just showed about uh >> solvent solventry.

>> Yes. Yes. um that okay let's let's just continue and let's see if if >> no no but I think to answer your question everything that we prove in Satra it's guaranteed to to hold the idea is that what will happen is that we we make the assumption first of all you could have access what we make the assumption that people are interested in the in the in the behavior of the code from external behavior so you write this this thing about the court you are you are absolutely right that sometimes that's issue of completeness that maybe there is something about the code that you won't be able to prove with the sat

prover because we didn't give you the right access in particular for example we are not reasoning about god's consumption and that's a conscious decision that we made because it's it is changing all the time so this means that when we prove for example suppose you have a command that is execute five times. Okay. In Sattor, we assume it's execute arbitrary number of times. So we ended up making the formal verification problem harder. So we we we we we think it's a a good thing because we we don't want to to make your code so that if the gas changes. So we ended up making your code more secure, but we think it's a good idea. It's a it's a

conscious decision that we made of what you want to do. And there are some cases that you if you have code which is too low level maybe but we are handling assembly code we are proving properties about a lot of things. So we we we ended up making certain assumptions also for I mentioned already that think of hashing hashing can be imperfect like the idea is that you have two hash and and we are not proving something about the hashing because it's not has nothing to do with the code of of the program. So usually in in in formalification we we have this notion called rely guarantee. So there is some kind of assumptions that we are integrate but we are not checking them. The these are

assumption that you have to prove it in pen and paper. Okay. So it's it's a it's a it's a it's a conscious decision that we made and so far it is it's working well for us. we are able to prove we are unable I can we are unable to to we are able to prove what we want about the code uh but yeah makes sense I don't know but I think I think the the point of this thing is that no matter what working with tools like Zapne or or or Sattoru is hard and I I I enate this problem I think Daphne has more and what I want to say here is that each one of them we have a solution now is coming with LLM

and I'll be able to elaborate. So we have a solution with the LM that we can infer specs and it's getting better and better. It's getting better and better and we are it can be used either with with existing LLMs or also training your own it can be and also diagnosing the result once the formal verification say in in our system the approver can also and like DAN it can tell you that it's right and it can tell you what it's wrong okay and when it tell you that it's right we can produce a proof when it tells you that it's wrong we can use the NLM and pro provide an explanation of the hack and that's a very interesting idea and we have seen it

internally we it's saving us a lot of time because stora is providing professional service for team to use formal verification and instead of spending two weeks in finding the issue we actually let the spending few hours in finding the issue >> okay >> thank you >> good so I'm a ending my lecture. I want to just finish in a in a very very very high level and again this is experience of somebody in this field and I think the uh uh some of it is is uh uh known but I want to see that there are a lot

of myths about formalification. I'm not writing all of that but one of that that people already saying is that formalification produce a bulletproof code. We know it's not the case and there there could be bugs in the spec bugs in the underlying system. We have seen that uh with Daphne with lead with our approver and we need to understand all the time what's the text another thing that people especially in the web three space that people thought that formalification replace auditing or testing or fuzzing it's a complimentary method in fact formalification is useful in the auditing another thing that we've seen uh especially a lot of team

proposing to run formalification is the last We don't believe it's the case. We want to write formalification as the first thing. We want to ideally actually write this back all the time. And in Shatra and we have seen uh other teams mentioning that you need to be the word expert in formalification especially in web three. We don't think it's the case. Of course we sell professional service but we love the fact that people are using the prover. I encourage you all to use the proven actually other tools I think also tools like lean is getting more easier to use.

So I believe that it's actually used by developers. We also see security researcher, white hackers and we are making the tool easier and I mentioned that if we did a great job but we believe LLM will do even better job than us and actually now you can use you don't even have to read our manual. You just download the tool, you start and actually it's very interesting before this talk even for this lecture I ask and the LM is is is actually able to to come with almost everything and actually answer many of the question. So I'm done with my lecture and I'm happy to take as many question as you have.

So I'm just trying to think through um a um so a project which is going to so what what a complex project is when you're say migrating from one type of contract system. So, if you've got contracts that are not upgradable and um you're going to need to hard fork them to um change them to a different contract and essentially upgrade the where the storage locations are for the ver for the the um storage in the contract. So imagine you you um go from

one type of ERC20 contract to a new type of ERC20 contract and the storage locations for balances for instance is changed and so you know someone writes some say Rust code to move the balances around. How would you go about formally verifying that with Centtor approver? Is that something the sort of thing that you could um formally verify? >> So that's very interesting because we build this uh tool which is actually now will be supported by the Ethereum foundation. So I mentioned one of the biggest problem forification is coming

with specification but this is a beautiful example because you need don't need specification you have equivalence. >> So we have we build this tool concord and it does exactly this. It's essentially you don't write spec you take two pieces of code you check are do they behave the same and they can be one of them is env because they are all we are checking things at the executable level and we have found actually bugs live bugs in the we compared two different version of the compiler so we took the same code we run it on version one of one of the major compiler and version two and and actually it's a live code and we find a bug in it so this is a new tool which are coming it's uses

the same technology but it's easier to use. It's actually already available in our website. It's called concord and you can use it exactly to do that. You can check and and the ideas you one question is how do you define equivalence between this r and the solidity code and we usually define it in terms of the two thing the observable behavior from outside and the storage. So in fact we we are doing it we are doing it and we are using it internally and this is a big good usage of of of formal verification is checking code upgrade checking migration from other thing we I think Microsoft research has started this thing Microsoft research but we are doing it in satura there's a

project that will be funded by the foundation that actually this project is actually and it's it's meant to be used as a as a sort of and people are using it also with LM because the idea is you have a code there's this library called so lady I don't know if you're familiar with so lady is a very complex library >> so the interesting thing even ask and the prover get very hard but what happened you ask the LM to simplify the come with a much simpler version how do you know that it's correct you run the equivalent checker and it tell you that it's not correct and then you give it to the chart GPT the charg say say okay ch give you a better program, you run the prover again and then it it's it give you another problem after three three

times the chat get it right. No. So the interesting thing you you you wrap a loop around the f and you and I can show you it's beauty. The the end result is fourline program >> that is beautiful and it does exactly what this complex executable library. Okay. And you can go both way. You can go from complex code to simple code and from simple code to complex code. You take the I don't know that you're going to get the so lady but sometimes you get something more interesting. You take the simple code you say how can I make this code more gas efficient and the LLM come with beautiful ideas but some of them they're

always 80 or 90% right but how do you get this extra 10%. So this extra 10% they prove it. So I want to think of the LLM is somebody very like I don't know if you think I think always is the the idea of dyster there is this good guy and bad guy. So LM is like the magician and the formalification is the demon the demon [laughter] the bad guy. So we run the magician with the demon. The demon the magician say all right find this and then the and and the both work very well together if you have enough money to pay the token to to this fee and but it's it's not very expensive actually. I think it's like $1,000 you pay to this provider and you get this.

>> Mhm. Okay. >> So it's actually great usage. It's a great usage of the the technology. We have been using it. We are seeing team using it. So it's it's a yeah >> okay that that's that's great and uh well I'll have a look at if how to >> code is there. I'm also I don't know if there is a place that I can share. We have a lot of documents. We wrote a technical because we ended up actually doing something pretty clever to how to to basically the idea is we instrument the program in a way that make this we have done some things that on the surface they don't make sense but for us they make a lot of sense. So we basically make the idea so we we make it

so this is possible to do this. So basically we have a tool you can think about it a diff. It compares between two pieces of code and it can check you and it compare between two different pieces of code which may be written in the same language or different language as long as they compile to a representation and we have our own internal representation I haven't explained which is called t it's a three others code it doesn't it's very technical but it's actually it's a uniform representation for all programs. So it's a this is how we handle WhatsApp SBM and so we build it once and it's like mathematician every time you give we can actually build and from that we have a reasoning tools we can do this

thing. >> Interesting. >> And I have another question. Um, so I I guess that with Concord you will also have found the compiler bugs or >> we did we did and they acknowledge Yeah. a experimental version. Yeah. And we we want to integrate it into we're already integrating it into the Viper compiler.

Hopefully we'll integrate into the solidity. Uh we also we are actually starting start getting to code which is not smart contract. We are trying to talk to the Vas Foundation of Vas because it's it's even though it's developed in crypto but it's it's for code it's a it doesn't uh anytime you have code of course it has the limit if you give something very big it's the usual limit of for verification is scaling to to bigger thing if you work on the function level it's great but if you if you give if you compare two 100,000 lines streaky these are very expensive algorithmic method and and we make we especially if you reason about

storage and we have some ideas that we can uh essentially uh recover reads and write and and understand because we are reasoning about low-level code so understand when two memories and that's another difference from Daphne we we understand if two me piece of memory are disjointed so if they are disjointed you don't need to reason about but and and it's it's a conservative algorithm which means that if we prove it it's right but sometimes we're unable to prove it so we have to use the vanilla version. So this means if we know how to reason about your program it will be faster and if we don't know the the tool will be way slower because these are hard algorithmic questions.

I I I think I remember that uh one way of uh I mean there was some either some paper or even some tool that to discover and define behavior in C they were compiling um with in different ways C code and comparing the where the the yeah the compilation had diverged. So I assume >> that's a very similar >> that's a very similar that's a very similar the only difference is that now we have this generic technology that using leverage the SMT and formal verification but yeah it's very similar it's very similar and uh yeah and and

also yeah it's very similar >> okay thank you So, one thing that I was pondering was, you know, if you does does your company like have a have a sub team that goes off and tries to do bug bounties cuz, you know, you could fund your company by doing bug bounties and getting, you know, $50,000 here, a million dollars there from bug bounty programs potentially.

>> Yeah. Yeah. We don't do that because uh I think I don't want to go into trouble. I'm no longer I used to be the CEO. I'm no longer the CEO. But the idea is that it's not aligned with our clients. >> The problem is that we we it's it's a good source of revenue definitely. But we if I if I if you pay me to prevent bugs uh it's I cannot uh we made a decision. We made a decision that >> we are so even if for example a client >> will decide to stop our service and even if we find a bug after that we're not going to submit a bug bounty we're going to disclose it privately that's a decision I mean the employees sometimes

don't like it but it is what it is [laughter] the the the decision we made is that we are we are to the client and and even if they it's a oneway relation It doesn't matter and it it's it's been actually useful to us because we see a lot of we are the company that has the lowest churn. So basically most client that engage with us I think 99% they stay with us. So so the idea is that people know that we are and maybe we did a good job in the spec or did or we also providing manual audit without formal so but the idea is we are aligned with them. So the the idea is if if we find a

bug bounty with or so if we find a bug either with approver and or with human we submit that with and not requiring the bug bounty and and we have cases that we propose back bounty we decline it. More interestingly there are a lot of cases that client comes to us after somebody submit a bug bount and in some cases we have to tell them that yes we messed up but in other cases there will be cases that actually we went the prover and the prover say it's right so we explain to the to the hacker that he was wrong and we save the client money so so the yeah we are working with our client in uh in uh in uh basically diagnosing bug bounties and and and and

either we see that it's correct correct or not correct and trying to but there are other companies who are submitting bug bounties it's not what we do it's a conscious decision that we made also it's a very different we made decision for good and bad to raise a lot of funding so that's has this advantage but it has advantage so if the monies that we are using is the VC money and and that has its I'm not going to say >> yeah yeah but you can you can decide for bug bounty does not so even when we submit a bug that was not found by tool and I I know that people have submitted I've seen in Immunifi bugs which were found by the

satov we of course it's an open source tool it's you you >> yeah yeah well I'm thinking that yeah I mean you could imagine a lot of people like maybe they can learn to you be very proficient at using satura approver and then go off and you know like look at all the projects and maybe they can make some money. But uh >> No, no, that's good. But we we are we are we are we are a service company. We product >> and we have a retainer with with your team to make sure that your code is right. So we we cannot and we are at the moment I don't know more than 100 people. So you will assign Bob Bob to to secure your code and and and and John

will find it's impossible. So they're going to leak this information. I mean sometimes we have engagement with the client that last over 12 weeks. So this mean during this process we understand a lot about the court. So we we we we probably have an advantage on on somebody that has a back bound. You understand? >> Yes. For sure. >> So so we don't do it etc. But and but of course it's it's a legitimic move but not for us. >> Yeah. Yeah. For sure. Okay. That's good. Are there any other questions?

Okay. All right. Well, look, um, what we what I'm going to do is I'm going to, you know, um, we're going to put the recording up in within the next 24 hours and, um, Mully, I'll I'll tag you. Your, um, slides, PDF of your slides will be linked from there. And so if anyone's got any questions or anyone who's watching the video has questions, please put it as a comment on the slide video and um you know we'll try and um work to have the con the question answered um or could I guess could they try and reach out maybe on LinkedIn or >> LinkedIn, Twitter, email uh also like uh

in academia I'm pretty easy to get in. I have also weak pronunciation of my name so you can Google me. So I think you can get easy and also Sattor has a discord server but you can get it's pretty easy to get a hold of me and don't feel like you have to uh ask me you can ask me about Daphne or or or lean or other things it's yeah of course I am biased for such but but you can uh you can ask me on anything I I'll I'll try to to answer and also I mentioned we have a big team and yeah also interested Now in ZK like using this uh actually reason about ZKVM equivalent of EVM. I wasn't

able to maybe maybe uh actually just uh if I can I don't know if it's too late. >> Mhm. >> I forgot something uh to mention uh wait a second. I don't know if it's too late. Just uh I forgot the the three thing. If it's too late >> here's what I want you to take from this lecture. I hope it's okay to if you have I think I want to tell you three thing one thing which I think is amazing which I wouldn't believe you can do forification at the executable level this is what su put but I think I I learned that in my career if you can now you can build something else the other thing is that these are perfect

technologies and I haven't talked about zero knowledge because but performation is a technology to get uh the uh to build trust in the centralized application. But the last thing and that's [clears throat] actually very interesting that I only hinted on that but I love for you to invite me in one year or two year or whatever when if I LLM is is is going to make forification looks very different very soon and uh and so that's uh and I I only hinted at that I didn't prepare enough but I will if you give me even three months four months I'll be able to show you that a lot of things that many people including myself thought it's undoable they are

doable. So these are the three thing I want you to take from this lecture that you I know tools like Daphne or they think of formal verification the high level which makes sense verifying the design or verify and that's very useful because you find bugs earlier I think formal verification of the exclusive will also make sense and that formalification is a technique to increase uh uh increase trust and last the LLM. Okay. And thank you for having me. Thank you for having me. Yeah. Well, thank you for delivering such a great talk. It's been very much appreciated and thank you for everyone who's dialed in from across the world. Um, yeah, have a great rest of your day, Mully, and have a great

evening and night and daytime for all the other people on the call. Right. Talk to you later. Bye-bye. >> Thanks a lot. Thank you for hosting me. >> Bye.