# Proving Correctness of LLM-Generated Smart Contracts | John Toman - Certora - Channel: [Ethereum Denver](https://streameth.org/ethereum-denver) - Date: 2026-03-09 - Duration: 11:31 - Topics: ETHDenver, Crypto, Web3, Blockchain, Event, Conference, ETHDenver 2025, ETHDenver 2024, Bitcoin, Ethereum - Watch: https://streameth.org/watch/yt-6VfRtVTj__U - YouTube: https://www.youtube.com/watch?v=6VfRtVTj__U ## Description πŸš€ Get Ready for ETHDenver 2026! πŸš€ We're already hard at work preparing for next year's biggest Web3 event! Keep your eyes peeled for more info on ETHDenver 2026β€”it’s going to be epic! 🌟 ## Transcript [music] Okay. Hi everyone. Thank you for your patience. Sorry about that. Um I'm John Tolman. Um I'm a senior technical fellow at Certora. Um and the talk I'm going to be giving about uh today is about a new technology that we've been developing for the past year or so uh around verifying uh LLM generated code. Um so a bit of context actually before I get into discussing the technology sort of what is the reason for us uh to be wanting to use LLM to generate code in the first place and to do that we have to talk very quickly about the sort approver this is our flagship technology um it's a symbolic reasoning tool that can formally verify uh smart contracts written in solidity viper uh we have support for Salana uh and several other blockchains um this relies on something that's called static analysis of memory and storage. How the smart contract is accessing you know dynamically allocated objects how it's interacting with the state variables and so on. Now if you've ever programmed in solidity you've almost certainly heard of this feature inline assembly and this is a very frequently used and also abused feature which lets you write low-level assembly code and I'd actually say solidity is almost unique in its the way it makes it extremely easy for you to write low-level code like this. Um now this frequently causes issues with our static analyses. Um and this is a representative example. It might be a little small but this is a safe transfer function uh that we took from the solotti library. Um it is heavily optimized extremely gas efficient. Um and this is performing just a transfer from accounting for the fact that you know sometimes uh functions return false sometimes they don't return anything. And all of this is doing in an extremely gas efficient way. It's also absolutely galaxy brain in its implementation. It does things like overwrite the free pointer but then put it back. Uh trash other bits of memory but then make sure like to put it back into place at the very end. Um and I'm not trying to pick on Salotti. Like I said, it's actually quite uh galaxy brain. It's quite intelligent, but it's also very representative of a lot of the inline assembly that you'll see uh out there in the wild, both when you're reviewing code or auditing code. And so it's not just a problem for our analyses. I claim this is actually pretty hard for you to review if you're not a frequent Galaxy brain user. Um and so the question we found our asking ourselves asking is could we automatically generate equivalent implementations again for auditing code review our static analyses whatever. Now the key thing here to notice is the automatically generate and equivalent there are the two key parts of this uh problem definition here and to focus on automatically generate is currently the year of our lord 2026. So when you want to automate anything you of course throw AI at it. So let's take uh this uh code uh throw it into some LLM with a prompt that says hey you know rewrite the code using standard solidity instead of inline assembly you know please make sure it's right and then out come will come something you'll definitely get something out of the LLM um so great um here's our system diagram you know just throw something into the LM get some simplified solidity out is it this simple and the answer is no of course not right um AI powered means you're getting AI powered mistakes right and so this is a one of the attempts that we got out of one of our test runs simplifying this code and the question is are these actually equivalent? They it looks very plausible um which the results of LM usually are. They look very plausible but in fact they are not equivalent. Um and the actual the reason is this little uh sort of uh innocuous looking AB code here. Now the fact that there is a uh error here is not surprising. After all the LLMs themselves are very quick to tell us that they can make mistakes, right? And so for us to just blindly put in code here to an LM, ask them to rewrite it and then trust the results would be utter foolishness. So what we actually do is we use LM to generate code, but we add guardrails. So in particular, we take the original code in a prompt which uh effectively just says um please rewrite this code to make it simpler. We then take the original code that we asked to simplify and then feed it into Concord. Now this formally verifies whether or not two uh smart contracts are equivalent. And we'll get into what equivalent means later. That was the second part of our definition there. And if they are actually equivalent, then we return this to the user and say yes, the LM did a good job and in fact returned a completely equivalent code and here you go. If not, we actually get an explanation explaining why the two behaviors are divergent. We feed that back into the LM and this loops. If you're familiar with something like a Ralph loop, this is kind of similar to that, right? You keep itering with the LM telling it it got it wrong and ask it to keep fixing its mistakes. And so this whole area between the two dotted lines are what we're calling concordance. This is this automated rewriting tool that uses LMS to generate uh rewriting rewritten code. Now again I've been sort of writing this check for a while and it comes time to cache it now which is that we have this equivalent. And so what does it mean when we say two the two contracts are equivalent to one another? Well I will start with sort of an intuitive definition that I think we can hopefully all agree on which is that two contracts are equivalent if they do the same thing on the same inputs. Right now of course there's a lot to unpack there. So, you know, we can sort of wave our hands here and have this diagram that says, you know, equal inputs go to equal outputs. So, I would try to make this a little bit more precise by saying that an external actor shouldn't be able to tell the difference between your two implementations. If you're just looking at the results of executing the smart contract on say Etherscan, you should never be able to tell the difference between executing one implementation versus executing some other implementation. The effects that they have should be the same. Now I just mentioned effects right because in addition to the actual explicit inputs and outputs the values that get returned by the function there are also state changes balances get moved around transfer uh ether gets moved so on and so forth another word for this is side effects right and so when we talk about do the same thing or the same outputs that also has to include this notion of side effects or state changes so what are some of these side effects or state changes that could be included here well I just mentioned one already which is mutating storage if you change the balances field of your pool, that is a state change. If you are emitting a log, that's a state change. That's something that an external actor can view. You can see that if you open up the execution of your smart contract on Etherscan, you can see the logs that it emitted. Calling another contract, and this includes both uh contract creation, balance transfers, that is another way that an external actor can observe differences in behavior. If you ever call out to a different contract and you're passing different balances or you're passing different arguments, that's an observable difference. So, uh, self-destruct is also there, but deprecated, so we're not going to talk about it ever again. So, what are some examples of not side effects? Well, mutating, uh, memory and pushing and popping the stack. Now, again, these sound like side effects. After all, we're mutating memory. We are sideffecting memory. So, why do we not consider these side effects? And that's important because I was very careful to say external actors. The stack and the memory are not visible to an external actor except to the extent that they influence the actions on the right. If you can push pop the stack 100 times, so long as you end up returning the same value, it doesn't actually matter to an external actor except for wasted gas. And that's something else that we don't consider to be a side effect, which is the gas consumption. Now, that is a very real side effect. The amount of gas you consume will determine how much money you're spending to execute your smart contract. This is a practical trade-off we had to make because if we insisted on equal gas consumption, that effectively constrains your contract to be exactly the same, right? just the chances that you'd have a different implementation that has exactly the same gas consumptions just that admits only one implementation which is the original. So we ignore gas consumption. So a final sort of more uh formal definition of equivalence is two contracts are equivalent if on the same call data in the same environment. They both revert with identical return data buffers or return with identical return data buffers and emit the same logs make the same external calls and end with the same stoages. So finally is uh the actual equivalence checking itself. Right? We've now defined what equivalence is. How do we check this? Well, this is actually just an application of the sort approver which I told you was a symbolic reasoning tool. What this can do is basically take mathematical uh expressions that assert some property about smart contracts and determine whether they uh exist or are they equa equation holds on all possible inputs. Um and so what we can do is encode equivalence as equality of side effects and equality of return values and then verify this mathematical property. So to see how we do this in an extremely high level and handwavy way we basically separate these two things into two tupils. The function has its explicit output and then its implicit outputs which are the effects that it has. We encode this as math by using math symbols and then we check this with a sour approver. So, this is a 50-minute talk, so I'm not able to go into a huge amount of detail here. So, I've handwaved a lot of how this works. Um, there is a tech report that you can go into. It's a 25page document that goes into all the detail you could possibly want about how exactly this works and how this integrates with the uh prover pipeline itself. I should say that this is slightly out of date since we actually wrote this document. We've added support for uh loops where we can actually now inductively prove that loops are equivalent, which gives us uh greater reasoning, modular equivalents and things like that. happy to talk after the afterwards if anyone's interested. So quickly to give you some idea about where this has been successful um I said we we use it for verified rewriting we can also use it to in other contexts like verifying compiler optimizations and in fact using uh concord we were able to uh independently discover a bug in the Viper experimental uh uh code generation pipeline. there was a optimization that caused it to completely trash the local state of variables and Concord actually managed to detect this and say that hey the behavior is diverging here because the optimization pipeline did something wrong. So uh quickly to to wrap up uh this feedback loop uh requires this explanation and I want to give a quick intuition for what this looks like. So the tour prover uses SMT solvers. These can give a uh concrete uh example not just telling you that hey they're different but why they're different. what did they do differently? And so to return to our example, I told you this abid code was the reason that this was not actually uh equivalent. And so it's actually this is the uh explanation we get out of the SMT solver. It says what happens if the contract you're calling transfer from on return two like 00002. Why is this a problem? This is not a valid encoding of a bool. A bool is either zero or one. The original implementation will just revert with transfer from failed. However, abid code on malformed input will revert with an empty buffer. And this is the sort of nitty nitty-gritty nitpicking that Concord is able to reason about. When we told the LM about this, it suggested doing this instead, which uh gives the original behavior from the uh salotti implementation. So uh I so far have been talking about this to use LMS to simplify code. Of course, as I hinted, you can use this with by simply tweaking the prompt a little bit, optimizing code, porting code between different uh languages or frameworks and so on, refactoring. And I should also mention it's open source. Um, and I think oh, that does wrap it up and I'm done. So, thank you so much for your time. Uh, any questions? >> Yes.