Securing your protocol with the Certora Prover

Transcript

So hi everybody. Thank you everybody for coming. Today we're going to talk about securing your protocol with the Sattorra approve actually how to formal formally verify it. So I'm Pamina. I work at Sattorra. I'm the formal verification team lead and Sattorra is a web3 security company and um we're doing uh all kinds of uh things uh that you might need for security in DeFi and uh especially we also have a tool called the Satra approver that can do various things and today I'm specifically going to talk about how to use it to verify some smart contracts and I'm going to

try to convince you that it's easy and if you're a solidity developer you can do it too. Okay. So what is formal verification? It is according to Wikipedia the act of proving or disproving the correctness of a system with respect to uh certain formal specification or property using formal methods of mathematics. Well, that sounds uh very long and very boring, but what this means basically all of your protocols, if you write a D5 protocol, you have some key invariance and we can if you know what your what your needs are of the the protocol that you want to write, right? There are some uh inherent specifications or and

assumptions that you make about your code. Now we can formalize them and we can use mathematical tools to actually show that the way you wrote your code satisfies these properties and that is exactly what we want to do uh at Sattorra with the STORA prover. So let's start with two truths and a lie about formal verification. What do you think the the lie is? So the first one is formal verification finds bugs. The second one is formal verification can mathematically guarantee that your protocol will remain solvent. And the third one, formal verification is hard and requires a PhD to be successful. So what do you think the lie is? One, two, or three? One,

raise your hand. Two, raise your hand. Anybody? Oh, you all think we can do this? Cool. Cool. Um, and number three, anybody? Yes. Yes. That's my opinion too. Um, wonderful. So, let's look at the first one. Formal verification finds bugs. Actually, we can find all kinds of bugs and especially the super strange ones, right? The ones that are not as obvious. So, we can find rounding errors that are not super obvious. For example, recently in a project, we um we basically found a rounding error in a moldive that was meant like that used a classical

integer-based algorithm for a ceiling mold operation, but it was actually used on fixed point numbers. Well, it didn't work out so well because the ceiling just didn't work. Like the the ceiling was basically just didn't do anything. Um we can find all kinds of strange edge cases like for example you're in some particular state where you have a very very high values in storage or very low values in storage and uh we can uh all of a sudden see that if you deposit at this at that particular state the share value in your system will decrease.

That's not something you want. You we basically with any operation you do in a D5 protocol you want to make sure that the share value either stays the same or increases right. um we can uh find bugs in with compliance issues. So for example, recently we had um um we we came across a bug in where there was a protocol they had a withdrawal queue like a redemption queue um and they claimed FIFO right so you if you withdraw you're going to be in the queue and as soon as there is liquidity you're going to get your liquidity out there.

Um turns out it could be circumvented. We can show that these things are possible. But most importantly, we can also ensure that when you provide a fix, it's actually fixed. Next thing, formal verification can prove solvency. Yes, we can. And we can prove way more than that. We can prove uh for example in lending protocols that a a well collateralized like a healthy account uh that is not uh that has a healthy LTV uh remains healthy unless a pricing action um tips them over right but not by any user action you cannot become unhealthy we did for example prove that uh for the oiler vault kit uh

we proved solveny in unis swap but we didn't only prove solveny we can also prove uh that your share value does never go down. We can prove um compliance um things like we we said before about like uh your redemption cues that everybody that your users are treated fairly but we can also make sure that if there are rounding errors that the users cannot take that like uh take advantage of that. So um those are the cool things that you can do with formal verification. Now I'm trying to convince you that you do not need uh a PhD especially not with the Sora approver because the Satara approver was specifically designed to be simple to use for solidity developers. And to that extent we have the Storra verification

language. We're going to do a little tutorial um after this intro. And in my opinion if you can write solidity you can write formal specs. If you understand what pre and post conditions are you can write formal specs. And if you don't know what pre and post conditions are, you know what asserts and requires are. That's that. Um, so if you can write code that looks somewhat like this, and I'll explain what the parts of this code are, you will be able to do formal verification. Okay, let me give you a bit of a background into the solidity part of the STOR or the the STO approval in general.

So basically we take your solidity contracts. We take a spec file and then we feed this to the STOR approver and the Stor approver will give us either um a proof that means that in any reachable state of your program the the property that we want to verify is is actually satisfied or we find um a weird rare behavior like a very a concrete state with concrete numbers where uh this behavior is violated and that is often a bug. Now, how does this work internally? That means we we basically take the spec and the solidity and we internally translate this to so-called verification

conditions. So, we translated to logical constraint formulas and we feed those to so-called SMT solver satisfiability modulate theory. Um, that's that's what's going on uh in in in simple terms under the hood. Uh but we're not super concerned about that right now because you actually don't even need to know any of that to use it. Um what is impo what is very very important and what cannot be stressed enough enough is that we're doing uh a sort of symbolic execution right it's not testing it's not fuzzing even if we write super simple properties that look like a unit test it's not the same as a unit test because the prover

will look into any possible state um like any possible state that is reachable in your program right it all the pos like all the inputs um are non-deterministic. So it's proved for so if you have a UN 256, it will be proved for any UN 256, not one concrete one. Um and the same goes for all the com the different branches, the different computation paths your program can take. All of them are considered. So um why do formal verification? you just add another layer of security uh on top of traditional ones like testing, fuzzing, manual code audits, etc. Um, and what what you want to use it for in

in my personal opinion also is you want to ensure the key invariance of your protocol like the the basic ideas that your D5 protocol, your smart contract should do, uh, those should be formally verified to make sure that your users cannot get wrecked. Um good. So that means a proof holds for any kind of uh state uh any reachable state of your program and a counter example is one particular state that violates it.

Okay. Uh some of you saw this already before. Um we will now go over to the practical portion. I will put my mic here. Please let me know if you can still hear me. Does that work? Can you Can you hear me like that? Okay, cool. Um, so we're going to do a little bit of a CVL tutorial with some very basic rules and I'm just going to jump. So, if you open this link, you will see um the following tutorial and you can just jump ahead into the first one if you want and follow along.

I'll jump over now to the actual code, right? So the first thing that we're going to look at is a very simple coding uh voting contract and it just has one mapping. Uh it tracks if um if the the people that voted already have voted, right? It just tracks true or false for each of those addresses. Uh it it's uh has votes in favor, votes against, and it counts the total votes. And there's only one function vote.

Now what do you need to do to verify um uh this con this very simple contract with the Stor approver? You need two things. You need a spec file and you need a conf file. The spec file is where we put our formal specifications. And this is our first rule, right? So this you can see here uh this is basically what what this looks like. We have a rule here vote integrity that just checks that the total votes are increasing um whenever you call vote. Okay, some things are going on here. So first of all, we have the keyword rule.

Instead of function, you just write rule, right? Um you give it some name like you would a function. Then we have this special um environment variable. The environment variable you can by the way you can declare this as a parameter or you can declare it here. It doesn't really matter. The environment variable gives you all the um EVM environment things, right? It can give you you can have the message sender with E dot message sender. You can have uh the block timestamp with E.Block timestamp. Okay, this is just the CVL version of of of all of these things you already have in Solidity.

And basically what we want to do is we want to save the states of the total votes into a variable before we execute a function. That's the voted before. Uh then we declare a variable is in favor that we use as a param to send to the function. But uh this is very important. I do I I declare it but I don't give it a value because it's nondeterministic. So it can the prover will know this can be any boolean. Boolean is easy. So it's either true or false. Uh but if it's if this was like a uint 256 let's say then this would mean any any value that u 256 could have. Okay.

So uh then we call the function. We call the function with this environment because um in this case this function depends on the message sender. So it's important to actually give uh the the call the symbolic call um the information of the environment. Um the total votes here for example are so this is the methods block. We can do a bunch of things in the methods block but for now let's just say we declare here functions of the contracts uh uh that we want to verify. And in this case we just simply say here this is n free that means I can call this function without passing the environment variable because this is just a getter right I don't need any information about message sender

block something um and then we write the assertion and in the assertion we could of course we could have done also this voted after is total votes or we can uh just call it directly in the assertion once more and just make sure that it's more than before. So that's that's our first rule. Now the other thing that we need to make sure is we need to make sure we tell the prover what kind of files they it it needs to and and what kind of things it should verify. Right? So to that end we have this conf files. the JSON 5 format. Um,

basically you want to um specify here all of the files that are necessary for you to get like um sent to the prover. And the way we specify it is so the Satara we usually put all of the Storra stuff outside of the source directory. And so in this case we want to um use the voting box uh file but the contract is called voting. So we have um this colon voting here to specify that we want to use that contract and we want to verify that contract with the specs that are in a voting spec voting box spec right we can pass a message this you will probably not need I'll need that so that it's not

running locally on my machine but I send it to the cloud you'll see in a second and then you pass whatever uh soulc version uh you use I personally use soulc select so you can just put here. Sy um and then we can go over to uh the terminal and you just go to the basic directory and you can run the tool uh by simply saying run and pass it the configuration file and up. So, we want to just do that.

This is not the super interesting part, right? So basically what's happening here is just compiling the solidity files and sends the the by code over to the prover and then you get here um uh the link to the prover output. So we can click this or we can do what I usually do namely go to the job list and see this is the latest job that I was u sending here to the prover and this is what the output looks like.

This is too small I guess to read, right? You tell me once it's okayish. Yeah. A bit more. Can I? Okay. So, as you can see here, these are the rules. So there are more than just one the one rule the vote integrity rule but there's also this like nfree static um check and that basically just checks that the why why can I not see this now there we go um it basically just so the

first rule just checks whether these end free declarations are fine so that the methods that we're using here are actually not using any environment information um and then we can see the vote integrity has a bug. Nope. And here we have a a couple of other views. So, first of all, we have this local variables tab. So, the local variables tab here, you can also see what you have in E. Uh, so we have a message sender that is 0x41 address. Um, we have voted before is 0x3.

Usually you get a hex output but um you can also make this decimal so it's easier to read. So voted before is three. And um here you can see the call tree. So we get a counter example and for the counter example we get the exact computation path that led to this specific counter example here in the call trace. So there's a bunch of things going on here is like some the the the states that led to the counter example is um set up here. So we see there is um uh in the voting contract there is a has voted field. We've seen it before uh with the address um for 401 did not vote yet. The total votes before were three.

The votes against were 590. So we al already maybe see another invariant that we're missing here. uh namely that the total votes should be the sum of something. Um and then we can see the native balances of the contracts in the scene which in this case uh what we're looking at right now is not that interesting. Um then there's a bunch of setup things happening mostly you can ignore this uh if you want to find bugs or find proofs. Uh but what is interesting is the before and after right. So if we open this we can see for whatever reason uh the total votes after are one. So here's like the what's happening in the in the voting

that's the voting before that's the call to votes. Um so we can see the message sender is this 401 contract. Um you can also let me just make this a bit bigger. We can also jump to source and then you get um at least for so for example here we can see uh here it stores voting total votes one so clearly that's the bug if you guys haven't seen it before I uh I removed the plus so we have a bug um and and that's basically how it goes we can see that the votes enhanced uh

increased by one uh but the total votes were just reset to Z to one and that's why we have a bug and then we can of course go to our voting box spec not the spec but the solidity contract and fix it run it again and check that it's proven. This will take us about a minute.

Okay. Meanwhile, We've already seen we might we maybe want to write another property right namely that the total votes is the sum of uh the votes against and the votes in favor. So I'll start writing a rule total vote sum. We'll call the vote function. And we want to assert that the total

votes is equal to votes against plus in favor. Okay. Do you think that this will work? Ask a question. Sure. How how do over how do overflows play into this? Um it it depends, right? I mean, if you have um so we model a UN 256 as a UN 256 in the logical constraints. Um in this case, the overflow is not the issue.

So in this case, there's a different problem. So I was I'm I'm talking a lot about invariance, right? How can we prove that total votes is the sum of the votes against and votes in favor? Um that it holds in every state. What do we what do we need to assume something here? Exactly. We already do that. So remember the the prover will assume any starting state.

Of course you have to increment one before the other. Of course you have to increment one before the other. It's impossible to increment both at the same time. So at some state you will have one and the assertion will fail. But we don't start in with a zero state, right? We start in a random state. Exactly. Could you repeat that with the mic?

So we have to ensure that we start from a state which is already valid otherwise in an invalid state you can vote whichever way it'll stay invalid. Yes. So how would we have to constrain it here? Any ideas? in the back. Maybe we can constrain maybe you have some I don't know decorators to constraint when this rule will apply. We will we have requires so what would I write here? Can you repeat

something like conra contract is initialized or something like that or it's not the initialization that's the key. We can be in any program state, right? We can be in the middle of exe like the vote function could have been already executed a 100 times. Is it your assert but with the assert changed to require exactly and because it's an inductive invariant right we and what we're doing here is we're proving not a base case like after the constructor but we're proving a step case of the contract. So any uh executing any function is actually um if you think about it in induction terms, mathematical induction terms, it's a

step case. So what we need to do is we need to require that we are in a valid state. We need to apply the induction hypothesis. You see? And now we can run it and probably get a proof. I can also pass here dash rule and just run this one particular rule now.

Let's just see. Okay, cool. So vote integrity has now been proven. Our property about uh the total votes has also been proven. And I just want to show you what happens if we remove this to make it a bit more clear maybe. So the counter example that we get here

looks like the following. So we see the votes against and votes in favor are more or less the same number as the total votes. And that is because in the setup already it has been set up in such a way that already violates our invariant of course and after calling it once like the vote function calling it once will still violate it. So we have to assume we're in a state where it already holds.

Um, okay. Now, let's say we don't want to write this for every function. Let's say the the voting buck contract has another external function do nothing that is now empty. Um, but basically we want to make sure that for any function it's verified, right? So we can go ahead and write a so-called parametric rule. So let me just copy this for a sec. So instead of just calling uh vote here, we want to call any method of the contract with whatever

arguments um it needs. So rather than declaring here bool is in favor I can declare some method f the proofable know it's from one of the methods from the contract that we're verifying and I can um say call data arc arcs and then the prover will know use whatever arguments are necessary for the particular instantiation of f that you're currently using. So this way I can basically uh prove the total vote sum holds for all of the functions of the

contract. So if we run this now So as you can see now the prover instantiates

um actually you can see all of the step cases that we're doing currently right. So we see it for for vote it's proven but it's also proven for all of the getters and it's proven for our do nothing. Um of course the question is is this necessary in this case it's not right because the getters don't really write to the storage so it won't change the state. Um but um we actually have something to make this your life easier and you can when you have a property like the one that you would require in assert we actually have the keyword invariant and then you can say total vote sum invariant and

then just write the invariant. And if we run this one So basically something that the invariant keyword that you will see in a second is doing

in contrast to the parametric rule is it will only run this invariant on any kind of function on any kind of external function that could technically change the state. So no gathers no few functions and it does that without you having to deal with it basically. And that we will see in hopefully a sec. Sure.

of those functions or function as well uh at the be the so it assumes it at the beginning of the function and then it asserts it after uh after the function is finished. Okay. So hypothetically hypothetically the the invariant could be violated in the middle of the function so long as it's restored when the function returns. Okay. Yes. Yes. So what if my function theoretically has some point of re-entrancy where eventually the execution would circle back in a state while the invariant is

being violated? Would this catch that? I'm guessing yes. But can you can you say that again? So I made a terrible mistake and left a re-entrance bug in in my code. Yeah. And and this can be exploited in a state where the invariant is doesn't hold then uh we will probably find that. Yes. Right. Yes. But we can we also have rules that check for re-entry even I'm guessing. Yeah. Yeah. So the the one thing that I wanted to point out here while um the reason for why I was waiting for that run is that the invariant keyword also checks the constructor. So that's the difference

between a step case and a base case. Uh I have it outlined uh I think here. What is what I want you to understand is what we're doing under the hood is structural induction. So let's say we have a contract with a constructor. The constructor is our base case. So that's what you were referring to. We initialize the contract and then we just assert it. We do not require anything on the initialization. We want to make sure once the contract is initialized, it's it's actually the invariant is satisfied. And then for any of the external functions that can change it, we assume that we're in a state because the base case already proved it, right?

Uh that we start in a state where this is satisfied. So we require it. we execute whatever function symbolically of course and and then assert it again. So it's nothing else than an inductive proof. Cool. So that's the first part. Um can you read this better? Um let's move on to something a bit different. Uh it's another toy example but it's a it's a bit uh a different one. It's a minimal token in an ERC20 style, let's say. It has um a mapping for for balances. It has a mapping for allowances. It has a total supply. It

has a a transfer and a transfer from function. And it has an approved function. And it also has a deposit function. And this deposit function is a payable function. So if you want to deposit to our minimal token, you need to pay um whatever amount like the message value needs to be bigger equal that amount. Um and that is then put into your balances of the message center and total supply is increased etc etc. I think you get the gist and then we have here our uh small little spec. So we declare again uh we used balance off and total supply here. So we declare balance of and total suppliers and free

because they're are just getters. And we have two invariants here. First of all, we want to make sure that the balance of the zero address. So we don't need to cast uh to address here in in in CVL. We can just use the zero directly um is zero. And then we want to prove at the token solvency namely that the that the ETH balance of our contract minimal token is at least as much as its total supply. Make sense? And this native balances keyword is our um nice CVL way of saying that's the ETH balance of of of whatever address you put here. In this case, we have this keyword current contract as well. um

that will basically um be the contract that you put in your verify clause in the conf file. So in this case the minimal token. Cool. Okay. Now let's maybe run this So we see cool the first invariant that

uh the zero address has no balance is satisfied in every state. Um however we found a violation in the token solveny rule. So let's check for which function the deposit function. So let's see what's going on in the call trace. Basically um let me just put this back to decimal here. So we assume the uh invariant in the pre-state, right? So we have a very large token balance of minimal token. Um we have a little bit

of supply and clearly uh the balance the ETH balance is bigger than the total supply. And then uh what we um want to ensure is that the minimal token balance uh is still bigger uh equal to total supply which is not the case anymore here. Now why is this the case? So we can see like something happened weirdly in the deposit function that made our total supply explode. Right? That is clear I hope.

So we can check the effects of one of the steps taken which is the deposit function. So we can see what's happening here. So we see there is an amount deposited that is really really large. But if we look at the balance before and after, even if it's very very long numbers, I think it's clear that they're the same. We can actually um maybe see this here or not. Well, um, so you can see basically this is the

same as this number here, right? And all of a sudden this is almost the same too. So what do you think happened? What do you think is the bug? Yes. the amount when you transfer message when you transfer message value but you adding to the mapping amount. So you can transfer any amount that you want and transfer less for example message value. But how is it possible that the total supply increased um but not not the value not the balance. Yeah but you you transfer like the function. This is the function right? Yeah yeah yeah. So you you you basically

I don't know maybe because you so we use this amount we we increment both values with the same amount right so why did one increase and the other one did not anybody think of such a situation uh good idea but No, it's not an overflow issue. Think about the message. Who can be the message sender?

Any address, right? Sorry, I'm not hearing it. any address any any address can be the message sender. So how do you think it's possible that if we send this amount contract and the constructor of the deployed contract you are doing like deposit so you are calling to deposit when you are deploying new contract and the constru you're thinking even uh you're getting I I think you might be getting in the right direction but

you're thinking way too complicated. If you call deposit and just one of the values and this is this is a payable function, right? It's a so whoever calls this it's it's going to remove the amount if if it's if the same contract it's also it's not it's not re-entry. It's not it's not that it's the contract to depositor. Yes, exactly. That's the correct answer. So the actual contract that we're trying to verify here is the message sender. So it pays to itself which increases the total supply but not the balance.

Make sense? Any any any questions on that? But we can we can actually see this in the in the counter example. So let me just see it actually says it here. So sender is minimal token. And then what happens here is okay the message value is big enough na no and then um of course it's payable so it removes it from the native balances but it doesn't uh and then adds it again and it adds it to the total supply but the bal the native balances won't change.

Cool. So that's that's one of these examples. Okay. I have one final example for today. uh which is a bit of a different contract. It's what do we have? It's the power voting contract. So the power voting contract now is another voting contract but it uses our minimal token and so the idea is now you can vote with the amount of money that you have. Okay. So we have a mapping uh amount voted uh we still have the mapping has voted. We still count the votes in the the votes in favor votes against. We have now the minimal token

and call it token. We still have like uh total votes. The total votes now are uh the are now based on the balances uh in our minimal token. So uh the total votes are the votes the is the token balance of uh our current power voting contract. Um voting has some some period here. So um so there is a way of ending the voting period. Um and the voting power is the token balance of the message sender. Okay.

So let's see our spec. Um we use uh again the vote integrity rule that we've seen before that the total votes are increasing if somebody votes. Um and we have uh also the the sum and variant and just let me show you quickly um how we set this up here. So we um have in the power voting conf uh we say that the so we we have to include first of all we have to include both files. So the minimal token uh fixed or in this case we used a fixed token.

Okay. Um uh so we have to include both files both contracts and we can then say in the power voting contract the token is meant to be the minimal token. So this tells the prover to resolve any calls to token to the to the actual external functions that are defined in the minimal token. And then we can go ahead and run this. In the meanwhile, let's fix the other

problem. So, what is the problem with the the function in the minimal token? We're missing a requirement here, right? We're missing that the message sender shouldn't be address this. I'm running the wrong spec.

Sorry about that. by the way, if you want to like look at this after as well or just keep continuing. We actually also have um all of the rule reports here in this um

little tutorial. So we can see it here too. Now let's see about the output. Okay, so we see we get some violations here, right? The first one is the total votes did not increase in this very very simple rule, right? So we can see here somebody calls votes but the total votes did not increase.

Total votes before after is 14 and before is also 14. So, one of the issues that just jumps at you here is that the transferred amount, remember the voting the voting uh function now needs money, right? If you don't transfer anything, you're not voting. Basically, you can still call the function, but the transferred amount is zero. So, it won't have any effect. Um, so in this case, actually, what is happening is our specification changed.

So, it's not actually it's not a bug necessarily in the contract, but we might want to make sure that if the token balance is zero, the total votes before stays zero. And if the token balance is actually greater than zero, the total votes um is bigger than the voted before. So we can also al also have multiple assertions in one rule. And then if we rerun this part, it called voting vote integrity.

What did I do? So this should work out now because we take care. Now let's uh let's see what the other invariant um did. So we see that the total votes is some invariant is also violated in one or more of our step cases. So what I did here uh is a is another step. So we can see uh we can actually run our invariance not only on one contract but on multiple contracts. In this case we want to run it on the power voting

itself but also on uh the minimal token. And we can see that any kind of um any kind of um method that transfers any tokens in our minimal uh transfer actually uh has some issues here and find some counter examples. So let's let's try to understand what's going on here. So we assume uh the votes in favor is zero votes against is two total votes is two. So great the sum is fine and then uh the votes in favor um is still zero votes against is still two but the total

votes is three. So what do you think happened here? Did someone just directly send tokens to the Yeah, someone donated. Yes. Yes. Someone just uh for fun donated crates, right? Um but that is basically uh that is exactly the bug that's going on here. Okay. Um that's it from from for this short uh Serto verification language tutorial.

Um, here's a bunch of interesting links. If you're if you want to use the prover, get us get yourself a Shatura key. Uh, it's the thing that you need to be able to send things to the cloud. Uh, we're also open source, so if you want to be a contributor to the prover, by all means, you can do that. Um, and, um, you there's an installation guide. We have a lot of more tutorials, uh, etc., etc. And if you want to use it, uh, please do so. Um, also there might be another interesting factor that plays in here, namely that we're hiring uh specifically for formal verification engineers. If you want to help protect DeFi in this in this way, um, please let me know. You can come to me. We have a booth today

too. So, please visit uh and you can find me on Telegram if you have any questions. If you're interested in the work that we do at Satara, uh, please connect and uh, and let me know um, if you have any questions. Thank you guys. [Applause] Thank you very much for this explanation. Do you have any question? So one thing I'm wondering about is reverts. So, so like in your last in your in your power voting example, uh I I couldn't easily find this the code for the contract, but if someone tried to vote and send no tokens, would

the call have reverted? Um it depends. If you have a require, it would actually have been reverted. Something that I omitted from this tutorial is that whenever we call symbolically call a function in a rule, uh the way I did it just plainly calling it, it actually assume it actually just the prover just checks all the computation paths that do not revert. If we want to include all of the computation paths that do revert, we have a keyword namely we run like instead of vote, we run boat at with revert. And that way we can also um incorporate in the in the proofer checks all of the revert cases. But what we want to do most of the time is in a

successful run that changes you know the states we want to prove some invariance. Sometimes we also want to write rules about revert conditions like for example that's where the overflow comes in often right we want to make sure there is no overflow of something. Um we often find of course it's it's very easy for us to find any kind of unsafe casting um with the with the prover uh but yes I omitted this part and so if you say check check paths with revert as well is a revert considered a satisfaction of the envir of the thing you're trying to prove or

or a violation it depends on the property if it can violate if if revert can violate the property. It will find a violation. But uh like in the power voting example, if if we said check reverts as well, would the proof still have gone through? Uh for the invariant, I think so. Yes. because I don't think that u if if a function just doesn't go through then the the sum wouldn't change but it would still find the same counter examples it found now okay make sense a little okay a little we can talk about it later if you want to

hi thank you so I was wondering what are the comput computational requirement to run this software Well, like can it happen that your smart contract is too complex and then you just run out of time for proving? Uh we do encounter timeouts for very very complex D5 protocols with very very complex properties that uh need a lot of computation paths right you saw like these these like small examples are done in a minute or less. Um, of course this is not the case for a lot of our clients like when we write um rules for for our customers. Uh that might look a bit

different but most of the time we still solve it. We have a lot of things going on under the hood to make for formal verification actually tractable for the real world which is really cool. Um but from time to time there is such a thing as timeouts otherwise we would make something undecidable decidable which we don't which we can't. Um so that's that's basically the gist of it. We have a lot of ways to tweak the prover to tweak the underlying SMT solvers. Um the configuration files usually look much larger and have way more specifications than you saw just now for the complex uh programs but uh from time to time it's yeah it's uh it's

not possible to circumvent timeouts completely. We don't have any time for question but you can keep after. Thank you very much. Thank you.