Safe Smart Contract Vibe Coding | Mooly - Certora

Hello everybody. Good afternoon and excited to tell you about a new project which is being uh started by Sata. Please take a look and we like you to contribute. This is a joint work uh wait this is joint work with John Tomman who will be here later. So many of you know that the the smart contact is a very very hard to get right and we know it's a domain with hero developers and a lot of bugs are there and but the question that everybody ask uh ask and we see it all the time and actually uh we have seen it yesterday is that what's going on with LLM?

So how many of you heard about the pash of tweet about the LMM hack? Can you tell me? Sounds like nobody. It's very interesting. Take a look.

Basically, what happened? LLM generated a bug and this bug actually cause people to lose a lot of money. And the purpose of this talk is to show that this can be avoided. So what we going to show? We're going to show something which is a little bit counterintuitive.

We're going to show that in fact with LLM we can make the code more secure not less secure and our secret source is formal verification. The idea is that we can generate a code which is formally verified. So we're going to basically make a code which is generated and and is formally verified. So the problem of LLM generated wrong card is not unique to uh web 3. So how many of you heard about cloud flare?

Nobody. Okay. At least some people had about so Cloudflare is a reputable web 2 company and what they did they had a very beautiful blog post. Take a look and this blog post say how they generated one of the most interesting distributed protocol in one day. Guess what?

This was completely broken. Okay. And and and basically LLM generated all these buggy code. And and and this is actually something that we're going to see more and more that LLM generated bug buggy code. And of course also code that is not generated by LLM is bugging.

So the Cloudflare workers project I really recommend that you take a look is something that is basically was generated overnight by engineer very very nice idea but what happened it was completely broken and you can take a look into the code here I hope you can see can you see from here can you see what's wrong in this code actually very easy to see in this case do you see I mean I I this code is huge I just took the the the one the small code did you see What's wrong here? Basically, the LM completely cheated. The LM basically put it to do on all the complex parts. Okay. And the engineer, I don't know, he wanted to ship the code early.

So, basically that this is code. And in fact, Cloudflare apologize. All is okay. So, LLM generate wrong code. And there's actually two problems why LLM generated new code.

It's not just you want to go to chat GPT5 or chat GPT6. is going to be remaining and the idea is that there are two problems of the LLM that it's a it's one of them is basically the idea is that LLM really doesn't know what you are building so it just has a guess and the other one is that and this is specifically to the program that it glances over coroner cases it really doesn't understand some corner cases of the code and related to that there are actually two problems that are really really specific that we see that the LLM is always making some unjustified assumption and I'm going to show you this has happened in the cloudflare in many cases this will happen in your smart contact it's making unjustified assumptions and the other one which is very specific to the code the LLM is doing some kind of pattern matching which is visual but in fact when when we are talking about program they have semantic behavior it they have something very very different. So here is a very very tiny example. There is a code which is generated by LLM and it is wrong. Can somebody guess what's wrong here?

It's a very very simple code and the LM generated the wrong code. Okay, does anybody see something? This is a verifying of signature. Maybe I give you a guess what does this function return? Can you tell me?

So this function return always true. It's completely broken function. Okay. And the LLM generated a completely broken function here. Okay.

And that's very interesting. That's very interesting that the LLM even in this small code it generate this wrong call. So the idea of unjustified assumption is very very interesting and it's a very interesting thing because when we talk to people with LLM they tell you oh the problem is is the fact that you don't have enough memory but in fact the problem is kind of weird. If you don't have enough memory then you don't have enough context it will get wrong. If you have memory then it will get a lot of context it will also get wrong because it will be confused by this other context.

Okay. So this make it like an art somehow. That's the idea. And you take a look it's it's very interesting. You increase the context, you reduce the context, still you get a wrong code.

So the other bias is the pattern. The LLM does which is the right thing kind of. It looks into the pattern and it looks into the pattern and it say what is it that is going on. So you see this verify and he's trying to see what is this verify and he's actually looking it and does this pattern matching and based on this pattern matching it says what is the correct code and in fact it's interesting it's many of us as human we do the same thing we also do pattern matching we look at it to say oh this is verify this is true it returns true so in a sense we do the same thing as human so this is what we So this is a bad problem and in fact everybody's going to use LLM and I'm not telling you from this talk that you should not use LLM. I'm only telling you that you should use LLM with caution.

Okay. So what you can do how can you prevent these bugs? How can you prevent the bugs that are generated by L? So there are many ways you can do it and the the the the first one which is the obvious but it's still not so easy to implement is with the appropriate prompt. If you know how to prompt even this bug you can avoid by telling the LLM not to you.

Okay you can tell the LLM tell me why this is function is returning this thing and in fact it will notice that this function is returning a boolean and it will not not return true. So it's understand it but you have to prompt it to the right thing. Okay. The other thing that you have to do you have to develop some kind of hacker mindset when you are working with LLM you have to assume that this can get wrong. So you have to somehow have like some kind of an auditor mindset and if you are an auditor mindset you can find these bugs.

That's the second thing. And of course you can also get external review or audit which are doing similar things. What in this talk we're going to show you that we have technology that can that can essentially uh find these corner cases for you. So you can use fuzzing, you can use static analysis, we use formal verification. The idea is that with formal verification we can eliminate these kind of bugs.

Okay. So we build this tool called AI composer. It's composed is basically you it combines LLM and formal verification and you can get the best of both world because you don't need to fully understand formal verification and you avoid the bugs which are generated by LLM. They both feed each other. So this is how normally maybe I can take this out.

This is how normally uh you work with LM. You see the you have a loop and you basically uh ask the LLM to write the code. The LLM if you are careful you find it and you get it wrong and then you iterate you iterate until you get it right or until you are satisfied by the result. With AI composer the situation is a bit more interesting in the sense that we save you a lot of time and we get you more correct code. So we ask the LLM not just to infer the code, we also ask the LLM to infer the intended specification.

So instead of doing one thing, the LM does two things, but in fact it does them better. So it infers the the the program and the specification and then we run it by a sequence of of method. We start with static analysis, fuzzing everything. At the end we have this formal verification that actually check that the code obeys the specification. And of course the human needs to know that the specification is right.

But I can show you that during this process we find bugs in the code and we also find bugs in the specification. Okay? Because in this process we refine. And of course at the end of the day you as a developer you have to review but you have now I'm telling you not just what the code I'm telling what is intended to implement. So air composer generate many things at the moment is open-source software.

We try it on small code. Let me show you here is a very simple example. This is a stable coin from circle. We wanted to generate the code uh by circle. But in fact it's very easy because the LLM will cheat.

The LM will just take the code by circle. So we made it so it doesn't generate the code by circle. We added a requirement of KYC. So basically the LM cannot cheat. And you see actually we wrote all these document basically it's a very it's a it's a 100 lines that explain what it's done.

So there is this document there's design document we feed this design document to the LLM and the LLM generated rules in our language it doesn't matter but there's parametric there are all these things that you generate it generate these rules and these rules actually capture the essence of this protocol it's pretty interesting okay and these are the rules that you generate so it get generate just formal rules of this code and then these formal rules you we have there. We basically uh use that to generate the code. So now every time the the LLM uh uh uh generate the code, we check it. And in fact, most of the time the LM get it wrong, but it's we fix it. We let we we give him the example and the LLM learn.

It's very interesting. The LLM learn eventually it get the code which satisfy the specification. Sometimes it's smart enough to tell you that specification is wrong too, which is interesting. So why are we uh doing that? So I think that this if you ask me I'm probably a guy which came very late to LLM but LLM now is actually getting standard.

I don't have to convince you and we have this AI coding agent which are coming all the time. So all of these coding agent can use our tool and LLM is actually getting better. It's interesting that in the Stor now LLM getting pretty decent rules and we think of LLM we think about LLM like that it's it's smart enough to generate rules so it's like a very very smart specification and the formal verification is like a a pedantic lawyer so it they kind of work in an opposite way the LLM is very optimistic and the formal is very pessimistic and they work together so in terms of formal There's a lot of progress in this space specifically progress that we made made by Sata that we actually have a lot of rules which are generated which are now the LLM can use of course there are other players in this space there is uh Amazon which has done a lot of work in including the tool lead which is used also in the crypto industry my priv which I developed in the academia and now used by Amazon. So a lot of tools are doing. So formal verification and LLM are both getting ready.

So what is the takeaway from this talk? What is the takeaway from this talk? So I think basically making this LLM agent with formal verification you can actually make them better and I and I think I already uh wrote something in Twitter but the idea is that you can make the LLM better with the formal verification and the the other players in this space I think Amazon I mentioned but the idea is you want to make the LLM better with integrating formal verification and uh again going back to the beginning of the talk we said that there are two reason why the LLM got get wrong. One is that there is no precise definition and the other one is that may that LLM may glance of on facts and so these are two problems and we have two solution for the no precise definition we generate formal specification which of course need to be reviewed by human but it's much more concise than the code itself okay and it's also reusable the specification of of a stable coin is usually the same and how do we worried about corner cases this is where formal verification is good. If you have a specification the formal verification can find corner case for you.

So this is how we combine the the two things. So uh just to wrap he wants to close. So I I'm out of time but I want to tell you that Satra is doing many things uh and and and uh please take a look. I'm not going to explain because I'm running out of time. And just to wrap up the talk, if you want to get involved, this tool is MIT licensing.

We have it. We have it for we develop it for solidity and we saw people from Solana adapted it from Solana. It's combined with the open source prover. So reach out to me and we have a fantastic team around here. Reach out to the team.

Thank you very much for your time. No time for question I imagine. Okay.