Using LLM Generated Formal Specs to Prevent the Next DeFi Hack

Transcript

[applause] >> Thank you, everybody. Uh it's lovely to be here. Uh I hope you can hear me. I have have been in this space for quite a while. Uh I have been in uh industry for a while and academia. I've worked in many things and I think actually this is by far one of the most exciting work I've been doing. I am very very excited. All of these things related to the stock, all is actually online. I love to get question either during the talk or later.

I think it's something very interesting for this domain. I want to actually understand how many of you are coders. Uh some. Okay, so that's the talk for you. But even if you're not going to code it, you hopefully you're going to enjoy. Stop me with questions. Stop me with questions, please. So So this is kind of obvious to all of you at this point. Uh software and I'm not actually talking about necessarily smart contract. We have been applying it in many domains. So there are different problems that call all kind of objects, but we need to understand coding agent are replacing software. Even in Cetera, we work in very complex code. We have many many engineers with PhD in computer science.

We are seeing that coding agent are getting good in doing good things, not as much as we. Also hackers are winning. I don't I mean, we already told you hacking are winners and they're winning because they're some of it we're using the AI. And we have fantastic auditing firm including auditing auditing firm since Cetera, and we have a lot of tools, but even with the tools and the excellent auditing, we are not able to find all bugs. And some of them are in the code or not in the code. And even worse, if you think that today the situation is is worse, tomorrow it will be even worse because what happened is that every time this

company say open AI, I don't want to they release a new model, there's a new spec. And on top of it, the code is getting way and way more complex. So, who can stop it? And we know companies Anthropic AI, they have this idea of intent, but they're thinking of intent in an informal way, and we think it's not the right way. We it's not the right way to think of to to to think of intent in an informal way. So, our solution is Agentyc formal verification. How many of you heard of formal verification?

Some. How many of you heard Agentyc? A little bit. So, the idea is formal verification is supposed to be hard, only used by PhDs or whatever, and I heard some of our competitors that say you need PhD for formal verification, it's nonsense. We want to make formal verification so that it easy as testing. And in this talk, I can show you that it is not necessarily as good as produced by others, but in fact, we have technology that will eventually make formal verification as easy as testing and very very accessible.

And okay, if by the way, if you have questions, I have mechanisms so please stop me and ask. So, the okay, I'm getting too excited. So, a lot of things formal verification, I'm sure you know, it goes back to the 50s. A lot of work, a lot of people giant in formal verification, like any other field, there will there was the case that every everything it will solve everything, and then say it will solve nothing. It's all the case, like AI and many other fields. And there are many many myths about formal verification.

And the biggest myth, and you see it many and many Ethereum talk, they will tell you that formal verification is intractable. It's a very hard computational problem. And they even have mathematical way that say that it's not solvable. This is nonsense. Because we and others find way to make formal verification feasible for many things if we know how to do it. So in fact, the computational problem of formal verification is not what is hard. So what is hard about formal verification? The idea is that the problem is that formal verification and the other myth that people have, and it goes back to Knuth and other that say, "I formally verify the code is correct." Okay, so you'll hear a lot of people say, "I don't need testing." I mean, I don't know if you know, one of the giant of

computer science, Dijkstra, he said, "Look, you don't need testing, you have formal verification." His of course was one of the most genius people, but it's completely wrong. The formal verification, the quality of the formal verification is really depends on the formal specification. So if you don't have good formal verification specification, you don't have formal verification. And a lot of teams they say they formally verified and it get hacked. Why is that? Because they haven't formally verified the right property. Okay? If I tell you that I I can go from here to here, it's not necessarily say, maybe you have another property that you care about. So the biggest problem of formal verification is actually formal specification. And this is where company like Certora are using a lot of smart people and others.

And this is where LLM will help us. Finding formal specification. And I'm going to show you baby step here, but that's the idea. We have a tool, it doesn't yet replace us, but it's actually find you formal specification. Okay. So how is this tool going? You're going to see later the UI, but the idea in that actually the tool is releasing now. It's going to be basically token based, and all the software is open source. So the idea is you write the intent like in the same way that you write the intent when you work with Cloud or others. You write the intent informally. Okay, so here is a thing that you say, "Keep the balance safe."

This is an informal statement. And then the the the tool will automatically come with the invariant. It can use our tool, it can use others. And the invariant says, "The sum of the balance equal the total." So, the the invariant is formal. Okay? And once we have the formal spec, we can use the prover, we can use testing, we can use many things. So, the idea this tool it bridges the gap between the informal spec and the formal spec. Okay? Okay, that's the idea. So, it goes from the from the developer write the intent, then you translate to formal spec, and then you verify it, you test it. This tool, of course, applies me on formal verification. It applies if you want to do testing. It applies if you want to do many other things.

Okay. So, here I want to again one of them, I'm sure all of you know, but this good friend still a living computer scientist and and a friend in Stanford always say, and this I like this quote by Don Don has many, I'm sure all of you know them, right? And you know of his work. So, basically what I want to say, in addition to formal verification, we also want to do testing, and this tool helps you do testing. Why does it work? Okay. So, how does it fit into your development cycle?

So, honestly, we don't know yet. We are starting to develop it, and we need you. We believe that the industry, at least in the smart contract, is built on auditing. Maybe this tool will replace auditing, we don't know. At the moment, we are thinking about is a tool that you use before the audit. Okay? So, you develop your code, you test your code, and then you use this tool auto prover before the audit. And this tool increase your security. It's not instead of auditing. I don't care if you decide, but I do is it it's in addition to auditing. And what do you do in this tool? You start from the properties, which are written informally, and then this is an interactive process. You need to talk and I'll show you. You need to talk with the human and find out if in

the the hardest part is actually getting the informal properties right. And this is where you need interaction. And maybe eventually LLM will get better, but at the moment you need some interaction. And once you get that, you got into the formal spec. Once you get the formal spec, you can use tools as on other to get proof or to get bugs. And of course, when you are done, we think and maybe in the future it will change, you need a human. And the human review the code, review the spec, review everything. And if the human say it's okay, it's deployed. If the human like an auditor say that it's not the case and you agree with it, you have to repeat the process.

So, this is how this tool fits into the development cycle. Inside is a pretty complex code. At the moment, it's about 10,000 line in of Python. We are actually rewriting it in in the Rust. But the nice thing about this tool, many of you know we have developed the Cetora prover, but it's actually agnostic to the Cetora prover. It can work with any technology. And it in fact is not even needed only and we have We are not of course AI. We have a lot of respect, but we have a lot of understanding of engineering and we have done a lot of things to make this tool very very agnostic. And this tool actually advance the state of art in AI.

And what it does, you start from the design document, you start from the spec, and you actually This is actually one of the most interesting thing about it. Before you do anything, because what has happened to us at Cetora, we are consulting company. We are providing service for companies like say auditing service. And sometimes we come to the client, we go on a call, we tell them, "Is this what you're building?" We say we wish if you knew it before, we would have write the code for for completely. So, we this is where we help the guy. We help them strengthening the design. So, we make the tool more we make the design more amenable to formal verification for other things. So, this is what we call hardening the design. This is an LLM agent

and it makes the design more formal verification ready. And you can use it as early as possible. And you just take the document. I don't know if some noise. Hope you are okay. And then we go of course to audit agent. There are a lot of agents we can use us, you can ours, we have ours. There are a lot of other team that have the audit. You can plug in your audit agent. And and basically we get the security review. We extract the informal specification. We have the informal specification. This is what we could talk about early. From the informal specification, we go into with the formal verification agent, we convert it to our own language or other language for writing formal specification.

And then we actually try to produce proof or produce bugs. We can use any tool. At the moment we are deploying it with different tool. Rock is a tool is academic tool. Actually used to be We are using it. We are also using lean four which is a standard by Amazon. We are going to use almost which is based by A16Z and we going to build use our own prover. And of course we want to deploy more and it's easy to deploy more. It's open source, you can add things. So, this is the idea. And we believe this get your code strong enough. Whether it's it's subsume auditing or not we don't know. It's remain to be seen.

Let's show you two examples and then I conclude. I want to show you two example. One is a toy example. I admit it's made. Other one is actually one of the most interesting protocol in this space that we prevented an issue. So, I want to show you both and please bear with me. So, this is how we apply to toy examples. We need to apply to to more examples. Okay. So, this is toy example. I'm sure everyone has seen like a ERC. It's a counter. It has a bug. It's a trivial bug. Anybody could see the bug. Here you see it's not using the parameter. It's a trivial bug. It's just illustrating example. It's not a very sophisticated.

You can find it by any tool. But the interesting thing is that once you have a fix, we can actually validate the fix. That's a big difference between other tools. But any tool will find this bug. So, let's see what you do. You see this is the agent. The agent is actually small is talking to you and you see it's finding these properties in English. Okay? And actually you interact with it. You see all the thing. You interact with it in English. And then you have this collaboration. Then you translate into a rule. You see it translates into a rule. You don't actually need to read the rule. If you want you can read the rule. But in fact, the more interesting thing is the informal spec.

And then you have the property. So, you see here it proves the rule that it generates. It proves three rules. It out of three rules. Sorry, I I apologize. I get too nervous. Out of three rules, two were verified and one is not verified. Okay, you see that. And there is a bug. You can look into our UI. Our prover has a UI that explain the bug. But you can also look informally. Informally we tell you what's the bug. So, you actually don't need to actually understand the inside of formal verification. And this is how this tool is used. You actually use it. And of course it when it finds the bug, it could be a bug in the code or a bug in the spec. We really don't know. And you as a human, you have to justify. Because in fact, it all what it finds, it finds

the deviation between the specification and the and the code. Okay, you think about comparing the formal specification to the code. Uh so, this is the idea. You see that it's it does this thing. Okay, and you see here you have this property. You see eventually when you fix the code it actually can have the the surface of the bug. This is the the UI of our tool. It's a bit hard to read sometimes, but people like it. But, you can have You can have also informal. You can look into UI of our tool, which is like a debugger, or you can see it informally.

Okay, that's the idea. What am I showing you here? So, it is property violated. And and there there is conversion. Okay, wait a second. So, am I Yeah, so now you fix, you see that the code is fixed. The code is fixed with a simple fix in this case using the parameter. And in fact, in this case, it can prove the property. And that's a very different with LLM, because now you know that the next version of LLM, you know, meters will not find a bug, because we have a mathematical proof that this code does what it's supposed to do.

Okay? Okay. So, what about real code? So, we we'll be honest with you. We've been playing with this tool for about 7 months. We have applied for some real code, uh in particular, notary RVV4, which is a code we have been applying it to want to apply it more in real code. We want to apply to more real code on blockchain and more real code outside the blockchain. So, this is an example. It's a real example. We have anonymized it. It's one of the interesting protocol I want to show you. And it's actually a code which is not a bug, because Why is it not a bug? Because it's a code which is not deployed. When the code is not deployed, even if it's more interesting, it's still not a bug. So, I want to show you what it finds on the code before it's deployed. So, this is a bug that

the tool prevented. Okay. So, this is a real-life example. You can probably figure out, but I tried to anonymize enough. So, you see, this is a real-life example. And it's a I basically we took the code, we gave it to the LLM. Of course, we also gave the design document. We gave everything we have. We didn't give any rules. And this is a project that we were about to audit. We didn't before the audit. So, the idea is we usually in the audit we have a team, security researcher, formal verification. Before anybody look into the code, we have the LLM look into it. Okay?

So, let's see what the LLM does. So, the LLM come with the properties. Okay? The LLM come with the properties. It come with a 15 properties. You see? 1 2 3. It's coming and maybe I can tell you what it is. Uh uh you you guess. It's a How do you call it? Like a uh uh mechanism to do gambling or to do some kind of again, you will figure out if you want, but it's a mechanism to allow you to to to gamble on money or something like this. And it figure out some properties of gambling and it figure out actually interestingly some properties of it. Again, I'm not saying that these are as good as something that we have people in in Saturna that has a lot of experience in this case. But it's something that is a step and it's done completely automatic. You can refine it.

It's done completely automatic. You see these are It come with 15 properties. Okay? And maybe I want to say the last one, which is simple, but it's actually people in this domain understand it as a as a as function. When contract is paused, executing invoked by session, signer must leave well. So, this is some condition. In fact, we have seen hack that happened like this. So, this is actually some condition that was actually identified and it's identified automatically by the tool. So, this is a property that you see was inferred.

Okay? And and so, this is a a property that that it's it's inferred automatically by this tool. And then, what happened? It converted to a real uh thing. That's the LLM. And in fact, you see the LLM is finding a a violation. The LLM finding a violation. In fact, we confirm it with the with the kind that this is actually a violation, which is a real bug. And in fact, it's also the LLM also inferred the fix. The LLM inferred the bug and LLM inferred So, tell element first the spec in the same severity. It's actually interesting. It tells you I will use the C the tool approver.

And then it says it it says what it does. It applies that. Actually, it doesn't even need us. Doesn't need us at all. It's all it does here. And again, I'm not saying but it's interesting and I think we can do it for lending protocol. We can do it for more and more things. Okay? Uh what am I showing you? So, here is the fix actually you see it's actually show writing you the the suggested fix. Again, this is not something that you need to set to a but the interesting thing about this is that we can validate the fix because we have a rule that actually can give you a formal guarantee that once the the fix is done, this rule is not violated. We have a mathematical guarantee that under all scenarios, this rule holds.

Okay, so that's the idea. I don't know what I'm doing showing you. Uh okay. So, what is the status of this tool? So, we have this tool available now and it's only at the moment for Solidity. We are negotiating with other people to to develop to develop it in Rust and others. It's also GPL 3. It means you can contribute. It's the same thing that we did with the prover. It's and it's Solidity only but we are thinking of Rust uh and other things. Also, another thing which is interesting about this tool, I showed you formal verification but we are not against testing. It generate test. It generate test. It just generate test in Foundry. It will generate test in other things. It generate test.

And also, we wanted to launch a product. We are always not so good but let's see if we can make it. July 15th is our deadline and please there is a list that you can register and the difference between this product this product actually leverage LLM. It's agnostic to the LLM but at the moment we only support several one of them. And by By way, this tool also include bug finding including static analysis, include many things. All the things that we did in Certora in the last four years, including, of course, uh rounding errors, everything we did, we put it in the same basket. And it's all open source. We put everything. We are betting on LLM like many other companies. So, we decided to put all the tools together. It None of it is perfect, but we'll get better. So, this is coming July 15th, and the idea is we

want to prevent many bugs. The pricing is very simple. We charge the tokens that we We have, and in fact, uh it seems like AEF will want to sponsor some of it. It's not us. So, we The idea is that we will charge based on the tokens. And of course, we So, this is basically the idea, and I can tell you a range of pricing. At the moment, we are talking about $300 per run, but we want to get it lower. We want to get it lower. The idea, and again, this tool, hopefully, will not replace our professional service or any other people on the team, but it's a beginning. And it's a beginning for this domain. And I'm sure some people will abuse it. But, that's that's the tool.

Okay. I think I'm Hope I'm going doing good good on time. I want to actually take take away from it. I think for this talk, there are actually two takeaway that are very interesting, and actually, they are surprising even for me. The reason that people care about I work in formal verification, I'm sure you can see from my age, for at least 35 years, maybe more. The reason and the reason that now we get all the VCs, whatever, interested in formal verification is AI. Because they say, "Look, how are we preventing all these bugs from AI?" And you know, of course, we have competitors Harmonic Axiom whatever.

We have actually tons of competitors, which are amazing team, raising huge funding. Great. All friends. It's fine. So, there are a lot of competitors coming to this Every speak, we have every day three companies coming in formal verification. It's great. Because people are trying and also internally, amazing team, Amazon, Google, all of these guys trying to to use formal verification. It's great. So, the idea is that these guys are trying to help against the hacker. The other thing which is interesting about AI, not only did it makes formal verification useful, it's actually helps you make formal verification easy.

And it helps in many, many things. It helps in making the prover easy. It happened to get I show you how it will get the spec, but I haven't shown you that one of the thing that this tool does, it helps on internally. We have these stories that the prover our tool found a bug which allow you to completely deplete the the contract, but our team has to spend two weeks on understanding how the scenario is. So, basically the tool takes the output of the satura prover and try to understand it to a human. We don't want a PhD to understand the result of the formal and sometimes with the tool finds a bug and it tell you under this situation, you probably had a bug. I don't know. We had this sushi bug that we prevented that allow you to infect deplete all the

code. And interestingly but the prover finds it in 5 minutes and it took our engineer 3 weeks to understand it. Eventually we show it to the developer. The developer said, "Forget about it. We know. We know." So, we want so the LLM is going to make the formal verification needed but it make the formal verification easy. So, we have a here we have the the the the the code the code the QR code. Please register. Please ask us. Some of us are here. We have a booth. Our engineers are actually most of them that do this thing are based in the US, but we are global company. We have security researchers everywhere. Please ask us. We want to actually have you use the tool. That's the idea. And and thank

you ever much for listening and thank you. Hopefully this will be useful with this tool. Thank you very much. Thanks a lot. >> [applause]