Formal Verification of Uniswap v4 Hooks - DeFi Security Summit 2025

Transcript

Can we start? Okay. Yeah. Uh welcome to this workshop. I want to talk about uh verification of unis swap v4 hooks. Um I think I have the wrong slides. Um yeah, the right one. I I see the screen.

>> Okay. Ah, sorry. I have to set it up.

What is this stuff? Um, I tried it before and now >> I can't switch the top anymore. Doesn't react. Easy. What do you need to do?

>> I'm wondering if I need to restart Firefox. >> Okay. >> Um because it's not reacting. >> Okay. Okay, thanks. Um, thanks for waiting.

So, I want to talk about formal verification of unis swap before hooks. So, first about me. So, I'm a former verification researcher at Sattorra. Here's my web address and my Telegram contact. And yeah, next about formal verification. What is formal verification? So, if you look up on Wikipedia, you get the definition of formal verification. Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property. And we will see these properties later using formal methods of mathematics

and this definition pretty much resembles what we are doing at Sora. Um there are some myths about formal verification and some of these are true some of these are false or halftruths. So there is a myth that formal verification can find bugs. There is a myth that formal verification can mathematically guarantee that there is no bug at all. And there is the myth that formal verification is hard and it requires a PhD to succeed. So let's look at these myths first. So formal verification can actually find bugs and we had several examples. The first one is

actually I put this on the slide a month ago and it became uh very um current now but there could be a mild rounding error that can be hacked to gain uh from the contract and bugs like these can be found by formal verification if you look for them. There are uh strange edge cases like in some particular strange case you deposit something but your shares will decrease and you want to find out that these extra cases exist and want to avoid them or you could have hidden or undocumented assumptions. So for example you have a

protocol um where you think everyone can always withdraw. you want to prove it and then the formal verification will tell you you need the assumption that for example the token does not block list your contract and the transfer will succeed and the most important part is if you have such a if you find such a bug with formal verification you can fix the bug and then you can just run the same formal verification again and uh then you will get an answer if the bug was successfully fixed.

The second myth was uh can formal verification prove the absence of bugs and well the the difficult part here is what is a bug and what is a feature. So you don't know if uh you need to define exactly what the bug is and we do it by doing something basically the opposite. We want to have properties of our contract. For example, you can always withdraw your funds and yeah and then we check that these properties are not violated.

So instead of proving the absence of bugs, we prove that these properties are true. And you also need often assumptions. So there could be uh ESC20 tokens involved and then ESC20 tokens come in very uh different flavors. There's no standard implementation if and then the question is does your protocol work for fee taking tokens? Does it work for rebasing tokens? Does it work for scam tokens where the balance can be random?

And there are also double entry tokens which can cause bugs. So you need uh to specify what your assumptions are. You can for example say I only support ESC20 tokens where the transfer tokens transfers exactly the balance and the balance doesn't change otherwise. Then there are other assumptions like price oracles need to give fair value. Liquidations happen in time which is kind of something that you can't really check because it's outside the blockchain. But you can assume that it will always happen from the outside.

And then yeah, governance must also for some contracts governance must not be malicious. For other contracts, you want the contract to work even with malicious governance. And if you have these properties and the assumptions, then you can prove formally that these properties will always hold under the assumption. So there there are no bugs that violate these properties. But it's important that you need to come up with the right properties otherwise you will miss bugs. And the last myth was uh that formal verification requires a PhD. And this is actually a lie because um if you can

write solidity you can do formal verification. So we have uh the Satara verification language. You write something. It's a rule. It's similar to a function. Uh you have some code in it. You have variables that you declare. You call functions. Um and then you check the property by yeah doing an assert. And then here is the condition that we want to check. And if you can write solidity, if you can write unit tests, you can write uh you can do formal verification.

Um yeah. So how does formal verification work? So um you start with a solidity code and we also need a spec file. The spec file is a specification file where the properties are described that uh should hold for our contract. These are the rules that you have seen on the slide before. You put both the solidity uh files and the spec files uh into our solver into our tool. So you run the tool and then the tool will tell you yeah there are two possible outcomes. Either it gives you a proof of that all

possible under all possible circumstances this the property that is described by this rule will hold. So there is no counter example or it will give you an actual counter example and it will tell you which with which values you have a bug and then you can analyze this counter example and see maybe you have an hidden assumption that you didn't think about. You need to add the assumption or maybe there's even a bug in the code. And internally it works by taking the code and it takes the spec file and it translates every statement. It's basically the bite code. Every bite code uh changes a variable or it um does an

operation mathematical operation. And each of these are translated to logic and it uh computes a logical formula that basically um describes the behaviors that will violate the property. And then you use a state-of-the-art um solver for these formulas. And these solvers can in many cases uh work with huge formulas which describe uh a single contract call of your contract and then find solutions input parameters where your property will break.

And as an simple example, I took one of the simplest function in the unis swap pool manager. I wanted to make it a bit unis swap uh themed here. And this is a take function. And we want to verify this take function. So the take function there are different things that we want to verify about this take function. I I mean there's one thing that we want to verify, but there are different things that can go wrong. We want to know that take the take function updates the accounts liabilities correctly. And what can go wrong here?

Yeah, there is an uncheck block here. So we don't check for overflows and the question is is this dangerous? Do we miss some overflows here and the function will break? And hopefully because it's unis swap before it's not unsafe. There are people looked at this but our tool will also check it. Then the question is is the sign correct? Do you need to negate it or do you need it positive? There are so many ways you can do different small bugs, introduce small bugs that are hard to spot in the code.

And what we do is um we want to verify this and we need a spec file for this. And I already said that we have this language CVL and in this CVL you write a rule which looks very much like a unit test. So if you think of rule as a function then it it's almost a unit test. There are some strange things here but that I will go into here. So first the rule has inputs and the question is where do these inputs come from and the answer is the solver will try every possible value. So it's like a fast test but it doesn't try random values. It doesn't run for a thousand

values. It checks every possible value. And this is possible because it does it symbolically. So we translate everything into a formula and then the formula solver will know how math works and it will check can check it for every possible value. Then there are function calls. So this is like you are used to in unit test. You can call functions like uh that are in your contract get there's a function get delta in which tells you what the current balance of the user is. And then the question is which user and for this we have this environment. So sometimes you need to know what who is the message

sender because take basically depends on the message sender and we make this hidden uh parameter the environment visible by yeah giving it as a parameter to take and then you can talk about the environment and say the yeah what is a message tender and can ask for the delta of the message sender but for get delta we don't need the environment because get delta doesn't depend on environment. Then another important thing is we have math integers and math integers will never overflow. And this helps us to find overflow bugs because here our

property is over math integer. we will not have the same overflow bugs that could be possible in the if you do it with uh the U in 256 math or with the in 256 math. So by using mathematical integers we will find discrepancies caused by overflows. And finally we prove this property and we prove it for every input and also every contract state. So we don't assume that the contract was just initialized.

It could be that there's a lot of liquidity on the pool. It could have been some swaps before and um we just assume nothing about the input state and if we need the input state then you uh yeah then we prove it for every possible input state and you get a counter example if there is any input state and then you have to work around that. Um yeah I want now to show this in practice on a simple example uh on a hook example. So we want to verify a unis swap v4 hook and I took as an example the points hook which is actually a contract from the unis swap v4 hook

tutorial and it's a very simple um example. It's a hook that has an has two um operations and the idea is that you want to provide reward tokens to anyone who uses your pool on unis swap. So um if you swap on this hook uh on a pool that has a hook, it should reward your tokens and it should reward you as many tokens as you spend in ether. So the tokens should basically they can be used for airdrops for example. It uh basically tells you how much volume you uh did on this unis

swap pool. So the swap hook is very simple. You check um do you swap ether for for so zero is always the ether token. If you have a unis swap hook with ether then it's always a zero token. Uh, and if you swap ether for the token that is in the pool, then you um then you want the cook to run. So if it's not the case, you return early. Um, you figure out who the user is. You figure out how much he spent and then you mint the tokens. And then you have a similar function which looks almost identical for after add liquidity. So if someone adds liquidity to the hook um

here we don't need to check the direction because add liquidity will always add both tokens to the pool and then it means the token amount and this is the property that we want to verify. So for this we write a rule on swap and at liquidity the user receives point token for ether he puts into the pool in a 1:1 ratio and the problem with verification is or the problem even writing the unit test is now you need to figure out where you start. You could of course write a unis swap for the after uh swap function

but then you may miss some bugs that are caused by the interaction with the unis swap pool manager itself. And so we ideally want to have at least the pool manager in our unit test or in our in this case in our verification rule. So um the full picture is we have a user. The user may use an router a universal router. The router then does all the operations on the pool. It provides a token. It swaps. It receives the uh tokens that it swapped into.

And the pool will also do the interaction with the hook. And this is uh completely out of control of the user. It's it's hardcoded inside the pool that the hook is used. And uh yeah, there are a lot of messages going around between these. I asked an AI to draw me a nice diagram which shows the interactions and uh unfortunately it didn't succeed. It just drew in a confusing picture. So uh I drew myself.

So this is what's going on here. So we have these four uh actors. We have the user and the user sends an execute function an execute transaction to the router and the execute takes as an argument the intent of the user that he wants to swap tokens and will also take care of getting the tokens. Afterwards the router then does the interaction with the pool manager. It needs to lock the pool manager. If you know unis swap before, you know what the lock is. Uh it's kind of a reverse re-entry lock.

Instead of um avoiding re-entry, you only allow to use the user in uh the re-entrant lock call. So you lock it and then it's like uh a flash loan. While you lock, you can't return before you paid all your debt and then you can do the swap operation, settle and take operation. And when you are done, you return and then it will check that your debts are settled. And uh yeah, there is a swap operation and the swap operation will call the hook and it will do the swap. And it turns out we don't want the whole scene.

It could be that the user doesn't even use the router and the hook should be correct even if we don't use the router. So what we want to look into is only this part of the calls. So we just look at the swap, the before swap after the internal swap and the after swap. And the next problem we face when we do verification is if the contract gets too big, the verification doesn't succeed. And the underscore swap function, the internal swap function is a beast in unis swap.

It goes through uh all the ticks um over the swap ranges. It looks at the liquidity. It computes the fees. And if we would try to verify this like this, it wouldn't work. And we don't need to because unis swap before was already verified. And we don't need to verify that the swap function is correct again. Instead, we replace the swap function by in an abstraction of the swap function, a summary. And I want to show here the summary. The summary is yeah, it's a function. It has the same arguments as the real swap function.

Takes the pool ID. It takes the swap parameters and it returns uh yeah the amount the balance delta the amount of tokens uh that were taken from the first kind and the amount of tokens that were given out of the second kind. And um the important uh trick here is we can just not initialize a variable. And if we don't initialize a variable then the prover again tries all possible values. So by not initializing the a variable we will check all the possible swaps that are possible. So now we have amount zero delta and amount

one delta and they are random values or they are yeah we check all possible values but we don't want all possible values. So we can then restrict the values further. So we can say if we want to if the swap params say we swap zero for one token then we want that uh we pay the zero token so this amount should be negative and we receive the one token so this amount should be positive. So um depending on what you want to do, you can refine this even more and say the price should be reasonable or the price should be in between the old price and the new price. Um but here for this

hook we don't even need this. So we can use a simple abstraction and then um we also remember the balance of each token because we want to reason in our rule about this and yeah we have a a ghost variable that is only used for verification. So it's called ghost variable because it doesn't exist in the real contract. It's only there in the verification. But it can also not affect the real contract because the real contract will never read it and it will never affect the control flow.

And this ghost variable um basically we say um the token zero balances decreases by the amount zero delta and the token one balance decreases by the amount one delta. And the decreases is because it's negative if the user pays. So the balance of the pool should go up if it's negative. Yeah. And here we need because we use math and we need to cast it back to a U256. And here we require that there is no overflow because we know that unis swap will never overflow the pool balance. We can do this safely.

And finally we uh return the the amounts that we just guessed. So the prover can guess the swap amounts. It can uh so if there if you execute it in in the real code there is some swap amount and the prover can always guess this swap amount that happens in the real code. So it will find all bugs um all bugs that are violating the specific property or the property that we want to verify. Um but it will sometimes also give you wrong counter examples. It will tell you yeah there could be a swap um which is very unreasonable which doesn't match the

price of the pool. Um if this leads to a bug then you need to refine your summary. you need to change the summary and be more specific there. In our case, we didn't have to do it. Yes. >> Are when we define zero delta and the amount of data? >> Yes. >> And we don't give them values. Uh are they symbols and the prover will try when you say we'll try every combination which will actually limit the range with the requires that we have.

>> Yeah. So uh good question. So this amount zero delta and amount one delta are used symbolically in the solver. So we put this as a variable and these uh conditions amount zero delta is small or equal zero is added as into the formula. So the formula we can just add logical formulas to it and so yeah we asked the solver give us a solution for this and one condition is that the amount zero delta is smaller equals zero. So now we can look at the property. We want to say uh if we if we swap tokens and we spend ether then the amount of points

that we mint is equal to the amount of ether that would were put into the pool. And yeah we can write a simple rule. Um yeah, we asked what is the token balance of the pool before we asked what is the number of points minted before in total. So we just use the total supply here. You could also try to figure out the user and ask what is the balance of the user. But here for simplicity I just use the total balance. It's easier. And uh then we do the swap on the pool manager. So we call the swap function of the pool manager and the pool manager will then hopefully call the swap

function of the hook and then we read the balance afterwards. We uh read the uh total supply of the points and we check that the difference is the same. So the number of ether that um were put into the pool is the same as the number of points minted. And yeah, now I switch to um Visual Studio and yeah, this is a point hook after swap function. Yeah, I shortened it a bit on

the slide, but it's basically what I showed on the slides. And here's the specification. um the minting matches on swap and what I didn't show on the slide is there are more conditions that you need some not so hidden assumptions namely um well the currency must be ether because we said we only want to swap uh mint tokens if you pay ether. So this is uh basically another requirement that we need in the rule. We um we also need that the pool actually has the right hook. If the pool doesn't have our hook, then the hook isn't called. So we need the require

that the current contract that we want to verify um the points hook is uh actually set. And then we also need um that we swap in the right direction because if we swap in the other direction, you don't get any tokens but the ether balance still decreases. Um, and we don't want to burn tokens. This is a design decision. Yeah, otherwise it's uh exactly what I showed on the slides. And then we um need to set up our verification.

Um, we have a configuration file. In the configuration file, we list all the solidity files that we want to verify. In this case, we wrapped the pool manager and the points hook with a harness. And this harness is basically allowing us to read some internal functions. Um, I think delta is readable, but I'm not sure if I added this to the points harness, but we need some internal functions that we can't access because they are aren't public. And so we we add a test harness around them.

And uh and we also need a token for the points token where we just take uh I think it's just an ESC20 token from open Zeppelin unchanged. Then we need to set up um something some variables. So we want that the points token that is set in the in the points hook always points to the points token. So we know that the setup works. So we can here statically describe the setup that we expect to be on chain. Uh we give some compiler options. We say which solidity compiler to use, which optimization settings to use. And uh then here at the bottom line, this is a

specification file that contains a rule that we want to check. And now we can run the prover. And uh yeah to run the prover you first need a key that you can get on our website because um then you can run our prover in the cloud which is much easier than uh installing it on your local machine and it also has a nice web interface to see the counter examples. Um then you give the configuration file.

Then I want to run it in the cloud. So I tell it to run it on our production server. And then I can um give some message so that I know what uh which run it corresponds to. This is just for yourself to know what you did. And then if we have internet here, let's see. Then it uh it compiles the code with solidity checks that everything is okay and then sends it to the server. It just does syntax checks and then it gives you a a URL and you can go to this URL to watch your your verification live.

And for this we need to go back uh to the web browser. Yeah. So um this is the interface. It's still running and it can uh it's not even running at the moment. There's a bit of traffic so it's still cued to be running. I prepared some runs so that we can just look at the result.

Um I think this is this one. And after it runs it gives you an overview what happens. So um there's always this entry checks static check which just checks that everything that you declared as not needing an environment like this get delta function doesn't need an environment um actually doesn't need the environment. So this is a very simple check which usually succeeds unless you make a mistake and then we have this rule minting matches on swap which we have seen and this is violated. So you get a red cross you get a violation and now you can click on it and figure out the reason why. So if we

click on it we get here we can go to the source code and see this was the rule. Then we see here the call trace. Um what happened um which is kind of a lock. And then we have here some tubs um this top is most interesting where you can see the variables the input and output variables that were used. And you see here um yeah there there was this the balance before is different from the balance after there was a lot of tokens swapped. It just generates random values so they can be very huge.

Um and um yeah and the points token supply is also very big but it now it's not so big. It's 2 ^ of 11 - 257 and it doesn't change. Yeah, these numbers we we try to make a pretty printer and show powers of two and then something like this happens. Um, you can argue whether it's nicer to show it in this form or in decimals. I think you can even change the way it's printed, but I can't. Uh, yeah, I am not going into this now. So, now we

want to know what happened and what went wrong. So, we can usually what I do is I look into the call trace. Oh, this was the wrong button. I wanted to close it. Um, you go into the call trace and you look at your property that is violated and you see it's violated. The ether balance changed by a lot and the points token supply didn't change by a lot. It didn't change at all. So now we need to debug it. What happened? Why didn't it work? So what we u what you probably already think of it must be in the swap function because this is where the points should be

minted and somewhere in the swap functions there's going something wrong maybe um the logic is wrong. We go into the wrong if case in our hook. Um so let's look into the swap function and there are yeah there are a lot of uh branches that are evaluated. You can always jump to them, but let's skip over them for now. Then you see here the before swap hook is called. Um, then we have our swap summary, which is the main swap. And then the after swap hook is called. And this is where our points token should be edited. So let's look into the after swap. And and

you see there's only one instruction in there. There's a branch condition that is evaluated and it and then it stops. And so let's we can jump to the source code where this happens. And we see we can also um make this going away. And this is a instruction. This is the branch that happened. uh if message sender is equal to address self then return and it's part of the hooks soil which is in the unis swap v4 core. So here the unis swap v4 core that we used unmodified has a branch that we

didn't think of and now we need to understand it. So the address self, this is what I first got wrong, is actually the hook. It's not the unis swap pool. So self is the hook. So if the message sender, which is a me message sender of the swap function, is equal to the hook itself, then unis swaps has this policy that they don't notify the hook um about their own chain uh swaps. And now we need to work around this. So um the reason why it's still okay is basically that the that our hook will never swap. We know that our hook will

never swap. And and this is a hidden assumption. I mean you can look at the code and prove it but for now we just let's just assume it for now. So, so what we do now is we need this requirement that the message sender is not the hook and we add this requirement to our code, our rule. So we go back to our rule and to the spec file and then we additionally require that um

yeah the AI is trying to suggest something but it's wrong. Um the e message sender is not the current contract which is the hook. Ah, now the AI has the right idea. So the points hook will never initiate a swap itself. So um we can run it again. Um but uh since it takes a while, I can also jump directly to the job list where I hook is not the message sender should be the run where I added this requirement

and it didn't help. So it's still minting matches on swap is wrong. We can again look into this. You can see the variables And um there's a very similar problem now. Um the ETH balance changed. The points token didn't change. Is it the same buck or is it um yeah, here's the assert. It's false. We can go into the swap function. Where's the swap function? It's here.

Um we scroll down to the place where the hook is called here. It should be called. It looks better now. Something is been is doing is running here. So it runs through this function and then there are yeah basically here seems to be a very if you look at this this is very suspicious. The hook function asks uh called the has permission function to check if the if a permission is set and this is false. So let's look where this happen.

So here's an if condition. If self has permission after swap flag then the hook is notified. And if it's not um yeah if it doesn't have permission then the hook is not even called. And where does the permission come from? I'm not sure how many do do you know unis swap before. How do you have to set permissions for the hook? They have a very neat trick. They encode the permissions in the address of the hook. So you need to uh brute force your address of the hook so that the last bits of the hook correspond to the permissions of your hook.

So if we go to the bottom here has permission function. It takes the address of the hook and it checks if the after swap flag is set with a bitwise operation. And yeah, the hook was deployed to the wrong address. So yeah, it doesn't work. So what we need here is we need to check that the hook is um is deployed to the right address. And there's actually a function in the hook that helps us to check this.

And I already added something to the harness that calls this function. This is basically the um the validate hook address function will check that the hook is uh that the address of the hook is correctly set. So that all the permissions are correct and it reverts if it's not the case. So I put a try catch block around this and I return a true false value. And now I can check this um using this harness I can check if this hook is given to the right address. So I can just require here require

check cook address and yeah because I did it before there's also already the uh suggestion to say um yeah this is a condition that it was correctly deployed. >> Yes. write as a can we write as a constraint uh directly address it wise end >> yes yes you can also write it directly if you want um I I found it nicer this way but it's uh you can just say I have to think about it because I'm not

sure how good the conversion works but I think you can convert the address to a number and then use bitwise operations It's a bit It should work. I don't want to try it in case it doesn't work. Um, so then we can run it again. Hook is with the correct address. And this time we get a green check mark. Yay. Everything works.

And um one thing that I want to say here is the hook can't be deployed to the wrong address. So the unis swap already made it um they have a hook library and if you extend from it, it will check that it's always deployed to the right address. If it's deployed to the wrong address, the constructor will fail and um the constructor will just revert. And so we can actually prove it in our tool that it's always uh deployed to the right address. But to prove this, we need to prove a so-called invariant. Something that holds for all the reachable state in our contract. In this case, whenever we create the

contract, the address is correct. And since the address never changes, it will always be correct no matter what operation we do on the contract. And so what we can do now is we write an invariant and the invariant. Yeah, let's call it like this or correctly deployed. And the invariant is basically saying check hook address always returns true. And instead of requiring the that check hook address works um we can require the

invariant that the hook is correctly deployed. And you may think what is the difference. One difference is we don't need the second argument anymore. We don't need to say why this is the case because we prove it. So every require we put in to our code needs to be needs to have a reason. If we put a wrong require into our rule, we will hide bugs. We And there are cases where we had bugs missed because we had a require in there that shouldn't be there. And to uh yeah, and therefore we require basically that you need to think about why your requires hold and you need to

write a short text explaining it. Why do you think it holds? And for an invariant, you don't need it because we proved the invariant. We checked the invariant. And yeah, then we can run the tool again. And uh yeah, let's go back to this here. We use the invariant. And now yeah we get uh it still get the correct result for minting matches on swap and we get uh this strange icon here which means there that the rule passed

the invariant holds but there was something fishy about it and so we have some sanity check that we use to detect if there is something strange going on and um if we open it you see we need to run the in invariant on all the functions of our contract. We need to run it on the constructor to check that the constructor will satisfy the invariant. We need to run it on every public function that they will not change the envir invariant. The um constructor is the base case. It works.

Um then there is another case when transient storage is reset then the invariance still holds. It's not very difficult to show that the address doesn't change if the transient storage is zeroed. And then we have uh for every function in the points hooks and for even for every function in the pool manager we check the address and in the points hook um yeah um there are a lot of uh functions like the after removed liquidity hook the um before remove liquidity hook that are not implemented at all and The

default implementation is to revert in every case. And our tool says uh tries to verify it for all non-reverting cases. So if all cases are reverting, we've we have um basically a warning because we say your property holds but we didn't check anything because there is no run that we could check. And um yeah in many cases these uh actually point to bugs in your specification where you have a require that prevents your code to run at all and you want to know about it and this is why we have this icon. In this case we can see it's okay. We know

that these function will always revert. Um yeah so our swap function is okay let's go to the other function the at liquidity function and for the at liquidity function yeah I prepared it uh beforehand so Let's uh just take this function put it in there.

So this is a very similar function. Um we call modify liquidity. We check that everything is fine. We also check that the hook is on the correct address. Um, we check the balances and we call the tool and um, and the outcome was again a buck uh, a red cross. So, we found a counter example and this time um, yeah, it's a bit more tricky.

So uh we go to the assert where this happens and we see there here's the difference the east balance changed uh is different from the points token change and if you look at the values you see the east balance is something a very large negative number. It's a large negative number and this is a very very large positive number and it looks like there is an overflow bug.

So it looks like a wraparound happened somewhere in the code and uh you can actually yeah um actually the you see that the balance decreased even though we added liquidity and you can say is this a problem of our swap function or is it uh a real pro of our at liquidity summary we have a similar summary for at liquidity or is this a real bug in our code? And I looked into this and I want to make it short. There is actually a very tricky bug in the code. It's a code from the V4 tutorial, but um it has a bug in there.

So if we go to the the at liquidity it's sorry I want to go into the hook if we check the points hook. Um yeah we compute the um spend amount by assuming amount zero is negative we take make it positive we cast it to you in 256 and then this is the amount that of tokens that we want to add and these casts are all unsafe

solidity doesn't have safe cast they only have safe arithmetic and this is a real bug in the contract contract. And you may ask, why can the spend ether be negative if we add liquidity? And the tricky part here is that unis swap withdraws the fees at the same time that you add liquidity. And if the fees that you withdraw are larger than the liquidity that you add, then the amount of ether that uh you put into the contract is negative. You take out ether and you get more liquidity.

And uh yeah, this is a buck here. So you can use it to mint yourself 2 to the^ of 256 to uh yeah so we can now try to fix the bug. Um I don't think I have the time to go into that but you can think of uh putting here an if condition where you check if it's negative you don't maintain tokens and then you also need to adapt your specification and if you do all this then you can run the tool again and finally uh you will hopefully get the green check mark. So I I needed a few iterations. First fixing

the code, then fixing the spec, and then you get the green check mark and you are done. Um yeah, one quick final thing that I wanted to show is we also wrote a generic uh list of rules that every hook should follow. So one thing is um there's a spec file these hook roots. One of the thing is that um if you call one of the hook functions the hook should make sure that only the pool manager calls the hook. Of

course, if if someone else could call your after swap hook and just give it random values, then he could mint your token to himself. So we you need to check in the hook that the caller is authorized that the caller is a pool manager and then you can write a simple rule and here we have a rule that basically takes as argument a function and it will check every function that is not a view function. So we can also filter this. So this rule will be checked for every function that is not a view function that is in the current contract.

And then we call this function uh and we check if it reverted and if it didn't revert we want that the sender is equal to the pool manager and similar we can use generic rules to check if the hook permissions are set correctly. So we want that if the hook implemented some function then yeah then this condition is true and yeah then you can run this generic set of rules on your own hook or on this points hook and yeah I had an example with this hook where basically um we

found a few bugs or I I I actually injected some bugs. For example, I didn't set the before initialize flag and the permissions correctly and then it will trigger this bug and also trigger the bug that uh it didn't check that the pool manager ported. So to sum up, um, so if you want to check out our tool, go

to our homepage. There's a button on the top right, sora.com. There's a button on the top right the get your own key and then you enter your email address and you get a free key with enough 3 minutes to try out our tool. You need to install it. It's a Python package that you need to install. There's a installation guide. I have put the examples that I used in this talk into a repository and uh yeah there's also documentation of our language. Okay, there were already some questions. I don't think we have time,

but if you have questions, come to me. I'm here. And yeah, thank you.