Fully Automated Formal Verification

Transcript

i'm not sure about the livestream hi everyone good morning congratulations on being here that early um yeah it's early i'm kind of slow maybe martin is too but we'll make it all right my name is leo this is martin we work with forum verification at the ethereum foundation um yeah and we wanted to go through um

the idea of fully automated form verification and see how far we can go in terms of verifying actual real world contracts as opposed to tie contracts which we do play a lot when developing new features and fixing bugs this kind of things so i'm going to start talking about some experiments and then martin will take over to talk about some hevm internals which is on the tools we're going to talk about and heads up right after this talk martin will lead a formal verification workshop right across the hallway at room bf or however it's pronounced so we're going to be moving right away um after this talk over there and run a few live demos and

also chat more about everything and there's a lot of overlap between these two talks didn't say anything first all right um so the goal of this experiment was to run over a few examples and see what we can get from fully automated form verification tools so how many people here understand this overall okay cool so this is the first contract we're trying to verify it's a solidity token contract a very simplified version of the usual erc20 contracts we have of course i

removed a lot of stuff here because i wanted it to fit on the screen so here we have the basic constructor that basically sets whatever amount to the owner of the contract which is the sender and here we want to verify the function correctness of the transfer function which just transfers a certain amount from the message center to someone else and then you verify that the sum of the two balances does not change after this transfer so we want to verify that this assert is true it must always be true otherwise we have a bug in our program the second one is an amm so an automated market maker um which this is also a very simplified version of in this contract you can find

this kind of contract in unit swapner exchanges where you can swap one token um to the other so in these contracts usually so this is an example that i took from david terry also from the form verification team so here we have the contract that has two tokens that we will want to be able to swap say for example die and uracity and some actions you can do in this contract are you can join the contract giving a certain amount of each of each of the tokens you can exit the the market or you can swap one token where is this you can swap one token to the other um and the price for the swap is calculated

over this constant formula that we have heard so much about x equals x times y and we want this constant to never decrease so this is the property we want to prove statically the next example is going to be the deposit contract i'm not sure how much you can read from this it's quite a lot of code but this is not a simplified version so this is the actual deposit function from the deposit contract that was deployed um last year so the deposit contract is the eth2 deposit contract where validators must deposit at least 32 eth to be able to be a validator on the beacon chain so this deposit contract has

a merkle tree of all the validators and it was formally verified by runtime verification we have ricard here i'm not sure if he worked on it but he works for rv and they first verified the viper version and then they decided the team that coded the country decided to swap to solidity because of gas costs and um yeah this is the final version and we want to prove that this assertion here at the end of this function is never reached so we want to prove that this loop always terminates inside this branch here the next one is a snippet from the opensupply implementation of the erc777 token what this token does is

it's basically a normal rc20 token plus it has the feature that it calls back both the receiver and the talker whenever transfer is made so there's this this interface for the sender for the recipient and both of these functions in each contract if there are contracts and they are called whenever there's a transfer and the property we want to verify is that whenever these callbacks are called so here tokens to send tokens received we don't want them to mess up with the total supply of the token so these two properties are what we want to prove okay so the experiment is basically to try to run some tools that are fully automated or almost fully automated basically relying

on a small and simple specification where so far i only show specification in terms of the assertion that we want to prove is always correct but some of these tools will require a little bit of a spec and if the tool was not here is because it either requires a more step a more complex type of specification like a for example or they are not um fully publicly available which i wanted to for for this experiment because i just had a script that ran everything so i wanted to just have a binary and run stuff um okay so the tools that i ran here were mithril which is symbolic execution tool for avm byte code

it's very fast but also very simple it does simple things hvm which martin will also talk about later it does symbolic execution similarly for vmware code but also in variant testing which echidna i never know how to pronounce it echidna also does it very interesting and then finally the smt checkers also verify and very smart try to do unbounded model checking so fully complete and about model checking but on top of solidity code it doesn't handle evm byte code only high levels limited code and we want to run these tools and see which ones can prove or break the properties i wrote before automatically or with a little bit of of spec so if you can guess which tool could either

prove correctness or find bugs in all the examples that i showed smg any other guesses ah no he spoiled sorry without false positives well my question was related to without false positives so here's the answer none of them did it [Music] one possible reason is not only automated but formalification in general is undecidable which means that um there's no possible algorithm or anything that will solve every single instance of a form verification problem so that's it

um okay so it's undecidable we can't really solve for general case so there are several different approaches that have different pros and cons that a lot of people develop in the wild and one very common approach is to either target vmware code or target solidity high level code some things against the approach of targeting solidity is first of all you have to rely on compiler correctness so everything you're proving you're proving a high level not exactly on the bytecode you're deploying so you still have to rely on the compiler being bug-free and there's a lot to encode high-level features there's various data types pointers inheritance there's just all sorts of really complicated stuff

that's hard to encode when generating the formal model of the contract some pros of this approach are you have a lot more structure and information on the program so you know what loops look like and what external calls look like you know what state variables look like so it's easier to um to simplify the problem sometimes than just the structure of the theorem you try to prove afterwards is just just look simply in general and this enables you to try harder problems that have loops contract invariants and all sorts of complicated stuff and out of the tools that i mentioned before destiny checker is also verifying very smart ver very smart adopt this approach the other tools they target evm byte code of course the first and foremost

pro of this approach is that the results are basically what you deploy right you don't have to trust the compiler you don't have to trust you of course you still have to trust the tool that verified it but you just reduce a lot level of trust that you need regarding a property and it's generally easier to encode because you just have you have stack memory storage and you don't have all sorts of complicated stuff from the high level language the some of the problems here are basically the opposite of the other approach there's not a lot of structures so a state variable that just looks like x in the other one it's a number here's going to be a slot in the entire storage so it's much harder to track storage external calls functions and all this kind of stuff another thing that gets a lot

complicated a lot more complicated here is that the api encoding and decoding oh sorry abi encoding decoding code is all in the bytecode as well whereas in the solidity code you don't have that code so when you start a function you assume that the call data is going to be translated correctly into the types in the signature of the function you don't have to deal with that at all so it's a lot easier so the experiment is usage tooling example first automatically just tool example that's all see what you got and then try to power user tools to learn a bit more about the tool and i think on average i gave myself basically like an hour per tool for example

to run it automatically then learn the parameters learn how the tool works more or less and try to get something stronger out of the out of the tool um by the way all the examples that i'm showing here are in this repo as well maybe not exactly a bit changed but you can find it there also the presentation itself okay so first trying to prove functional correctness of the transfer function as i said we want to prove that so we have the person who wants to send funds and the person wants to receive funds or a contract they cannot be the same and the method center must have the amount they want to send so we compute what the sum of their balances is before

we perform the transfer we compute the balance of their sums uh the sums of the balances after and then say must be the same is that correct which one could overflow but if overflow if it overflows it just stops execution here oh yeah sorry yeah so this is your eight yeah so overflow doesn't exist um at this point at least okay so overflow and underflow reverts early said that is that correct yeah that's correct right so if we just run

tool um token.sol these are the results we get so all the tools um can either prove that it's correct or acne doesn't doesn't issue proofs but it didn't find any bugs meaning didn't give any false positives at least in the 50 000 instances it tries by default so what if we make the transfer function buggy like what is the bug here go ahead right so this one is wrong right we're basically giving more to the sender himself themselves and um this one's correct but yeah there's too many tokens here

and this should fail right so just running the tool on the example this is what we get so these four tools okay meaning they found the bug and they give you a kind of example meaning they tell you how to break the assertion and what the state is when you break it um saucy verify did break the assertion but it could not give a kind of example and various might did not break the assertion i suspect it is because i suspect very smart doesn't really check assertions by default even though it does claim to do so in the documentation that's why i tried it but i don't know because in the log it even says there were no restrictions to be verified so maybe it's a solidity zero eight thing um

i don't know um okay sounds good so the next one mm swap functional correctness we want to prove that this assertion is always true is it correct okay we can go through a little bit this might be complicated so the goal here is so someone calls a swap function they want to swap this token for this token right these two tokens must be these two here just the order doesn't matter but they must be the same as these two and that's what this requires you to do that's it then the way you compute the price

for the swap is basically always stressing this formula here you want this k equals x times y where x is the balance of the market itself in token zero and y is the balance of the market itself in token one so this cannot decrease because if it decreases with time it means that the market itself is losing money right so we first compute what the current ratio is what the current current multiplication is then we transfer to the market from the sender the source token they want to swap to the contract give to the contract which means that now the contract has more

source than before right and then now we want to compute how many destination tokens we want to give to the user or to whoever called the swap function so we take k which is the previous multiplication with both old balances divide by the new source right the new amount of source tokens that the contract has which is going to give us this is just the same multiplication this is so this is going to give us the new amount of destination tokens that the market has which must be less than before right because one increase or the other one must decrease um then we just um subtract this there's a minor minus here it's a bit um right we just

subtracted from the previous amount of tokens the contract had in destination token and this difference should be the amount we give then to the user and then we compute the same multiplication again this must not have decreased otherwise the market lost money is this assertion correct any other gases i mean only other gases know so okay so we're not gonna solve it yet so that's why the integration work so first one is supple execution and model tracking tools they could not tell us anything they did not prove the property but they also did not disprove the property meaning they just say i don't know so the next

thing we can try is fuzzers so here's hvm and here's echidna and actually both of them did break the assertion and here's how so hvm actually if i would have used a verbose mode it would also have given the full list of functions but here just gives you a simplified look at the call data needed to break the assertion and here ecna tells us that you can very easily break the assertion by first calling join then calling swap and this looks very simple okay so the assertion is actually not true but what did i have to do to actually get this so this required a little bit more work than just just the contract itself

so hvm works with ds test which you can see here and instead of verifying things in the contract itself we want to write a test that uses the other contract and then tries to verify something on top of it so here we have the same countries before but i changed the k prevent post to be state variables instead of local variables and you can see that for the first iteration both are zero right and for the second iteration this one is going to have ground so it it should be true also of course it's more expensive because now there are state variables but for the sake of proving the property it should be um equivalent and here we have a function called invariant k which is a view function that basically asserts the same property

so this is just the same as before and here just getters for the two variables so to use hevm fuzzing in this case so we have a setup function that deploys the two tokens we create an amm with the two tokens we create three users which you will find in this repo just didn't have space here but what the users do they're basically just interfaces to call the join exit and swap functions in the other contract they just um relate the calls um and then the the this contract was the owner of the two tokens it just mint a bunch of tokens to the users and then just let them do whatever and hvm fuzzing also requires or you can use this feature of the

target contracts here it's a function that returns a list of addresses which are the addresses that are going to be used as the as the interface at the front end for the fuzzing calls to be generated that's it and then we have this so invariant fuzzing in hvm it runs functions that start with the the word invariant and basically this just calls the invariant from the contract itself and then if this assert fails it's going to fail and then you get the result that i showed before to run this with the kidnap it was very very similar i used pretty much the same users the same tas amm i only didn't use the target contracts and a kidney invariant fuzzing needs

the function to start with echidna and the difference is that it doesn't um check for assertion failures in this case you need to return a bool so basically instead of starting you just return whether the invariant is true or not and that's it and that was the result that you got before okay so the contract was wrong i think my next slide actually tells how to fix it does anyone have any idea how to fix it i'm going to go back for a second do you know the answer okay so the fix requires two characters i'll show you the hint um so the

property that you actually want is sorry the property we actually want is that k post equals k but for some reason this cannot really be true all the time that's why we say it's fine if it's greater we just don't want to lose money but ideally in an ideal world this should be equal to not greater or equal yeah getting there sorry [Music] right so the join function basically you

give um yeah so you give both tokens to the market um yeah then you get like a a share of the of the market then when you access it you get tokens back based on your share of the whole pool so let's go in the right direction so the thing is you have integer division here so sometimes this division is not going to be an integer result which means you have to round the output and this is a solution with this plus one so this is how it is actually implemented at least in this

version of the contract um yeah because of rounding basically so basically what this does is if the division is integer then the property is equals so no one gains or loses more money but if the division is not integer then the rounding goes to the contract to the market and that's why k can grow but it can never decrease so now the both fuzzers say okay everything's fine um and yeah so that's how as far as we got with this example so the model tracker still could not prove anything but the forces can now give us good confidence that it is correct

let me just see how much time i've spent did i spend 20 minutes already okay i'm gonna try to speed up a little bit so trying to prove functional correctness of the deposit contract and we want to prove that this assertion is false so running all the tools just like this just with the contract as is also no tool could prove anything you get false positives you get i don't know what's happening all kind of results [Music] but we can try different things so when running actually when running hvm on this function the main problem is that in the original contract

the you can see that here there's three parameters that are dynamic bytes and hvm doesn't support symbolic dynamic types and the input of functions it wants to to reason about but here you can see that these dynamic bytes they actually must have a fixed length all three of them so pubkey must have 48 bytes with raw credentials signature must have 96. um they could be fixed types the reason why they're not is historical when converting the contract from viper to solidity and yeah i'm not gonna not gonna go in too much details we can talk after but

yeah there's a historical reason for that but effectively they could be fixed fixed byte types so that's why we change here for hvm so instead of having a byte that must be 48 in the require we can make the pub key three bytes 16 variables which is 48. withdrawal credentials was already 32 and signature was 96 so we make three bytes 32 variables and we can remove all the other requires because now the length is guaranteed by the api decoder just with this change the rest is all the same here now we can so hvm can now prove that the assertion cannot be

violated and it proves that after exploring 295 branches that assertion violations and you may ask well what about the for loop how does hvm know that the loop um like this does include all the loop iterations and it actually does because if you take a look at the contract you'll see that the loop is actually bounded by constant number and it can only run 32 iterations not more than that and hvm by default um sets to 50 the number of um times that are that uh that in the evm cfg node can be um rerun so we know that here all the loop bounds all the iterations are covered but of course this includes internal knowledge about the tool right i know

that it's 50 because martin works in the tool and he told me it's 50. so if you don't know that it's 50 then you could also use a parameter called max iterations for hvm which i did try but then it it failed it took too long um i don't remember why but there were reasons um it proves like this so we're um running the model checkers they also couldn't do much so very small couldn't do anything and with salsa verify which has a very similar approach to smt checker it just it didn't support a lot of the solidity features in this contract it has a lot of weird stuff has encode packed has hashing has a bunch of things and it just couldn't handle the language part of it which means you couldn't

prove anything um the smt checker um i got it to prove in the end but it took quite a bit of work so the first thing is you see here this line in the original contract it basically tests that size is whether a size an odd number or not right by doing a bitwise operation with one and if it's one this means that it is an odd number so the semantics of this line is just that so i can replace that line by this line so just doing mod 2 instead of bit y is 1. so the semantics gas might change a little bit but math is also cheap so um the behavior should be the same here the reason why i changed this as destiny checker or the solvers that it uses

um in the underlying logic layer they have more problems with this type of operations than with this type of operations so if this change would make the problem much easier for gender line server with the default solver that the smt checker uses which is called spacer it still couldn't prove it so recently this other solver we used something called horn base solving and this other solver actually added some support we needed to run in the theorems that the tool generates called alterica and using this solver via sausage.js smt callback which something actually exists plus setting a different abstraction option in the tool

allowed us to prove it quite quickly actually less than two seconds but you need to know that a second horn solver exists and the tool actually can use that solver via sol cjs the javascript wrapper for this lc compiler and you need to know that this solo has this abstraction option when that when turned off actually proved the deposit contract so it took a little bit of work um but it worked and here is part of the proof from the from the synthetic from the tool actually so this whole thing here is an induction variant for the loop before the assertion which should prove that the loop always terminates inside that branch but this is just this is maybe five percent of the whole

proof so this last contract i think i'm going to go very very quickly through it because it took 25 minutes already or even more so this is in your c777 token contract which i mentioned before when you make a transfer it calls this function tokens send [Music] in the sender and it calls this function tokens received in the receiver and what we want here and this is from the open zaplin official implementation from the repo minus all the registry authenticator operator stuff which is i don't think is part of the actual

um standard and there's a lot of this is a lot of stuff around it and i yeah if you try to verify that of course it's going to take much longer and i wanted this to be quicker so removed all that and this still has the the core of the ec777 token and i want those callbacks to not mess up with my total supply so yeah this must be true and i'm going to go quickly over this contract because running out of time and we're actually going to demo this contract live in the workshop so we can talk more about this contract there if anyone is interested but just very quickly do you think this assertion is true with the contract as is

the rest of this contract is the same as your c20 you can mint you can burn you can do whatever so if i call this callback here in the in the sending in the sending contract do you think this assertion is true yeah you could do anything right based on the entrance so we think the property is actually not true right in this case so salsa verify does say it's not true but it doesn't give a kind example very salt doesn't say anything so these are just running the model checkers for now and that center checker does say the property is wrong and this is actually one of the

in my opinion one of the coolest features is that it's gonna sometimes not always it's gonna synthesize the reaction call so what it's basically doing is it's saying transaction trace is you can deploy the contract you see 777 this is the current state then someone calls burn then which calls internal function underscore burn which then calls the call circuit to send callback thing that's going to call the um sending contract and this is that call this is the untrusted external call it's untrusted because we don't know who that contract is right it could be anything you could have any code and you have no idea what it's doing so what the tool now does it synthesizes calls that that contract could make back to your contract so it synthesizes

um a re-entrant call over here calling burn which then calls internal burn which then is going to change the the total supply of the contract then breaking the assertion finally and i also had to change some stuff in the contract so counter examples are actually strings are pretty hard for counter examples in smt checker so i removed like the string um the name of the contract symbol of the contract this kind of stuff um i just removed the state variables and this already made it possible to get a counter example because otherwise it would have to come up with values for those strings as well and that's what it's hard here and it doesn't really matter for for the property so we can test that so this is a quick

gs test and here i'm just running a test not really any symbolic check or any fuzzing so basically we just have a new recipe contract that when it receives tokens it then burns those those tokens basically what the the kind example taught us to do when we run this this is running with depth tools you get a full transaction trace here so i'm transferring and here where's the this is the external call tokens received this is the callback and the receiving contract which then calls burn and then the assertion breaks afterwards so we can forbid reentrancy by adding mutax to every public function

this is just one way obviously if you want to do forbid re-entrance in this case so we add a lock and then every public function must use the modifier mutex which means that basically we're forbidding reactions here right so if you're trying to transfer we're going to call the callbacks but if they try to re-enter and call mint or burn which should also have this mutex modifier then it's going to fail right right at that point right it's going to fail the reentrance to guard and the assertion should not fail if it if it's ever reached so now running the test again it still reverts but now it's reverting because of the re-entrance to check so you see that it really works much earlier so you try to do a transfer this is the callback it calls burn it

fails right away because of the mutex so now if you re-run this and t-checker on the same thing so now we finally got a proof and one of the new features coming up this is of course a feature branch it actually exports and tells you contract and variance and external call properties for reentrancy in the contract and this still looks quite verbose and quite long but basically if we simplify this formula with just very basic operations we get this property so the solver inferred for us that this property is true for any external call that this contract might make so if lock is true this thing's maybe running out of battery so if locks true it means that

the total supply after the external call that you make an untrusted code is not going to change which is basically what we wanted to prove yeah so i'm going to pass over to marching 2. talk a little bit about hbm internals okay thanks um just a little quick theory on how hvm does symbolic execution hvm does a lot of different things like we saw it in the previous examples both doing invariant fuzzing and symbolic execution and i won't really be talking about any of the fuzzing features or anything like that i'll just go over a little bit of the symbolic execution stuff

and the equivalence checking that it has which also uses the symbolic execution engine so it's basically just um well it starts as a normal evm interpreter and then it was generalized in march last year to also be able to deal with abstract arguments um so in the call data or in the call value or who the sender is and all these things not not fully abstract in that you can't have abstract code for example it doesn't deal with abstract gas but it has sufficiently many abstract argument that it becomes interesting for the types of things that you normally want to prove and as a tradeoff is also quite fast at doing those things

so the way that it works is that it's executing the evm and some of the arguments that are in the stack or in memory are going to be symbolic terms which means that we don't really evaluate the results immediately but rather we build up this abstract syntax tree that we can then send to the smt checker to or the smt solver to to consult whether this term actually is is possible to fill with some real arguments um and as we're doing this um there may be branching points and on the evm level these are all um the branching points are when you see the jump i instruction

and actually we're doing an eager algorithm here where we don't actually consult the smt solver for which path is reachable we just explore both of them and then at the end we look at all of the final states that we get and we look at the final states where our assertion might be violated because often this is like a structural property that you can see without consulting smt um to prune a lot of states early on so if we know that we're looking for an assertion violation with

the asserts and and we have a bunch of cases where we have ordinary reverts then we can just prune those from the state when no need to consult the solar at all but for the ones that do look like they might be problematic we take all of the constraints that we got from from getting to this particular branching point so all of the conditions under which we would have jumped to this particular branch and we see whether it's possible to get to this branch and to make sure that we're not getting stuck in an infinite loop somewhere in the code we have this max iterations which eternally keeps track of every time you encounter a particular jump i instruction okay um so that's how it works it's an

eager algorithm and also this max iteration stuff this can also explain what what leo was talking about when um we were looking at the deposit contract and we get different behavior when we change max iterations because here um max iteration sort of stops this eager algorithm in its tracks because we need to make sure that we're not getting into this infinite loop and so then uh once we reach max iterations we want to make sure okay what's this pass path actually reachable and then we do a consultation with the smt solver and often this can be the bottleneck for the entire execution so

sometimes we run into a timeout here and then you know the whole thing will not be as easy to verify okay and since we are interested in performing this symbolic execution in a variety of different contexts like we want to do it in ds tests where we have a very specific setup we deploy all of the contracts that we're interested in or maybe we're using mainnet states or we're just like performing the symbolic execution on an arbitrary run of the contract we want to assume that it's in any arbitrary state we have a couple of different options

when it comes to how we deal with storage when we're doing symbolic execution and we have three options so the first one is concrete so this one actually fails if you try to do something symbolic with storage if you try to read from a symbolic location or if you try to write to a symbolic location um because this one wants to be compatible with with our pc if you want to run symbolic execution against the mainnet contract for example um then obviously you can't be asking for the main net value of an abstract location because no client will be able to

to tell you what is that storage location x where x is a unknown number um but if you say i want the storage location i want the value at four they can give you that so when you're using concrete you can use symbolic execution against main at states and the other two are both symbolic versions but they make a different assumption on which particular state you're in in that in the first one which i call initial s we're not assuming we're we're assuming that everything that we haven't spoken about in storage is zero the way it would be by default

we can still read and write from abstract locations and we keep track of where we have uh read from and written to in this in this abstract uh storage mapping um but yeah if we try to read from a location that we haven't written to before we always get zero so this is like um yeah it's it's basically performing um what you would get if there was no previous state besides what you've done in the setup function and your whole sort of dance that you do before you actually run the execution whereas the third one and the most general one you're not assuming uh you're not putting any additional constraints on

the state of the contract you're saying this contract can be in an arbitrary state and whenever i read from any storage location i can get any possible value back and this is actually a bit of an over approximation because you may have certain constraints enforced by the code of your contract like you can't for example write to the storage location 13 ever so if we were to have uh analyze the contact completely then we will know that this is zero but if we're just looking at one particular invocation of a function then we won't know that so if we're reading from storage location 13 or x or whatever we're just getting an abstract value back and we're not putting any additional constraints on that

so when we're doing ds test we're actually doing initial s because you're assumed to do all of the things that you want to do in your setup function but when we're doing some other things like the equivalence thing that i'll be explaining to you what it is in the next slide we're using this symbolic um so the fully unconstrained storage okay so quickly about the equivalence checking that we can do with um with hvm so as i mentioned when i describe the general algorithm of the symbolic execution that hvm performs it's going down all of

these it's going down the entire execution tree and looking at all of the leafs right so we can do that in two vms at the same time so we uh we copy the entire vm states and we change only the contract code so now we can explore um two vms that differ only in the code of the current contract that we're executing and we explore both paths of both contracts or all of the plans in both contracts and we look at all of the pairs of end states that we have and then we compare every possible combination of these pairs and see if

the constraint sets of each path are simultaneously satisfiable and if so if their results differ because this means that there is an input such that if you run it with a one uh piece of code you'll get one result and if you run it with the other piece of code you get another result that means that the contracts are actually different and in fact this is the only way something can be different is you run it with the same input and you get different outputs and so if there is no such pair then

these contracts must be equivalent so that's how the equivalence trigger work and i think that's all i'm going to be saying about the theory of symbolic execution in hvm right now and now i gotta run to the other room and prep the workshop but all right thanks um um just like across the hallway same floor here yeah so we're obviously over time i'm just going to skip to the very last one i was not that optimistic um so just a few quick conclusions on actually the experimental part that i should maybe have for the slide before so some of the automatic fvu tools can be really powerful even given which

approach you're taking very fine solidity or even by code or doing small execution or model tracking or this kind of stuff but there is no tool that's going to do the job at every single time so i would encourage everyone to actually use all of them and every each one of them is going to do something differently and you might actually get a complete result if you use each one of them separately also a conclusion of this experiment is that fv still have very much very much an expert domain and some very specific tool knowledge was required to verify um to extract the full potential of the tools and even verify this simplified versions of the contract so you can only imagine what you need to do to verify the full version of the contract so for example we needed to

note that hevm this fifth iterations max needed to use a different horn solver different abstraction options so it was still quite in-depth knowledge required to verify these contracts and of course playing of the tool knowing the the specifics of the tool knowing the parameters and what things do differently is essential to get any good results out of the tools so i don't think we have time for questions but we're running over to the workshop thank you very much thanks very much