DeFi Security 101 2025 - From Fuzzing to Formal Verification | Kevin Lotz, Certora

Transcript

I've been with Certora for about 4 months and yeah, today I'm going to talk a little bit about um how to get from fuzzing to formal verification. Um one sec. Okay. So, quick outline of the talk that I'm going to what I'm going to talk about. I'm first going to present a little bit what the difference between fuzzing and formal verification is. We've had a great talk about fuzzing, but we haven't touched much about formal verification so far. So, I'm going to give a little overview what the differences are. And after that, I'm going to give a small hands-on demo to make it a little more details what the differences are.

And the demo's going to be completely stateless. So, afterwards, we're talking a little bit about invariants, which take into account the states of contracts. And then I will wrap it up with another hands-on demo. Okay. So, uh I thought I start this talk by trying to convince yourself that fuzzing and formal verification are both in the end are just tools that allow you to uncover bugs in your contracts, but I think we wouldn't be here if there was a problem.

So, I don't think I need to convince anybody that this is a problem. But, um to sum it up, um if we have bugs in our contracts then just a single one of them that can already lead to substantial amounts of funds being lost. And another thing that amplifies this is the problem that there are adversaries out there trying to find these bugs um because they have a potential huge huge potential financial gains. So, we want to make sure that we find these bugs uh before they do, before we deploy our contracts or projects.

Okay. Um we've seen one technique to do this, which is fuzzing. And just to give a short reminder about what fuzzing is. Um we have our code that we want to make sure it doesn't contain any bugs. And we want to check it for some property, right? That it must hold. So, we write what's called a parametric test case, which is test case that has some input parameters that we do not choose ourselves. This is the difference to regular testing, but we give it to the fuzzing engine.

And the fuzzing engine will then come up with hundreds of thousands, millions, tens of millions of different values for these uh value values for this parameter of our test case. And we check if we can find a violation to the property that we're testing for it this way. So, in essence, fuzzing is just making millions of tests out of one test case. And if we find a violation, then of course the fuzzer will give you the concrete counter example that you can then use uh to instantiate the test case to to to trigger the bug. Or otherwise, as we've seen, we get a coverage report telling us uh what kinds of the code have been explored by the by the fuzzer.

Now, the coverage report or the amount of test cases that we run with uh with fuzzing that compared to the possible values that we could put in our parametric test case, is usually going to be pretty low. And if you want to make sure that um no value we can put in so that the fuzzer cannot miss any value, uh we can instead rely on uh formal verification. And from a user's perspective, um it doesn't look that much difference different. So, formal verification compared to fuzzing is providing mathematical proof that the implementation adheres exactly to what we call a specification.

So, on the left-hand side, we have our inputs to the system, which again is the code that we want to check is correct. And now instead of a parametric test case, we have what we call a specification. But for the sake of simplicity, if you have if not seen this, uh can imagine this to be very much like a parametric test case that would you would use in fuzzing. So, it has some input parameters. And now, instead of having a fuzzer decides randomly for those input parameters, we give both the code and the specification to what we call a compiler.

And the compiler will come up with one logical formula that covers all possible inputs or all possible values for the inputs of our specification. And what that formula is saying is basically it is valid if our implementation, so the code adheres precisely to the specification that we wrote. So, there is no input that can that we can put in there to violate the property that we want to verify. That's what that formula is saying. And we have then another tool called a solver, which then automatically solves these kinds of formulas checking [snorts] whether it's valid or not.

And if it is valid, then this constitutes a proof, a mathematical proof, that our code actually adheres exactly to that specification. If not, then the solver will give us a concrete violation. So, this is something that we also call a counter example, and we can then check the values that the solver gave us, so the violation to that logical formula, and those are then also a violation to the property that we want to verify. Okay, so that's on a very high level the the differences between testing or fuzzing and formal verification.

And so, if you've never been in touch with it, that might still be a little bit mysterious now. So, I'm going to make it a little more precise by exercising a small example. And what I'm going to use here is a function that is called the pop count. And if you've never heard of the pop count, that's short for population count. That's just That's a function that takes an integer, and unsigned integer and returns the number of ones that are set in the binary representation. Um so I have some examples here. For example, for n equals zero, um that's just a bunch of zeros, so the pop count would be zero.

For n equals one, that's just a bunch of zeros and then a single bit set, the LSB set, so the pop count would be one. For 13 in binary, that's four zeros, then 1101, and we have three ones, so the pop count is one. And um for if we assume that we have eight-bit integers, then for 255, that's the maximum value, all bits would be set, and we'd have a pop count of eight in that example. Okay, so um pretty I hope it's a it's a simple enough function. It's not necessarily uh related to D5, but we will uh see another D5 example later on, but it makes a perfect example for what I'm going to um

say next. If you're a developer, um you probably can come up with with an idea how to implement this function. Um the most easy way to do it, um that's just by popping the LSB one after each one after another, and just counting how many ones you see in that process. And that's totally fine, uh but you have to if you have to call this functions a lot of times, uh and you have uh you have 256 integers, then you have to loop through all of these integers uh bit posi- positions um again and again, and that can become quite expensive.

Um but luckily there are efficient implementations out there that don't require this uh this looping. And one of them uh I brought today. Okay. Okay. So uh please uh let me know if this is not readable. Um we have a contract here called uh bit ops for bit operations, and now we have Is it not readable? Yeah sure. Is that better? Great.

Okay, we have a contract called bitops for bit operations. And we have a simple function called the popcount. It takes a uint256 uh X and returns another uint256 value. And it's supposed to return the number of bits set in X. And the implementation that doesn't look look very nice. Uh so, that's just a bit of assembly and seems to be all bit fiddling and subtracting and doing all sorts of things in in uh on the bit level. Um so, that's not so nice to manually verify that this is correct. So, um Don't worry, I'm not going to go here and I'm going to explain what's what's happening.

But instead, uh we can imagine for a second that um this is something we have to review, make sure that is correct, or if we're implementing something that an LM came up with this efficient implementation of the popcount. So, now we want to make sure um that this is actually doing what it's supposed to do. So, the first thing that we could do is we could write some uh tests for it. And I prepared a bitops.t.sol file. By the way, if you haven't uh noticed already, this is uh uh it's a Foundry project, so we're using Forge here.

And I already set up a bitops test file, a contract, and set up a new bitops instance um to test it. The very first thing that we could do is we can write some simple tests and check if the popcount actually computes what we had in the table before. So, let's call this popcount uh test. Popcount, let's call it simple to not have naming conflicts. And that is supposed to be a public view function, otherwise the compiler complains. And now what we do is we do assert a queue and then call the pop count for example on zero and compare that to the expected value which is zero.

We can also do this for one and the pop count of one that of course is one. What else did we have? We had 13. Pop count of 13 that is three. And finally we also had 255 and the pop count of that was eight. Right? So now we can give this test case to Forge by running Forge test and then I'm using this here to run the exact case and we run it. It compiles it and runs the test.

Again, please tell me let me know if this is not readable. Um and it seems to pass. So for these four examples the pop count seems to be the correct implementation. Um so are we convinced that this is now is now a good pop count implementation? I hope nobody is. Okay, so what else can we do? Inside we can use a fuzz test, right? We have seen before how this works in Forge. Uh we simply write the test case that has a parameter, right? In this case it's a uint256 uh integer x.

Again, we have a public view function. Come on. And now we assert that bitops.popcount of x is equal to um one thing that we could try is um what is called functional equivalence testing where we instead of or again where in addition to the pop count implementation that that already have we uh provide another implementation and check that on all inputs uh both return the actual actual actually the same thing.

And here what I have is a different implementation of the naive pop counts or the naive pop count implementation that I mentioned earlier, right? We just loop through all bits by shifting X uh one to the right in each iteration, and whenever we see a one at the LSB position, we increase our counter by one right? So, that looks I mean, I could could be convinced that this is the correct pop count implementation. So, we can do a little uh functional equivalence test, putting the same value into both functions, and then checking that they are the exact same thing.

And let's put that to the test using forge test, and then we do match test and give it that one, and forge compiles it, and it runs it on we can see 256 different values. Uh that's not much, so we can ramp that up quite a bit doing fuzz runs. Let's set it to don't want to wait too long to 100,000, and it takes some seconds, but turns out um this seems to be okay. Um the test case passes.

Um so, forge fuzzes using uh 100,000 different values, and we do not see any violation or in the in the different Let's say it in a different way. The output of the naive pop counts and the output of this weird assembly pop counts, uh they seem to agree on all of these values. So, are we convinced now that this is the uh correct implementation? Um maybe, I'd say I wouldn't be sure so far. So, there's actually one more thing we can try. Um turns out that we can state if the pop count is correct without giving an actual implementation of it um because any function that satisfies these three properties here

that is a correct implementation of the pop count. The first one being that the pop count of zero is actually actually zero. That makes sense, right? So only zero has zero bits set. And then the next property that we have is that the pop count of 2x that's equal to the pop count of x and that also makes makes sense if you imagine what 2x in binary is. It's just a shift to the left and if we shift an integer to the left by one then we just get one more zero to the LSB so pop count doesn't change.

And the third property is basically the same thing. We shift again to the left and now instead of adding one zero to the right most position to the LSB position we flip that to a one by adding a one. And we can put this to the test by implementing these properties and then fast test them. So let's do this real quick. Let's call it test pop count. We don't need to check the first one we already have it covered in our initial test suite here. So let's start with the second one pop count P2. And we put in 256 unsigned integer.

So let's fortune out it's a fast test. Again it's a public view function. And now what we do is we compare we compute the twice the amount of x. It's two times x. One thing we need to make sure here now that is that we don't leave the value range, right? So if you multiply x by two and x is already 256 bit integer then that might leave our value range. So what we can do here is do a little VM assume that x is less than Let's do it this way.

uint 256 and then the max divided by two so we can safely multiply by two. Sorry? Okay? That's just something more we could could test but I mean these are the properties that that make sense.

But this I think if you if if you can show that this holds for an implementation that it is popcount. But we we I'm just using them as an example here. I mean What's the question? Ah, okay. So in in this Okay, yeah, yeah. Okay, I should have mentioned this. In this case, I'm not assuming any limit on the bit width. So just just integers. Okay. So this is why we have to make sure that we don't overrun here.

The Well, good. Okay. So let's compute the popcount of both of them. Bitops.popcount and then we do it of X and then we compute it of Y and then the property states that both of them should be equal, right? Okay, let's put it to test. And let's ramp up the fuzz test to 10,000.

Oh. Let's test fuzz. Oh, it's fuzz runs. Oh. What's the mistake here? PC of Oh, that's PC of PCY. And now it should What's Small typo. So, now it should be good. And we see we ran 10,000 different values for this and we couldn't find a counter example.

We can also check the third property by just copy-pasting this here and let's call it P3. And now we got to make sure that we don't overflow by adding one. And property states that popcount of 2x + 1, that's equal to the popcount of x and then + 1. And we can also check if this holds by just fuzz testing it and it seems to be okay.

Right, so are we convinced now that this popcount implementation is correct? I think No, I see Uh the the property function or the the implementation? Um so that anything that we put in here Can you Can you say it once again?

Exactly. The max value of Okay. Yeah, we can also have have a fuzz test about this. That's actually a good idea. So, that would be uh uh a more general test case. Let's call it max. So, you want to do something like And then we compute the pop counts. Um

There can't be more than that, right? Something like this? Okay. Oh. Oh. There's an error here. Ah, it's not necessary to kill. It's that one. Um I'm not sure what this counterexample is, but it should it should hold. Uh I mean, the test case is uh is perfectly valid. Um Ah, okay. Yeah, sure. That doesn't make

That doesn't make sense, but it should it should hold. Yeah. Okay. So, that also holds. So, we have another So, what we have now is we have uh functional equivalence test. We have checked two properties that the pop count must satisfy. And we also have uh checked that the the value range of the pop count is not uh violated. Then we have another question. >> So, we're basically fuzz testing different properties >> of the same >> of the same. It's It's not like a mathematical form of verification yet.

>> Not yet. >> Can we have that mathematical verification uh using some type of language? And what are the limitations of doing like this fuzz testing on on different properties? >> Thank you for the segue. Perfect. This is what I wanted to go into next. Um because instead of fuzzing it, and I think um so the the problem is here we tested a lot of of different values using the fuzzer, right? About 300 different instances now across all of these properties as fuzz tests. But now let's check if we can instead formally verify that the pop count is correct.

And as I said before, um so this now is using CVL. This is Certora's Verification Language. Instead of writing a test case, what we write is a specification. And we do this by first starting to declare which methods we are interested in or which functions, which is the pop count. Returns the takes the uint256 and returns the uint256. And now the the um major difference in writing between writing a test case and formal ver- very formally verifying something is instead of writing a function, we write a rule.

And now we can for example, uh use both of these properties that we had before and specify them as rules rather than as uh fuzz tests. And you see in a second that this is actually most mostly the same thing as we did in the fuzz test. So we Every input parameter x, um we compute the double of x. Let's call that y again. So again, we need to make sure that we do not leave our value range. But um in CVL, we have this handy function here required uint256. And this just makes sure whatever we put in there um it returns a valid uint256 bit integer.

Then we compute the pop counts both of X using pop count of X, and we compute the pop count of Y using pop count of Y. And we assert that both of them are equal. So, that's the first first one. Let's also check the second one. That is pop count of 2X + 1 is equal to pop count of X + 1.

Okay, so this looks very much like fast test case, but these are now formal specifications, and we can use our prover to let it or we can use the prover to verify them or try to verify or check if if they don't hold at all. And to do that, we're using our handy command line tool called Certora EVM Prover, and we point it to uh what's it called? To a configuration file. We can quickly look into this, but just basically it's just glue. Um we give it the contract that we're interested in, which is this bitops.sol, and we state how we want to verify it um by using the popcount.spec that we

just wrote. And the rest of it is just basically um optimization stuff. Okay, so if we hit enter, it should Oh. It should compile, but it doesn't. What's the problem? Ah, I said assert. And we still have one more error. Oh, and the same name. So, this is P3. Thanks. And now what happens is it goes off to the clouds. So, the prover is software as a service. You can in theory run it on your local machine.

And for this example, that would be totally fine. If you have medium-sized contracts or if you have uh larger rules, then you might quickly run out of of uh power on your machine. And so, what you see if you follow this link is our interface. And as you can see now that that a verification job is cute. So, we wait until there is uh capacity is free to actually uh run it. Uh because I don't want to wait now for this this talk. I have prepared that earlier. And what you will see is uh the following.

We can see to the left-hand side your rules. Let's ignore this for for a moment, which is pop count P2 and pop count P3. And as you can imagine that little Oh, it's a little too small, I guess. That little red cross here means that there's something something not wrong. And um in fact, it means that this vi- this property is violated. So, we can click into it. And we see the exact um assert statement that is violated. Let's make it larger one more time. Put that away. Uh because we only have one assertion in that rule, then of course this is this assertion here.

And what we can also do is we can inspect uh the value that we have to put into this rule into this parameter that will break the assertion. And this we can um inspect this in this variables tab right here. And we can see Oh, let's set it to decimal that it shows this seemingly random large integer uh that I'm not going to pronounce now. Uh as the input parameter X, and we can also see what it computed for the intermediary steps. So, for Y, that's supposed to be double of X. That kind of checks out.

And then it computed the pop count of X, which is 129. But for the pop count of Y, it computed zero. And that's cannot be true, right? Because the only only input to the pop count that is that is uh uh, then works out to be zero, is zero itself. So, let's check. Maybe the prover did a mistake here. Uh, we can copy that value and check for ourselves what happens if we put uh, that value into a test case. So, we can reuse the initial test cases here. Let's put that in here. What did the prover say about it? Should be 129.

And if we execute that, let's run this again. Doesn't need fast runs. We see it actually found an counterexample, or the assertion doesn't hold. And it turns out pop count of this number here is actually computed to be zero, which is a bug. Okay, so what do we know now? That this implementation in fact is not correct. And we've shown this by using formal formal specification and our prover. And now the next iteration would be check what's what the reason here is.

But um, again, I don't want to go through this bit fiddling. So, imagine we just feed it to an LLM and let it decide what what's going wrong here. And that LLM comes up with a different implementation by removing some stuff here that somehow is not needed. Whatever. And we can test it again. And now it seems to pass. Well, we couldn't trust the fuzz test before. So, maybe let's just check what happens if we verify it again. So, we use the same set of rules, the two rules that we had.

Uh, off it goes to the solver, or to the prover. And again, we have another cloud job. I don't want to wait until it's finished. So, let's check what happens. And now we can see we have a little green check mark next to our rules, meaning that now everything passes. And we are actually What this means is now we have mathematical guarantee that this pop count implementation follows the rules that we have. So, there's no value that you can put in these rules here uh, that will break this assertion.

Okay. Let's take a step back and recap what we just saw. Okay, I can take it from here, but I but I need to one more time. Okay, so let's compare what we've seen. We have the specification on the left-hand side here and the the fuzz test on the right-hand side, and they look pretty identical. And I'd argue that only the restriction of the value range is what's different in both. So, why did one find the bug and the other one didn't?

And that is that the the fuzz test or in fuzzing, what the fuzzer will do as I explained earlier, it will try 100,000, a million different values, whatever we give to that fuzz runs parameter, and check if it can break if one of these input parameters, like one one value for X can break the assertion down there. Whereas in formal verification, we have the spec and we translate that to the mathematical logical formula, and that formula already covers all possible values that X can take. So, we do not rely on the on the chance that the fuzzer randomly picks the value that will break or will find uncover the um the violation.

Um can we do it with fuzzing? Um of course, we can try. If we assume that this was the only bug in there, and this is only triggered by that value that I just showed, that integer, um then the probability of finding that with fuzzing would be one over the input space of 265-bit you and 256 integers, um which works out to be a probability of 0. and then you have 78 zeros 86. >> How many runs you have to do in the prover because we cannot see and when you are doing further you just set 1,000. If you increase the runs, so it's kind of a trade-off between how many

runs you have to do in the further consuming the resources whatever like the complexity and if you can give us how many runs in the prover side you have to to do. >> Um we don't do any runs in the prover side because everything is translated to a mathematical equation. And we do not have to evaluate that equation using random inputs as fuzzing does, but we solve that equation and if that equation has a counter example, then also also the rule has a counter example. So we do not rely on trying out different inputs. That already the formula covers all possible inputs that you can can put in. That's that's the main difference.

There's another question. Is that >> Uh how does the prover works and what are the limitations of the prover because right now we're just like abstracting this okay, we're going to put it in the server and going to run some algorithm there and then just prove something, but as I understand there's a lot of mathematically like known equations that can that nobody found ever a number that don't satisfy them, but nobody can prove them as well. So what are the limitations?

>> Uh good question. I don't want to go into the details on how the prover works. That would be off the topic. Um but there's actually one one prover that cannot prove certain formulas. It's not able to prove the question the formula. That is something that you have to take care of. That's one of the down sides of the formula verification and fuzzing. Um but there are ways around this. Yeah. Okay. >> Okay, sorry.

If it if it doesn't prove it, um so there is no um not proving it, it will just time out um after a while trying to prove it. And the guarantee that you get from that is that within the limit that you gave it to solve the the problem, it couldn't find a counterexample, but you can't also be sure that with more time it could have found one. That's the trade-off. Do you want to >> So the the issue is that you are absolutely right. This is a computationally hard problem. It means that it's doomed to fail in certain cases.

The way around it usually is that we break the program into smaller things, and we use modularity. So this the when it fails, it just usually has to do with the complexity of the code and the complexity of the property. And in principle, we can solve it giving enough human effort. So the idea is that the engineer puts uh his time or her time in writing a spec and writing it in a modular. And you can break the code into pieces. The nice thing about formal verification, unlike fuzzing, that it's not running. So you can break the code into pieces, and you if you have a code which is modular, it's usually more amenable to formal verification. If you have a code which

is like spaghetti, it's probably harder. >> Thanks. There There are more questions, yes. >> Yeah, so in in the pub count example, like you could uh you could like prove it with just like three properties. Like you need the initial state to be correct, and then 2x initial state gives the same result and then adding one increments up by one. Um how do you actually find these like properties which would guarantee that every state is correct for like a more complex system like a D5 protocol for example?

>> Um yeah, good question. So in this this this example I kind of just gave you like one solution and you you have to trust me that this is what we actually want to uh want to prove. Um and it's hard to give a an answer to this because this will depend on a state-by-state case on what you're trying to prove. Often it's in D5 um we see the same kinds of properties that we want to prove over and over again, right? So for example, in the lending protocol you don't want to make sure that any operation can make that go bad or um we have an I have another another example coming up that the vault doesn't become solvent insolvent. So that depends on what the protocol is ought to do and it's hard to to give a general answer to that question right?

>> [snorts] >> We're we're coming to this in a second. Okay, again, thanks thanks for the segue. Very good. Okay, it's true that um that example I gave you there was completely stateless. Well, we had a pure function that took that takes one input parameter and returns one value for it and it doesn't depend on the state of the contract or the state that the contract is in. And often that's not what we want to show or it's not what's interesting. But um we want to make some claims about our the state of our or we want to make some properties of our contract that depend on the state, right?

And this is often expressed as uh what we call invariants. And invariants is a property that holds true in all states that the contract can be in. And there's a this is what you were referring to uh a principle of induction, but it's not actually important how it's what it's named. Um we can make sure that an invariant holds by showing that it holds right after the contract is instantiated, so right after we create a new contract, and then we show that it is preserved by any state-changing operation. Right? So, any function that modifies the state of the contract make sure that if the property holds and we call that function, then it's not broken afterwards.

And again, um it's possible to show this or to check invariants um using fuzzing. And um this is done by literally doing what's what's um stated down here. We create a new contract, we check that this contract satisfies whatever property invariant property wanted we want to show right after the um creation. And then in fuzzing, um what we do is we simply call random sequences of methods using fast inputs and assert that the property is not broken by any any of the sequences that we call.

Right? So, we start by calling one function, assert that the property still holds, then the next one using fast inputs like with the pop count example, and the next one and the next one, and we assert that our property is not broken. And in fuzzing, uh what this gives you then is the guarantee um that in all of these states that the fuzzer explores uh that way by calling random sequences of of functions, that in all of these randomly reached states our uh property holds. Um that's totally viable, but the problem that you have now is that the amount of reached states that's that's way less than the states that are actually possible uh reach to reach uh in the in the contract because the state space is functionally uh infinite.

So, you don't want to wait an infinite time for your fuzzer to reach all of the states that you could potentially reach uh in in the real execution in which the property could be broken. Um you can, if you want that extra guarantee, um, you can again use formal verification. And so, the principle again from from a user's perspective side, uh, is not that much different from fuzzing. Uh, we also verify that P holds after the constructor, um, using now a rule just like in the pop count example. And then instead what we do is, we assume any state of your contracts uh, in which P holds, so the property, the environment that we want to check.

And then we check for each function that can modify the state, we check which state can we reach in after calling this function. Again, without actually relying to fuzzing uh, putting in um, concrete values. And then we verify whatever that state is in which we can end up, P still holds. And if we do this for all functions that can modify the states, um, then we have a proof that this property holds in all states. That's called the principle of induction.

Okay, so um, that's again a little uh, abstract. So, I want to make this one also clear using a small example. And this time I'm going to use vaults, like classic ERC-4626 vaults. Um, I'm sure most people will be familiar with that, but if not, um, that's just a vault just something that somebody or users can put in their tokens and they get shares in return for that. And later on they can redeem their shares for uh, whatever they're worth of tokens. And in the best case scenario, you should get the exact amount of tokens back that you put in by redeeming your shares.

And the vaults manage to do this by keeping a a conversion rate, which is the total amount of tokens that are in the vault at the moment divided by the shares that it admitted to uh, across all users. And one important property of such vaults is uh, what we call solvency, um, which basically reads that the total amount of shares is less than or equal to uh the total amounts of tokens. So, whatever we minted to users in shares is less than the amount of tokens that we have in our vault at the moment.

If the property is broken, uh then that means uh some user has some shares but cannot redeem it anymore because we don't have enough tokens in our vault. Okay. And I have a very simple implementation of a vault right here. Um right? So, we have a contract called vault. It is itself itself an ERC-20 because uh it means shares. And it has some underlying assets uh that we set on construction.

And it has some some queries to to to get the uh total amount of assets that are currently in the vault. This is tracked in a in a state variable, which is increased whenever we deposit into the vault and decrease whenever we take something out of the vault. And then we have our deposit function takes some assets um transfers the assets to the vault and means some shares in return. And we have the redeem function that then takes shares and um burns the shares and then transfers whatever these shares are worth in assets to the receiver we give it to you.

And so, we want to know if this vault is solvent. I don't want to go through the whole implementation here, but um instead um start with fuzzing again. So, we can create this vault also I have created this vault test right here um that has a fortune variant uh called uh invariant {underscore} solvency and it asserts that the vault's total assets are always larger than or equal to uh the total supply. And I set up the vault here. Uh you've seen this before what what's happening here in the previous talk by setting up a mock token then instantiating the vault with that mock token and then I create a handler so the fuzz test is not testing the vault directly but using a

handler and that handler just forwards has the same method signatures and just forwards it but make sure that for example if we call the deposit function that whoever wants to deposit something in fact has enough assets to deposit by minting it before that. Okay, so if we now run this invariant test here this fuzzing test uh we can again do this using forge test. So this is classical forge fuzzer. It compiles it now it takes a while uh because it will exactly do exactly this and call random sequences of methods on that vault and check that after each sequence the property still holds. And after a while we see how many

uh different function calls it did uh roughly uh 33,000 different calls to any of these functions deposit mint redeem and withdraw. A few of them reverted that's okay that's just a small amount uh these reverts come from overflowing uh the total amount of assets we can live with that. But more importantly uh none of these tests uh none of these functions sequences broke uh the invariant. Of course this is a much less sophisticated test than what we have seen before and you can probably uh come up with a way clever idea to test that and make sure that you have better coverage. But instead I want to make like take a look at uh how it would look like if we were to specify this invariant here uh using formal verification instead.

And for that we we just uh oh yeah it's good. For this one uh we yet again just create a new uh specification file which I've already done here. Uh we again start by declaring the methods that we're interested in which is the total supplies and the total assets. We also need the balance of users for some reason. And then we specify our invariants. Again, we call it vault solvency and we don't need an assert statement here, but we simply write down what we want to show, which is that the total assets is larger than or equal to the total supply. Now, if you were to run this, we would get some counter examples, and this is because now we have the opposite problem in formal verification that we have on fuzzing. In fuzzing, we only check for the states that we can reach by calling

the functions actually. In formal verification, we just assume a state where this one holds and check what happens if we call any of the methods. And that means that we can end up with a violation that shouldn't be that we wouldn't consider as a violation because that could not be reached in a in a real realistic scenario. So, first what we do is we make sure that the vault itself or the underlying assets, that they don't make any they don't initiate any transaction. I think that's a reasonable claim. And second of all is we need to make sure that the vault's total supply, that this is equal to the sum of the balances, right? So, if we have we have the balances of of the users in shares, and if we sum them all up, then this is

the total supply that we have in our contract. If we don't do this, if we don't assume that this holds, then we would get a counter example for example for example where we had Alice has 20 shares and Bob has 20 shares and that's all, but we have 60 total shares in our vault, and that would then completely break our a conversion rate. So, we also prove this invariant right here and require that this is true. But this goes now too much into detail. The reason is just we want to rule out some counter examples that are not reachable in a realistic scenario.

Okay, once again, we can run the Satorra prover um pointing it to uh configuration file. That one now looks exactly like the one for the pop counts but now for the solvency and the vault using solvency specification for the vault implementation and it's called solvency.com and then again it goes off to the clouds and after waiting for a while until the queue is queue is empty and it's our turn to run the job we will see the following we will see that this property is actually violated

what we see here now is what I mentioned earlier what is happening in formal verification or for these inductive properties we first have the solver or the prover show that the property the solvency property holds just after contract after contract creation like right after calling the constructor and then it checks that it holds after each of these methods is called and we see that it holds after calling approve transfer withdraw deposit mint and transform but it doesn't hold for redeem and I of course want to know why doesn't it hold for redeem and we can click into it in the UI and let's put that away for a second and we can inspect this by going through the call trace where we can exactly

follow along what the prover is trying to do and how it produced the counter example so it starts by asserting that the vault is in a solvent state right we have 15 total assets and we have 12 shares so that's solvent and then it checks the effects of the function that we're interested in which in this case is the redeem function and we are redeeming 11 shares and then you can now go into into all details what is happening here like really go line by line what the prover is doing to figure out the counter example right to to the exact operations that are being called and after the redeem function is done with these concrete

values. Um we assert that the property still holds, but it does not because because now the vault has zero total assets, but still one share is left, meaning that whoever owns that share cannot redeem it anymore for assets. Again, we could now really dive into here what's going wrong, but since we're time is limited, I'm going to give you a hint what the problem is. If we look back into our vault's implementation, uh what's what's happening is that we have this function here called convert to assets, which converts our shares to assets that they're worth.

And if we have a look at this line here, what it is doing is it's figuring out the amount of assets these shares are worth and then rounding it up. And that means that anybody redeeming some some shares gets slightly more assets for their shares than they're entitled to because we're again rounding up uh by after multiplying with the conversion rate. So the problem here is of course that this should be a mold of down. So that's um rounds everything down after after multiplying it.

And are we sure now that this fixes the solvency problem? So we can yet again run it after doing this fix. And if we do this, um again, we have to wait for the queue, but the queue is oh, wrong one. Queue is not important now. So afterwards, we will see that the solver and the prover and actually managed to prove prove our property vault solvency, meaning in any state that we can reach by calling any of these functions on any input, the solvency is preserved. So we have now a guarantee that we cannot break the solvency by calling these methods listed here.

Okay, um thanks. Great. Um Okay, so what have we seen here? Um to to wrap it up. Um If we do fuzzing or to compare fuzzing to formal verification, the um most important difference is that what fuzzing is doing, well, first of all, they look pretty similar. Uh the invariant looked similar to the first first invariant in formal verification, and the um the rule looked different. It looked didn't look much different from the first test.

But the uh difference arises from how the fuzzer handles these functions and how the uh the prover handles the rules, in that the fuzzer will choose randomly variable random values to put in into the parameters and try to check if any of these randomly generated values can break break the property that we're testing. In formal verification, we do not rely on chance, but instead um cover all possible input values uh at once in one formula. That also holds for the states, right? In fuzzing, uh we only cover random states that we reach by calling random methods sequences of methods. So, these are all reachable states, but these are not all states that are possible.

Whereas in formal verification, we cover all states at once. Um That can have some some um some problems in itself, some downsides, as we've seen. Um because fuzzing actually evaluates from the initial state of the contract, uh the states that we are in by calling the functions, we cannot generate false positives because all of these states are actually reachable. Uh that's not so much the case in formal verification, uh where we can get uh false positives as violations uh because we we assume the the contract is in a state where the property holds, but that state is not actually reachable by calling any sequence of methods.

And then there's another difference in fuzzing. The good thing is that you can do fuzzing with whatever framework you're using to develop anyways. So, there's little to no learning curve here. And formal verification, instead you have to learn a new language, but I hope I could convince you that it's very similar to Solidity in that case. And the most important difference here is the guarantees that you're getting. With fuzzing, the guarantee that you get is a probabilistic one, right? So, we know for the random values the fuzzer choose our property holds, but we don't know if there is one value lingering lingering around that the fuzzer didn't choose that will break our property.

And for formal verification, what we get as a guarantee is a proof that the property that we are verifying actually holds on all possible inputs inputs um that we can use. Okay. To wrap it up one more time, automated tools can help us find bugs in our contracts. We can use fuzzing for that. That's easy to do, but has limited coverage. We can instead do formal verification, which has perfect coverage, but has some some learning curve to it. My suggestion here is use both.

And I'm shying away from giving a concrete recommendation what to fuzz and what to do FV on. And just a recommendation is start early. Don't do any of this as a second second uh consideration. Start as early as you can with fuzzing and formal verification to cover bugs or to disclose bugs as early as you can. And yeah, with that I'm done. Thank you for listening and thank you for your questions. I'm happy to take questions myself afterwards some more.

By the way, there's a QR code and you can register there and you get a free prover key, Uh, is quite generous for um, medium, small to medium-sized contracts. Yeah, one question. >> Like, in terms of development and engineering cost, what do you think it's the best approach? Like, do do formal verification first, fuzzy first, or mix? Yeah, when you start from the ground up a new project.

>> Oh, that's uh, that's a tough one. Um, well, that's a personal personal question, I guess. I would start with testing and fuzz testing first, I guess, when you go bottom-up developing and check the the implementation details in unit tests and fuzz unit tests. And then as as the way as you go further to your concrete to full implementation, and you've figured out what your key invariants are on your protocol, like the really the economic important things, then I would do formal verification for these. So, that's basically a rule of thumb that I would would suggest.

>> And then you can start like a feedback loop to >> Yeah, exactly. And then you can use both the fuzz tests and the specification as regression to make sure you don't break anything. >> Okay, thanks. Okay. If one more question, yeah. >> First of all, thank you for the talk. I would like to ask you if you can briefly talk about maximizing an impact through formal tools.

>> I I can't I can't hear you. >> Um, okay. So, could you please talk about maximizing an impact, like say you shown the insolvency, but how would you go about showing an insolvency that is perhaps of a higher magnitude by using the prover. >> Of a higher I I'm not sure if the microphone's working. >> Okay, I'm going to just scream. So, can you show me a higher magnitude of an insolvency with the prover? How would you go about doing that? >> Um Ah, you mean so insolvency with with a difference being more than 0.1?

>> Yes. >> Um yeah, you can you can do this. I'm not Yeah, let's go into it. Well, let's not do it in code. That would take too much time. You can inject into the into what we're trying to prove in these rules. You can inject requirements that the prover has to fulfill while trying to prove something. And if you add these requirements, for example, saying that after doing something um the insolvency is is the difference is I don't know N, then it will try to figure out a a counterexample for that.

If that's not possible, so then if it if it passes that rule, then you can be assured that there is no counterexample or there's no bug that can lead to an insolvency of that particular range that you're testing for. So, that's definitely something that you can do. >> Awesome. Thank you. >> Sure. Okay, if there no more question, then thanks again, everyone. >> [applause]