{"id":"SWtAwPPBGoI","title":"Whiteboard Series with NEAR | Ep: 39 Rikard Hjort from Runtime Verification","description":"Runtime Verification (@rv_inc), Formal Verification Engineer Rikard Hjort (  / @rikardhjort  ) and NEAR Developers Dr Maksym Zavershynskyi and Nikolay Igotti (  / @nearprotocol  ) discuss Runtime Verifcation. \n\n------ About Whiteboard Series --------\n\nThe Whiteboard Series with NEAR is a set of video interviews with Founders who are building scalable solutions for Blockchain.  We deep dive into their story, what they're developing and how it is helping the ecosystem. \n\nFollow the latest from NEAR Protocol on, \n\nWebsite: https://near.org/\nDiscord: https://near.chat\nTwitter:   / nearprotocol  \nGitHub: https://near.ai/github\n\n#WhiteboardSeries #Blockchain #FutureIsNEAR","channel_name":"NEAR Protocol","published_at":"2020-07-31T00:00:00.000Z","thumbnail_url":"https://img.youtube.com/vi/SWtAwPPBGoI/hqdefault.jpg","transcript_text":"all right uh rickard thanks for joining us and uh do you want to introduce yourself um yeah i'm ricardo i am a former verification engineer with runtime verification and blockchain nerd and day-to-day i work on on k awesome which is our implementation of webassembly so that's so when you say when you say your implementation of assembly you who uh so runtime verification or the the k framework uh implementation of webassembly so basically it's a formal formal and executable specification of web assembly uh written in what would look like a high functional language to many programmers i think i see but it has some nice special properties i'm sure we'll get around to talking more about it cool and nikolai what do you do yes uh i work near uh helping with uh with what we call the contract runtime which is which is essentially the way how we execute uh contracts smart contracts which which are technically web assembly programs inside of our blockchain and how we integrate it with what you call transactional which is essentially uh the part responsible for the functioning of uh of the blockchain as a distributed database this consequences so i'm working also with nikolai my name is max on the runtime which as he said includes the execution of the contracts also trying to figure out all possible safety aspects of our runtime because safety is incredibly important for the blockchain you kind of can live without liveness if you if your node stalls or crashes it's okay you can just restart it have some social consensus about things you know when to restart the notes or whatever get a new binary version but if your safety is broken it can be fatal for the blockchain therefore it's mine and nikolai's huge focus in our contract runtime and transaction runtime on how do we make sure the contracts execute deterministically and execute correctly that's what we're going to be discussing today so i'm going to let you guys kick it off actually oh i think it would be very nice before we start discussing like particular technologies such as webassembly or formal verification of runtime verification the company uh to discuss a little bit uh background ideas like mathematics behind that uh the reasoning behind behind the formal verification so regard what would you like to share um well in essence i think um a good way to describe it is that formal verification is a process which takes right a bit it takes a program you take a program p and a specification s are you writing somewhere yeah can you see it in the whiteboard oh now i can wait wait a second great you put it through this typical program refreshing magic box and out comes either a proof that the specification holds or a counter example and in in in theory that that's that's what you want but in practice there's also this uh slight possibility that we often don't talk about that you can report uh i don't know like the we could neither find a counter example or a proof but but in principle you you formulate something you want to hold of your program for example you know the if it's a token contract it could be uh the number of tokens are is constant or no one can have negative balance uh and then you give the the program the contract as input and you ask a system to uh prove that this is true or come up with a counter example and you often end up in this kind of don't don't know face so this this box here often requires some manual manual intervention uh and that's what formal verification engineers spend a lot of a lot of their time on and what is the language for expressing b and deaths respectively so how i think for b it's mostly like predefined and depends on the on the area where you essentially perform the phone verification but how do you formulate s well i mean there are many ways to formulate p as well i mean you can't say well it's just a program but the thing the thing that is say i'm going to say it's implicit in all of this is that there is this semantics that are goes into the box and that's one way to express what a program is so essentially it's like you define you define the world of all programs in a language that could be rust or webassembly or what have you and then your program is just a specific a specific element in this world of languages but to do formal verification you need to express this language l in a mathematical fashion and that's for example the the web assembly implementation i'm working on is basically a way of turning the webassembly written admittedly mathematical um specification into uh another mathematical specification that we can run uh with our system so the way you express s depends on how you have expressed the language l or rather like how you express this world around here um so you usually don't just give the program as source text into this system or you you can but the first thing that is bound to happen is that the program is turned into this mathematical object and for example we use something called matching logic so you write your specifications in matching logic uh if it's a if you're using a tool like isabel hall you will have a you'll have an isabelle hall model of of the language and you can express things in regular higher order logic or it could be first order logic it's it's it depends on the tool and the best way to come up with or finding a good balance between powerful specification languages where you can express a lot of things and but you don't want to be able to express too much because if you have a too powerful specification language then you uh verification can become harder so there's a balance to be found there and there's also obviously a user experience aspect to it uh where you know you want to find a way to express specification that makes sense to developers a very easy way could be to have assertions in your code and then just have the tool transform those or transform the specification into or write a specification for you that basically says we're never going to revert because of an assertion but you might want to express temporal properties as well like say like well if if you ever touched this variable during the run of the program you are not allowed to touch this later and that can be harder to express but doesn't it actually mean that in a good case or for for modification p and s better be the same uh because uh it like programmer uh shall express his her desire in a program and a part of the those like desires and tensions uh logic you also express the invariance so for example a search as i mentioned is is a very simple form of the formal runtime verification so why do we want to go beyond asserts um well first of all like i personally agree with you like and a big part of uh making formal verification more widespread is to make sure that it's has good ergonomics for developers and you know systems where you can use asserts or do um or do uh like write annotations for like pre and post conditions for example that usually makes more sense for the developer the problem is that if you want to do source level verification or like you know if if you just want to have the developer as the writing code also you know write specifications that's often a good thing but there's not necessarily a big chance that the automatic formal verification engine is going to be able to prove that and if you're a former verification engineer you usually know your tool the the engine you're working well with pretty well and some ways the formulating specifications are more amenable to verification and you might want to like take this high level specification and break it up into many different smaller uh smaller sub goals that you want to prove for example and then then you need to have a language to express it in i mean it's the same thing if you write if the first thing that happens to the program is that you it will be expressed in this um mathematical specification of the language if the specification is also part of the source code then the same thing happens with the specification the specifications derived from the source code but the first thing that gets put into the actual formal verification tool is going to be this it's going to be written in you know some specification language that is usually more powerful um and you want i mean if you're doing formal verification you probably want to be able to you know write your own specifications that you don't have to go through the source code to implement but actually if we talk about languages uh i think uh usually there are like formal languages in like in in the form of formal grammar standing behind the language and that's kind of one layer of languages but actually uh with languages there is associated around time semantics and certain behavior behavioral characteristics and the question is which part of the language is actually to be addressed by the formal verification is it is it on time behavior is it like a certain uh syntactical properties of the language well i can't really think of anything that would be all that interesting to uh verify uh just using syntax i mean usually most languages try to have a very like straightforward uh and not too complex and undecidable um grammar like if you want to write a parser you'll write an lr1 parser like you know that's parsing techniques um but then to give meaning to your language uh that's sort of where the magic happens so so to speak uh and that's also you know where languages become more equivalent any touring complete language is essentially you know are essentially the same to some extent and the way you define what each construct in the language does i'd say that's the that's the more interesting part i mean i'm thinking whether there's something that could be very interesting to verify as like what a programmer usually thinks of the pure syntax but i mean if it's rejected by the parser then you're probably going to have a parse error and resolve that and that's i mean the parser is a verifier it verifies that your what you're giving it is something that is expressible in the language syntactically and the type the type checker is a verifier it verifies that uh you are not doing anything that's considered illegal by the languages type system yeah yeah okay so like on a different level layers or levels of of the language uh there are different rules like on the lowest level uh there are like pretty much syntactic rules of of the of the formal language on the on the level of the type system there are different uh different computation essentially expressed in a type system and i think a significant part of of the language research like during last 50 years was put into into essentially making a type system such that uh most of the semantics are are actually caught on on the level of of the type system and and so my question about like like the formal verification as a technique is is essentially how it augments uh the research because like every everybody knows how to write parsers many people know how to do like a type system and how to how to perform uh like uh like that type checkers on on lattices and so on but uh i think uh not so many people at least not myself are aware how to go on on the next semantic layer which which is which is higher than a type system so how to express uh formal statements in that area which builds like a complete exchange system which which could be actually used for uh as as input for any like reasoning machine which which any formal verifier is and so that's that's pretty much my question just so i understand you correctly you're you're trying to like figure out what what's what's what's the gap between you know the the type level kind of verification that a programmer is expected to do and what the things that we usually call formal verification where you know you hire a formal verification engineer to prove properties of your program i mean really yes pretty much it's like it looks more like uh the for example type verification is absolutely like mathematical procedure it's an algorithm you once you have a described system uh for the language and it's usually in some form it's formalized as a part of the language uh you can verify that the types type attribution is correct in a particular program and that's mechanical process and you don't need any additional uh operation and it's not important in the program uh like on the same language if if it's like a word processor or web server the type syst the type system manipulation will be exactly the same and because because it's compiler and which does the verification and so my question is um imagine uh if you have a form of verification or what is the formal system against which verification happens so like how how uh how it could be built how it is built in in your tool or not in other tools um well so in in our tool um it's built through something called matching logic which looks fairly similar to most logics that people may have encountered but it's slightly more slightly more expressive um but say for example in isabella hall you are using a slightly more familiar probably higher order uh logic to express the um the meaning of of of programs and i mean it's not really the type system and like these kind of formal verification uh things we generally do are not really in uh competition because the idea with the type system is usually that it's supposed to be uh fully decidable like i mean it should be pretty straightforward for your type checker to just say this well typed or it's not well typed uh and might be unification like oh you're doing addition and you know it's going to see that you know one uh actually this is a good whiteboard moment like if you have if you're doing one plus one somewhere in your program or rather if you're doing like p plus q and the type checker can infer that this is an int and this is an int then you know this expression is it's well typed but that for that the um the type checker must be able to infer the type of every every expression the program uh which puts a limit on the type system's expressiveness if you want to have a type system that can express any anything then you move into undecidable territory now type checking becomes undecidable and i mean this this limitation here that you will sometimes end up in don't know that's just like a sort of mathematical threshold you cross at some point things are no longer decidable decidability means there is an algorithm that can decide this and will always be successful regular type checking is something like haskell or rust or java is decidable because the type checker will always succeed to tell you whether your program is well typed or not but if you want to have a slightly more expressive logic system uh things become undecidable so a question you're saying it's undecidable when it's theoretically undecidable not something that your tool cannot uh infer because of there's some computational limitations well i mean i mean obviously there can be computational limitations like i mean there is there is definitely a uh i mean in practice for example i think in isabel there's a tactic that i think is called blast which is technically uh you know it can take certain i think linear formulas let's call and do and check if they are uh true and it's like a com uh sorry i lost the word it's not is it you don't say that it's complete well you know it's it should always succeed in theory but in practice there's obviously a timeout limit some some somewhere the children give up but there is also um i mean the halting problem and so forth exactly the halting problem is like the example that you know like if if i give you the simplest if i make the simplest turing complete language or if i give you lambda calculus and say well you know will this program ever terminate for a great deal of programs that's pretty straightforward uh but there are there are going to be some programs where it's not straightforward so for example i mean people often confuse this and think that oh you know the halting problem is undecidable therefore they can't be you know it's meaningless to try but honestly in many cases i mean if you if you're writing a smart contract and your contract just looks like this it's just like straight line code then i can tell you well you know if and this contains no calls and no jumps then i can tell you you know this is going to terminate but if you have a jump in here or you have a little while loop all of a sudden uh then it becomes more complex maybe i won't be able to decide whether this terminates or not but for and the way many tools work is that they make sure that you uh when you write like certain functions for example in isabel you also have to provide a termination proof but if you if you just define your functions and start using certain simple structures then the program can automatically tell you sure this is going to terminate and if you want to do something more complex then it's your job to also provide a proof so the loops also include like loops in let's say standard arithmetic operations mathematical operations like let's say hash computation right or or like signature computation i mean like if if we use it somewhere in our code then we might end up in this done don't know state um what was your example well i mean let's say we have like a very simple example that our our program verifies certain uh hash or like certain signature right and like we want to prove that the assertion that says the hash doesn't match never never fires in the program and so we cannot really prove it for for the input because you need to literally pre-image the hash which right and but but like hash but this is like an example of like a very simple program where you just have a hash computation and you just cannot prove that the program will not panic because the hash has been like one way function has been is being used somewhere in the code but those one way functions are like incredibly popular in in smart contracts even like basic like asset manipulation like defy contracts so wondering whether if someone drops in this kind of like crypto function will it automatically you know uh make it unusable that they formulification usable oh oh no and i mean for example you i think you can scroll down a bit maxim i'm just yep let me scroll down below uh there you go that's my terrible like what you do in general let's see where you are okay uh what we tend to do is like we if if we have um i mean often you're doing something called symbolic symbolic execution which means that instead of like put inputting specific values into your program you are inputting um let's see there we go uh you're inputting like a variable x right and so say your your input to a program is x and then at some points you get to a place where you do hash x oops since x is unknown we probably won't be able to call this function so what we'll do is we'll just leave the symbolic variable hash x here and now we know certain things about this value x for example it's between 0 and 2 to the power 256 minus 1 or something right and we also know that if you do if you also have y and you do hash oops i mean the because you you're just defining it as a function and if you say well let's do hash y then we have the same situation but now i if you ask me to prove can you prove that uh hash oops sorry it's a bit of a lag on my end so this becomes pretty ugly uh if you ask me to prove given that x equals y that hash of x and hash of y are the same i can do that because that's a work that's i i just have that as some assumption of my specific hash function i i write like a lemma saying that you know this hash is correct and that's usually what you do you you're i think it's tony that said something like uh the job of formal methods is to elucidate the assumptions upon which formal correctness depends that's a fancy way of saying well the way you're doing formal verification is you're trying to figure out that something is correct given certain assumptions so for example if you if i'm verifying a smart contract i will often assume things about cryptography because i'm not really proving things about cryptography and proving things about the program and i will say this program is correct given that the cryptographic primitives are correct like you know if i do encrypts x with a key that's a key and then i do decrypt with the same key i have a lemma saying or like i have an assumption essentially saying well you know that's going to be the same thing as x if i encrypt it and then decrypt it and i use the same key that's going to work i will also have or i might have a lemma saying the opposite but you know i mean i guess there's usually a chance that there is some probability that the problem with crypto with cryptography is that it's very probabilistic so for example if i'm computing if i'm storing two values let's say x and y are not equal and you ask me is hx equals to hy the answer is maybe unfortunately we could just add as a an assumption saying that oh you know if x and y aren't equal their hashes are not going to be the same basically there are no pre-images that's not true but you can say that you know given that you're not getting a house collision your program is correct and then you can decide and then you can employ your reasoning about that to say if that's good enough for you if if your data is longer than uh 256 bits then for 256 bit hashtags you are guaranteed to have at least one collision that's uh like uh that's obvious so yes i mean so the the point is and and that's why i come back to this this horror quote is that what you're doing is you're usually not saying you know this program will always work in every circumstance because you know there are physical there's a physical world out there and things can go wrong and you know no it's just going to work correctly given that every node fails in the same way at the same time maybe not but you can if you just have encode that as an assumption that you know your virtual machine is deterministic or you encode as an assumption that you will never have a hash collision then you can prove certain things but that also means your proof doesn't work unless you state that as an assumption and that's valuable right um and you can remove that assumption and say oh no our contract works even if there are hash collisions uh but either either way you can i mean you're not you wouldn't you probably wouldn't state that you know there are no such thing as hash collisions because that's i mean that's patently wrong you could use like you said the pigeonhole principle to prove that wrong and now your whole system is unsound but you could add an assumption saying well for these particular values x and y they do not collide and then you can prove that you know you're you're no one no one is able to steal your tokens given that they can't produce a pre-image for example um and actually like i really like our discussion however it gets very uh very theoretical and probably uh close to like mathematical problems or even like foundation of computations let's say so so if we i have i hate to be kind of a moderating person here but but i guess to make it more like closer to the theme which we which we aim to discuss uh we probably can discuss more like a practical aspect so so imagine that in our case p is like a rust smart contract uh could you give an example what would be an s in your uh verification example and how uh how does it bring the value to uh to the like a normal developer who's not mathematician not a formal logician but like like a smart person writing smart contracts um sure i mean if so if you're writing a program in rust and um i mean the my standard example is it's a token contract and i mean history has proven that history like the last 10 years have proven that even something as on the surface simple as a token contract can have all kinds of really bad bugs in them a program that looks super simple can you know accidentally mint tokens um and so i mean that that's that's an s that i usually take as an example that uh the in a token transfer the the outgoing sum of every um of every address touched or the outgoing balance of every program touch is equal to the sum of all the in-going balances so if uh a on the inputs plus b on the input plus you know forever is equal to if if these are all the the addresses that are sent as input to the transfer function uh and you know these can be very complex you know it can be like oh it's delegating to someone somewhere and it's you know giving something to the um to the contract owner address and whatever but i can say that you know the in-going um the in-going transfer or the balances has to be the same as the outgoing balances and i mean this fails for all kinds of reason i mean you could say you might or you know the transfer might fail an excellent example of course is overflow i mean if one of these if one of the addresses overflow during the transfer then this doesn't hold um and so you might say that okay this is going to hold assuming that all the uh none of the addresses there's no overflow in here and you have to express that as a property like assuming that you know the changes in balances don't cause overflow uh this works this is once one property you want to hold but another property you want to hold for example is that all the all the balances uh oh sorry all the out balances should be uh oh wait sorry actually let me do this by text that's easier so a i a i uh b i etc uh the outgoing balances are larger than zero or so that the ingoing balance are a lot larger than zero that's going to imply that all the outgoing balances are larger equals zero for example and that's another property you might want to prove um and from from this you might want to prove that you know the um the the total amount of tokens in the contract is always the same this might not be something you want maybe this contract is supposed to do minting um but i mean from this perf you might be able to extract quite easily the property like okay if you do a transfer the transfer doesn't affect the number of tokens in the contract um and i think one way this can help a developer and we often have this conversation it's like how can we make formal verification easier one way to make format verification easier is to make sure you're always very explicit about your assumptions and you try to like at least give enough information in your comments or your specification documents or by the way you name things or whatever that or by assertions uh that uh it make it look very clear that these kind of things can never be be violated but i mean if you just write a straightforward transfer function there are many ways that can go wrong but if you write this down this kind of specification and then try to just look at your code you're going to there's probably going to be places in there where where this is violated and then you need to start thinking okay am i sure that this is going to go back to uh a proper state like there might be there's going to be somewhere where the value of ace balance has been decremented without the value of these balance have been having been incremented and so on so i think like until we get i mean our tools are improving rapidly we're in like a formal methods renaissance but for the programmer on the ground right now i think starting to familiars become a bit familiar with formal verification and maybe with like property-based testing is an excellent way to make use of this right now because if you just start writing down your assumptions and your invariance then you're probably going to catch yourself making certain mistakes or or end up i mean if you if you write down an invariant that's saying like for example say you never want your contract balance to you want it to be constant and you just look over your contract and you're trying to like make sure that that holds if there's one function where you're kind of scratching your head and saying oh i'm not sure but yes i think i put it i think i thought it through once and it should work then maybe you can rewrite that function to make it clearer and convince yourself and others that um that it's correct so i i think the formal methods thinking and approach is valuable to everyone and i mean especially in the defy world yeah yeah i just i just wanted to say that it's like it's what you described sounds like a very good hinging which most good programmers i i'm aware of pretty much follow even without without much of the for training in you know formal verification so like i know that good programmers writing complex systems always write a source so like like checking your invariants frequently as possible is is very common and very good habit that's uh that's i'm fully agree but this kind of uh gets back to the previous question which i had so don't you really believe that uh the best practical form of verification is where at least languages for p and s coincide all mover even where uh the pia and that's itself inside so where uh the formal verification must be a part of the program yeah i would even add to that because i was going to ask in the same kind of lines the question that you know when engineers design a program and have invariance in mind they they enforce them through asserts for the assertions right and the the way they basically the assertions that express the invariance is the is the s for the engineers like that's what i think nikola is going with is that you have a program right you wrote a program and then you go over and you try to make sure that the invariants hold and your ass is actually a set of assertions that you put in the in the strategic spots in your program and since they have to do it like anyway like good engineers right they have to they need to be aware of the invariants and have to add the asserts everywhere um where does the value of the formalification comes in since we enforce the invariance through the asserts like why do we need why do we need to prove them additionally on top of that um i mean that depends i mean i guess there are two kinds of asserts one one kind of assert is like you know sanity checking that everything works and if it doesn't abort like you know checking well is someone trying to transfer money to themselves then you know we you can abort for example or that kind of thing but another way we could use a search that isn't that isn't really meant to be functional is writing down these research that should never be violated and you believe that there is no way they can be violated uh those are the kind of research you probably want to remove at compile time it depends but i mean those could cause your contract to to um dost like you know well if if you have an assert that you think can never be violated and all of a sudden you know and you know that's say in the transfer function um and somehow you're wrong and that ends up being violated uh and there's no and the only way to modify it is by you know calling transfer then you know you're never going to be able to transfer anything with your token contract again and now your token is like worthless probably yeah um so i i say there are two kinds of research like people will often like you know write a cert like sanity checking your input like you call this thing correctly and you're not going to break anything if that's wrong we're just going to if this is his theory we're going to eat your gas or you know it's it's your problem um and but that's that's input validation and that's that's saying and that's exactly like you're saying every like or most good engineers when they're not under the very like some certain very tight deadline or something they should have those in place um but they're also the the system invariants and i think i mean my i i haven't been over all all the all the contracts all the different platforms but i think those are usually less not present as much and those are really the kind of things you want like you want to be able to say that your system will always be in this consistent state your your deposit contract is never going to lock up you're never going to lose these funds or so on and those aren't really like input checking a search those are a search of your system and like and if those are violated if it's your system is probably designed around those always holding and if those are suddenly violated are you sure that you know you have the correct fallbacks for that um and i mean and i mean if that's all you take with you like oh i'm gonna i'm gonna if you want to say i'm gonna show those those uh former verification engineers that i don't need them and i'm gonna write a search and i'm gonna say well if this invariant is ever violated we're gonna call the fallback function and all our things are going to be liquidated and everyone's going to be reimbursed then great like you've added some great some great um panic handling basically but you did that by trying to like think what are the variants i expect to always hold where can they be violated am i sure that i can handle them correctly because that's the kind of thing a verification engineer would find like you know you assume that this would always hold well it won't hold in this case you say okay but if in that case i'm going to deal with it like this and that's great now we have better software um yeah and and actually in this regard i have like related questions because uh one of the like uh i'm a practical engineer in the sense that i uh i did look for various like complex systems and uh it showed that there are like two very powerful practical techniques for verification one is the sword which i mentioned and and other is some form of a virtual machine because because you can put some invariant checking actually into into your execution uh engine for example things like a for jvm there is a form of formal verification of of stack manipulat manipulation correctness for example so so that like it's a stack machine so when you when you put values on on stack and from stack you essentially ensure that stack is balanced and properly typed and uh similar thing exists in in many other virtual machines so um so some some invariants could be checked and insured by uh by the virtual machine so uh so what uh what do you think of formal verification could bring to the virtual machine for example if we have like wasn't virtual machine do you think there could be something uh which we could add to this virtual machine to execute smart contracts in a safer way um i mean what you're talking about i mean if i understand it correctly this sounds like runtime monitoring like checking that you know uh certain things like checking at runtime that things always work and maybe like executing this exercising the system and running a lot of things and making sure that things always work is is that correct it's not exactly continuous no no for example if you look at the john virtual machine uh it has a bytecode verification but verification is essentially uh before executing the the code the bytecode you check that the the manipulations with stack uh are correct correctly like balanced and so on and uh uh and and so uh there are other chats like uh memory manager in this in a sense is is something which helps perform modification because it ensures that objects for which the reference being held are not actually disposed which could happen in language like a c or c plus plot uh and i mean so this web assembly has four more things yes yeah and i mean and i mean those are kind those are properties that are super good to verify and are actually also kind of relatively easy to verify again they're decidable you can say that these uh you can just look at a a sequence of um jvm um uh jvm bytes and say okay these are not going to violate you know yeah cause stack underflow for example and that's because it's a decilable property and it's also you know it's well known that that's something you can do if you just design your language correctly uh but some things are not decidable and especially like if you're if you're an engineer writing writing contracts it's very hard to design a general process that is going to check some meaningful property of every proper possible program you can you can construct i mean essentially like formal verification is you know applying applying all these formal methods to things that are not easy or rather i mean the thing you're describing is also sort of formal verification but it's the kind we take for granted it's the same way we take um type checking for granted it's something we know how to do there's nothing we can do well it's something most people will be familiar with and therefore we do it obviously um there is no real such process for uh checking these kind of specifications of a token contract if there were we would just apply them and every every uh program on the evm or the near virtual machine would you know be guaranteed to satisfy these properties but since we don't have that we need to do whatever we can and that's usually takes some human ingenuity and in 30 years in 30 years we're going to have a lot of cool new decision procedures to automatically verify a bunch of things that we think are important for smart contracts but right now you know no one's thought of them yet so what you're describing are a bunch of properties that are very important to verify but there are other properties that are important to verify that are not as easy it's not like the the in in algorithms like i mean there's a bunch of algorithms there's there's p and mp like there's a bunch of things that are easy to do uh and there's a bunch of things that are not easy to do but the things that are not easy to do might still be important therefore we're applying our ingenuity to try to solve the best as we can even though we know that there are some or okay we don't know but even though we assume we think that there are some basic limitations to how how well we can do it we still want to do it so even though we don't we know that there is no decision procedure for whether a program halts we want to be as good as possible in detecting halting and we want to be as good as an automatic as possible in detecting important properties of smart contracts and when they're violated and when they're satisfied and that's sort of where the research is happening yeah yeah that's that's absolutely correct i just uh just wanted to like uh understand the practical uh consequences of uh formal verification for uh for engineers so what would be uh the best practices i guess we we can understand one of the best processes which which is uh asserting uh other probably would be uh adding more checks uh into into vm but uh um that's as as you said it's it's on the lower level so it's it's less on the semantic layer and more on like on just execution engine layer and and so if we talk about uh like semantic related or formal gratification so what would you recommend people to do here essentially how to other than think about the before the program which is probably very valuable suggestion but still um it's hard to do in general it's sort of like saying you know what are the principles you should adhere to to make good software i mean it depends on what software you're building if you're building a website or you're building a a nuclear missile launch system you have different practices um and there are some things that are you know obviously always good like you know document your stuff and think through things um and i think it comes down to being clever like i mean that's you know keep it simple stupid principle like i mean if you want to do something really really clever uh something that optimizes something in a really smart way but it's that is not obvious you need to convince yourself and ideally convince someone else that this holds so i mean code review is a great example i mean if you if you make sure you do good code and honest code review like people actually don't just you know let your stuff go through like people actually say i'm not sure this works can you show me and convince me 100 that it works if you can convince them and you just like write that down in a comment or in a document somewhere uh then you know you're i mean you're essentially doing formal verification on paper if you if you can write i mean mathematics is essentially writing convincing enough stuff um but also you know try to convince i i think we often stop in this place where okay it's probably true and i can't i can't think of any way this would not work um whereas of course verification deals with the problem of like am i 100 sure this can never be violated um so but i mean and then i mean i also think one shouldn't be too hung up on formal verification as like you know the holy grail either i mean there are all kinds of things that are in between i mean in essence you have like uh let me let me grab the whiteboard again uh you're gonna have this uh let's do an arrow oh it's very laggy sorry let's see uh that's a bad arrow like more and more better verification uh and i mean if you do testing if you write unit tests and integration tests and everything great you've you've taken a step in the right direction right um and if you do um like runtime monitoring or like you know you know you're always checking at runtime that things are working properly uh that's a step in the right direction and there there's all these things that happen on this scale and i'd say where the more formal verification stuff starts is things like uh bounded symbolic model checking and say um symbolic execution like uh you you find a symbolic execution engine and run your program on different inputs and try to verify things or use you know state-of-the-art tools there's every step to the right is probably an improvement but i think we tend to get stuck in testing and then this fluffy thing which is you know just oh hang on this is not going well uh here we go this fluffy thing which is hard to place on the scale which is auditing right that's someone looking at things and saying oh this probably works and this falls best practice um i mean one thing we're working on is trying to make a tool called firefly which focuses very much on um using the existing test suite like your your existing program test suite and our formal methods to find make sure that you know you've exercised every branch in your on the bytecode level and we can also use those that testing to do symbolic execution and check for properties getting violated and you can write like invariants of your system like saying your my system should never violate this property and then we can have that invariant and we're going to keep it with us as we are running your test suite and we're going to make sure that that always holds so essentially your tests we did not is not only testing the things that is that it's supposed to test in a sense it's also uh making sure at all times that all your systems variants are not violated and i think it's important to not not get stuck in like full formal verification because full form modification is valuable but it's also harder than these other techniques and it's therefore right now it's sort of reserved for the most important things the things that can absolutely never go wrong uh like you know the beacon chain contract on ethereum like making sure that you know that is going to work and making sure that whole certain properties hold of it uh that's a good place to employ for more verification if you have the the tools and the means but it's not going to work for everyone at all times yeah could it give like an example how um because this sounds uh like a super cool idea to uh to what you just described to uh to actually take tests and like uh essentially uh do like factorize it in a sense so instead instead of of actual uh values used in tests just use equivalence classes of of the text which which leads to like the same or different uh program behavior uh could you please explain how how it uh how it works in in the file so i i'm not sure i understand the question you're saying how the how you can automatically generate tests or how um now how how could you like translate test from the actual execution to symbolic execution i think if i understand what you described here you you essentially use use a test as an input to symbolic execution uh engine so that you kind of understand what's what's going on yeah okay yeah so i i don't i don't work on firefly so i don't pretend to be an expert on this but the way i understand it is that what you do is you have uh we just have a specific contract uh and if you are calling that within firefly we're going to catch that and give you a symbolic value back or initially we're going to give you a random value back just so you can do some random testing but then we might also give you a symbolic value back but if you run the same test in say ganache then uh it's just going to give you a specific number at all times or maybe a random number so the way the way the way i think firefly does is is like you ask for a random value from a specific point and if firefly sees you doing that that it's gonna uh turn that into symbolic value if i understand correctly um so essentially like you're you have to write your tests and or like you write your tests as a property-based test like a randomized test uh and then i don't think this f uh feature is fully implemented but in the future uh we're gonna turn that into a symbolic or we can turn in a symbolic value for example but i mean so i mean it's it's it's all just standard like you know programming tricks using hooks and you know checking work which environment you're in and um so i mean formal verification is just it's very similar to programming i've i i identify myself as like a software engineer day-to-day because like it doesn't feel that different it's just working on a slightly different domain it's like i'm building the tools to help specific development work um and it's and i'm just doing it in a specific special language that has some neat features um so i mean i i don't i i think it's important i know that formal verification doesn't get stuck in an ivory tower of like you know i i know i talk in very abstract terms sometimes because i want to make sure i don't i i stay correct and don't say things that are like probably wrong but uh i think i mean a problem with formal verification sometimes is that it can be a bit too abstract and i think what we're doing what i like to do is just you know show the tools i'm working on and say like hey here's what this can do and it it looks like you're doing functional programming which is probably not that scary and it's something you probably should do like just kind of putting it in the hands of people and making sure like i said that people start thinking about uh oh i wanna i wanna prove something and then you start by saying oh what is you wanna prove right because people often come and say oh can you prove i just to prove that my contract is correct and then you asked have to ask well what does that mean what does it mean for your contract to be correct and like well half the time people don't really have like oh but you know i know what it's supposed to do well you know then it's doing what it's supposed to right i mean unless you have something written down that you can check it against um you can't really do verification and unless you have that it's quite possible that you haven't fully thought through what your system is doing and it's also even more possible that it's going to be hard for you to explain it to someone else so i have like um and this is a question here yes sorry nicole and that's also about the practical aspect so we talked about the financial contracts here right and uh you might have heard that many financial contracts were broken or abused not because um you know there was some bug in the code but because people were able to find a way to combine them somehow together or to do some manipulations on them in such a way that they at the end they come out profitable like or oracle manipulation and like with like flat phones for example yeah like flash flash loans like yeah whatever just like you know like some temporal manipulation like you can you can like you know like jack up the price then then you know the dump it and all those kind of things right and call out some other contract and yeah manipulate the price ask you yeah and your thing like even without going you know like in those areas where we talk about the cross-contract you know interaction everything how would you go on with trying to prove that your contract cannot be financially manipulated in like in temporal way in such way that someone can somehow come out profitable at the end by just doing some a bunch of like atomic operations on your contract um well i mean always start with the simplest way of doing things and i mean the simplest way of doing things would probably not be you know to do full formal verification on all the code and all the contracts it would probably be probably be something like uh set up a model like just a little graph of the different contracts how they interact and um like and and again like you have to come up with well like you said how do you make sure someone doesn't walk away profitable well how would you you have to come up with a way to specify that and it kind of depends on exactly what you're trying to uh what you're trying to specify one thing you could say like for example i don't know these all these facts in like in the specifics but you say like you want to prove that someone will not be able to manipulate the price of a uni-swap uh swap as their you know in the body of the code for example yeah i mean like yeah sorry i mean like before we go into the details like the reason why i like express this concern because it sounded like to me at least it should be intuitively really easy to formalize something you know like like something like a property of like some energy preservation thing where you say like something that we're trying to talk about uh which is like you cannot mint or or like your total supply stays the same something in in the lines of you know whoever interacts with the contract loses took the gas or like always you know it it's it's more like you know like some some law of thermodynamics he interact with the contract you always come out you know at least losing the assets for the gas okay and it's and like in the direction you're going with is is trying to say like well uh trying to formalize is too abstract so you need to express more specifically what are the properties in there and then try to for like to prove formally that they they hold well well i'm saying can we can we come up with some set of like almost like a laws of thermodynamics but for the financial contracts that we can formulate overall for all financial contracts and then just run verification independently what is the body of the contract is uh that's a really cool idea um yeah i mean definitely get a committee on that just like trying to figure out what are like figure out the thermodynamics of financial contracts and you know make sure that i mean again since like you know i can publish a financial contract and it's term complete and you can do anything not all contracts are going to adhere to it but we can at least put down you know some best practices saying like all these things should always be respected by any good um financial contract that would be really cool i don't know what that would look like uh that would be really cool and it would i think definitely be amenable to um the formal verification one problem with smart contracts is that they like to call out to other contracts which is a good thing that's you know composability but it also means that you have to extend your assumptions to other contracts so you have to say like if you are doing if you're entering a specific function and that calls out to another contract and you want to make sure you don't violate the laws of thermodynamics you also have to assume that the other contract doesn't violate the laws of thermodynamics but what if your contract call can be pretty complex maybe like there's you know you're calling out a different contract and depending on you know the world state there are four different paths you can take and each one of those paths call out to a different contract all of a sudden like now you have like a pretty complex you might come up with a pretty complex system of interacting contracts um and and and of course you know users can define checks to say oh please call this contract in in the in the course of all this and i think it in practice it can be hard to do that like at code level co-level verification um unless like we have all the code which we usually don't because you know often you can call arbitrary contracts it's usually not a white list that you can only call these um and that's why it's often good to model it in a more abstract sense like make an abstract model of the system as interacting interacting objects and so on and try to work it out from there and that's i mean you know definitely if you're if you come from physics or something then for complex adaptive systems then that's i think that's a great exercise but then you know it's it's also interesting how do you bridge that gap because oftentimes you do verification at like a protocol level or a systems level uh and well what i do is usually i do verification at like the code level and there's definitely room for error in in the gap between those uh where like you know you have some implicit assumptions in your in your big model and those are slightly different in the code verification and you know that can be violated but basically you know if you if you're expressing your system in mathematical terms mathematical terms and doing some reasoning and proving things about your system you're doing formal verification and that's i mean that's just the description of the the action and whether it's usually useful or not depends entirely what you're doing just like in math there are absolutely you can do things that are not very meaningful you can do things that are really really important like you can calculate you know the triangular theorems in graphs that don't really have a strong application or you can calculate you know the stability of bridges and uh you know security of financial systems and so on so actually i have very similar question to what marx had asked just just from another standpoint but exactly about exactly the same problem i mean uh if when you started talk about formal verification as essentially mathematical modeling i think humanity has very long experience of mathematical modelling and especially in area physics and in physics we quickly realized well uh in any physics like one of examples um i was thinking about like like uh like gas dynamic for example or thermodynamics as as max said it's it's the same so you can in theory uh solve like a dynamic equations uh for every molecular in air to to to essentially make make a statement about uh uh like absolutely perfectly valid statements about uh about the air around you but that will be first uh absolutely understandable by a human uh who think about that and secondly it will be absolutely useless or you can say that it's like 25 degrees tells you in in this room and it will be like very simple statistic property which first makes sense and um and relatively easy like measured and and computed so so my point is that was exactly the same so from human point of view so if if you make a validation of very complex uh software models they became useless it's very easy to make to make a mistake it's not important how how smart is a particular person it just means that uh the like the complexity have to be like a little bit bigger and uh and and the brain will will break our brain is not that powerful technology and so we have we simplify and and like um the trick here is that are there a way to not to not model or not even precisely model but quite the opposite uh uh to model in in a way which uh uh which avoids uh like the then they need to understand every behavioral aspect of the program right still be useful for yeah absolutely absolutely and i mean that's that's i mean if you're doing like protocol verification that's often what you're doing you just have actors that uh that way that's more more discrete deterministic thing uh but again like i'm not coming from the realm of physics and like if you get a committee together and decide to work out like a theory of thermodynamics for these kinds of systems and a way to model you know your smart or the smart contract platform um where you can like look look for pro these kinds of properties that would be really cool um i'm not like again i'm not it's not my area of expertise so i'm not 100 sure what the use cases would be i can i can imagine something like okay that would be that would be great like you know money you know value isn't destroyed anywhere for example or even if it moves around in interesting and complex ways it doesn't like go up in smoke or so on but uh all i can say that it's that it sounds really cool but uh and no i not but it sounds really cool and i hope you do it and get back to me when you do um but i also want to counter your point on saying like you know oh if you're trying to verify a system that's super it's super complex uh then you know the brain is going to explode because it's so big and it's so hard i mean that that can be true but i mean verification one of the powers of verification is that you can ex you can have very complex systems that do a lot of tricky stuff and it's very hard to prove that they're right but the statement of correctness can still be quite simple like a famous example is the four color theorem um so basically the idea that any any world map or any possible word world map can be colored in using only four colors uh without having adjacent countries um having the same color i mean that's that's the layman's statement the proof is immensely complex like super complex and it's been verified with like you know proof assistance and but the thing is the thing is the statement is pretty straightforward and i i absolutely 100 believe the four caller theorem not because i can understand the proof but because i can understand at least somewhat the um the proof checker and someone says like i have a long string of you know that represents a proof we pass that through a very simple kernel that is a proof checker that only does like some very simple logic and won't allow you to do anything uh anything like obviously bad and it's going to say in the end oh yeah i've seen you've actually derived this simple thing you you here this is something that you have a simple statement and i can attest to that this complex body that is the proof actually proves this theorem and now we're done so i mean it and and your head doesn't have to explode around the theorem even though like the proof of course took like a huge amount of people and a lot of years to work out uh and i think that's one of the powers of verification because we often talk about how like the number of bugs in code scale with the number of lines of code and i'd say that you know the more complex your theorem statements are the easier it is to make a mistake if you have a lot of complex assumptions and complex encodings of states then it's going to be easy for you to make a mistake but oftentimes your your theorem statement can be quite small and the process of verification is often taking these more complex statements like for example we did here with the uh the transfer function i mean the statement the transfer function you know doesn't violate the loss of thermodynamics like the the amount of tokens stays constant or shrinks or whichever one we choose uh that's a simpler statement than saying every variable that is used somewhere in the body of the program has these properties at the input output that's a i'd say that's this the second statement of the problem leaves more room for error but you can use that to then prove the bigger theorem and i mean that's pretty common in mathematics you have like you have to if you're doing group theory like lagrange's theorem is really really easy to state and prove you can do it in a tweet but you have to create this more complex body of other things first but then the actual statement and the proof are pretty simple and i think that's one of the really cool things about verification is that you can kind of get this very high assurance because you have a very very small statement and you have i'd say absolute assurance that your statement is true um so yeah yeah i mean but in practice especially with smart contracts you often end up saying like you know well this is through given these and these assumptions because obviously it's a software system and this can be hard to encode these assumptions in an intuitive way yeah this sounds natural yeah so i guess we actually already like to 20 minutes before our like land deadline however uh i guess uh we have very interesting discussion i i personally truly truly enjoyed it and and like the ideas which we discussed here and so i want to say say thanks thanks a lot to eureka to to max for for like for for joining this this talk and and so maybe uh we can we can continue discussing uh this uh this manners in matters in in some in some other format uh because because it seems to be very very deep and very uh they say uh uh strangely it's very practical in a sense because because what we do we we we all write a complex system and we and we regularly and routinely verify them so so probably discussing it with uh from more like a distant point of view maybe very uh very enlightening for any software engineer so thank you a lot thank you so much it was uh fun all right see ya thanks around for listening","transcript_synced_at":"2026-11-04T04:24:58.231Z","segments":[{"start_seconds":4,"text":"all right uh rickard thanks for joining us and uh do you want to introduce yourself","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4s"},{"start_seconds":12,"text":"um yeah i'm ricardo i am a former verification engineer","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=12s"},{"start_seconds":18,"text":"with runtime verification and blockchain nerd","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=18s"},{"start_seconds":26,"text":"and day-to-day i work on on k awesome which is our implementation of webassembly","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=26s"},{"start_seconds":33,"text":"so that's so when you say when you say your implementation of assembly you who","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=33s"},{"start_seconds":41,"text":"uh so runtime verification or the the k framework uh implementation of webassembly so basically it's a formal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=41s"},{"start_seconds":49,"text":"formal and executable specification of web assembly uh written in what would look like a high","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=49s"},{"start_seconds":57,"text":"functional language to many programmers i think i see but it has some nice special properties i'm sure we'll get around to talking more about it","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=57s"},{"start_seconds":66,"text":"cool and nikolai what do you do yes uh i work near","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=66s"},{"start_seconds":75,"text":"uh helping with uh with what we call the contract runtime which is which is essentially","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=75s"},{"start_seconds":82,"text":"the way how we execute uh contracts smart contracts which which are technically","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=82s"},{"start_seconds":90,"text":"web assembly programs inside of our blockchain and how we integrate it with what you call","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=90s"},{"start_seconds":98,"text":"transactional which is essentially uh the part responsible for the functioning of uh of the blockchain as a distributed","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=98s"},{"start_seconds":107,"text":"database this consequences so i'm working also with nikolai my name is max","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=107s"},{"start_seconds":115,"text":"on the runtime which as he said includes the execution of the contracts also trying to figure out all possible safety aspects of our runtime","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=115s"},{"start_seconds":123,"text":"because safety is incredibly important for the blockchain you kind of can live without liveness if you if your node stalls","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=123s"},{"start_seconds":131,"text":"or crashes it's okay you can just restart it have some social consensus about things you know when to restart the notes or","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=131s"},{"start_seconds":138,"text":"whatever get a new binary version but if your safety is broken it can be fatal for the blockchain therefore it's mine and nikolai's huge","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=138s"},{"start_seconds":146,"text":"focus in our contract runtime and transaction runtime on how do we make sure the contracts","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=146s"},{"start_seconds":153,"text":"execute deterministically and execute correctly that's what we're going to be discussing today","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=153s"},{"start_seconds":161,"text":"so i'm going to let you guys kick it off actually oh i think","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=161s"},{"start_seconds":169,"text":"it would be very nice before we start discussing like particular technologies such as webassembly or","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=169s"},{"start_seconds":176,"text":"formal verification of runtime verification the company uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=176s"},{"start_seconds":183,"text":"to discuss a little bit uh background ideas like mathematics behind that uh the reasoning behind behind the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=183s"},{"start_seconds":192,"text":"formal verification so regard what would you like to share um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=192s"},{"start_seconds":200,"text":"well in essence i think um a good way to describe it is that formal verification is a process which takes","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=200s"},{"start_seconds":209,"text":"right a bit it takes a program you take a program p and a specification","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=209s"},{"start_seconds":218,"text":"s are you writing somewhere yeah can you see it in the whiteboard oh now i can wait wait a second great","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=218s"},{"start_seconds":228,"text":"you put it through this typical program refreshing magic box","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=228s"},{"start_seconds":237,"text":"and out comes either a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=237s"},{"start_seconds":247,"text":"proof that the specification holds or a counter","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=247s"},{"start_seconds":254,"text":"example and in in in theory that that's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=254s"},{"start_seconds":262,"text":"that's what you want but in practice there's also this uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=262s"},{"start_seconds":269,"text":"slight possibility that we often don't talk about that you can report uh i don't know like the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=269s"},{"start_seconds":278,"text":"we could neither find a counter example or a proof but but in principle you you formulate something you want to hold of your","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=278s"},{"start_seconds":286,"text":"program for example you know the if it's a token contract it could be uh the number of tokens are is constant","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=286s"},{"start_seconds":294,"text":"or no one can have negative balance uh and then you give the the program the contract as input and you ask a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=294s"},{"start_seconds":302,"text":"system to uh prove that this is true or come up with a counter example and you often end up in this kind of don't don't know face","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=302s"},{"start_seconds":310,"text":"so this this box here often requires some manual manual","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=310s"},{"start_seconds":318,"text":"intervention uh and that's what formal verification engineers spend a lot of a lot of their time on","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=318s"},{"start_seconds":327,"text":"and what is the language for expressing b and deaths respectively so how i think","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=327s"},{"start_seconds":334,"text":"for b it's mostly like predefined and depends on the on the area where you essentially perform the phone verification","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=334s"},{"start_seconds":342,"text":"but how do you formulate s well i mean there are many ways to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=342s"},{"start_seconds":349,"text":"formulate p as well i mean you can't say well it's just a program but the thing the thing that is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=349s"},{"start_seconds":357,"text":"say i'm going to say it's implicit in all of this is that there is this semantics that are goes into the box","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=357s"},{"start_seconds":366,"text":"and that's one way to express what a program is so essentially it's like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=366s"},{"start_seconds":374,"text":"you define you define the world of all programs in a language","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=374s"},{"start_seconds":383,"text":"that could be rust or webassembly or what have you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=383s"},{"start_seconds":388,"text":"and then your program is just a specific a specific element in this","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=388s"},{"start_seconds":395,"text":"world of languages but to do formal verification you need to express this language l in a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=395s"},{"start_seconds":403,"text":"mathematical fashion and that's for example the the web assembly implementation i'm working on is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=403s"},{"start_seconds":410,"text":"basically a way of turning the webassembly written","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=410s"},{"start_seconds":418,"text":"admittedly mathematical um specification into uh another mathematical specification that we can run","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=418s"},{"start_seconds":426,"text":"uh with our system so the way you express s","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=426s"},{"start_seconds":435,"text":"depends on how you have expressed the language l or rather like how you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=435s"},{"start_seconds":441,"text":"express this world around here um so you usually don't just give the program as source","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=441s"},{"start_seconds":448,"text":"text into this system or you you can but the first thing that is bound to happen is that the program is turned into this","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=448s"},{"start_seconds":455,"text":"mathematical object and for example we use something called matching logic so you write your specifications in","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=455s"},{"start_seconds":463,"text":"matching logic uh if it's a if you're using a tool like isabel hall","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=463s"},{"start_seconds":470,"text":"you will have a you'll have an isabelle hall model","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=470s"},{"start_seconds":477,"text":"of of the language and you can express things in regular higher order logic","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=477s"},{"start_seconds":485,"text":"or it could be first order logic it's it's it depends on the tool and the best way to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=485s"},{"start_seconds":492,"text":"come up with or finding a good balance between powerful specification languages where you can express","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=492s"},{"start_seconds":500,"text":"a lot of things and but you don't want to be able to express too much because if you have a too","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=500s"},{"start_seconds":508,"text":"powerful specification language then you uh verification can become harder so there's a balance to be found there","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=508s"},{"start_seconds":516,"text":"and there's also obviously a user experience aspect to it uh where you know you want to find a way to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=516s"},{"start_seconds":523,"text":"express specification that makes sense to developers a very easy way could be to have assertions","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=523s"},{"start_seconds":530,"text":"in your code and then just have the tool transform those or transform the specification into or write a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=530s"},{"start_seconds":539,"text":"specification for you that basically says we're never going to revert because of an assertion but you might want to express temporal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=539s"},{"start_seconds":547,"text":"properties as well like say like well if if you ever touched this variable during the run of the program you are not allowed to touch this later","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=547s"},{"start_seconds":556,"text":"and that can be harder to express but doesn't it actually mean that in a good case or for for modification","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=556s"},{"start_seconds":565,"text":"p and s better be the same uh because uh it like programmer","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=565s"},{"start_seconds":571,"text":"uh shall express his her desire in a program and a part of the those","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=571s"},{"start_seconds":580,"text":"like desires and tensions uh logic you also express the invariance so for example","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=580s"},{"start_seconds":588,"text":"a search as i mentioned is is a very simple form of the formal runtime verification so why do we","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=588s"},{"start_seconds":596,"text":"want to go beyond asserts um well first of all like i personally agree with you like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=596s"},{"start_seconds":604,"text":"and a big part of uh making formal verification more widespread is to make sure that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=604s"},{"start_seconds":611,"text":"it's has good ergonomics for developers and you know systems where you can use asserts or do","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=611s"},{"start_seconds":621,"text":"um or do uh like write annotations for like pre and post conditions for example","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=621s"},{"start_seconds":629,"text":"that usually makes more sense for the developer the problem is that if you want to do","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=629s"},{"start_seconds":638,"text":"source level verification or like you know if if you just want to have the developer as the writing code also you know write specifications","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=638s"},{"start_seconds":648,"text":"that's often a good thing but there's not necessarily a big chance that the automatic formal verification engine is going to be able","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=648s"},{"start_seconds":656,"text":"to prove that and if you're a former verification engineer you usually know your tool the the engine you're working well with","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=656s"},{"start_seconds":664,"text":"pretty well and some ways the formulating specifications are more amenable to verification","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=664s"},{"start_seconds":672,"text":"and you might want to like take this high level specification and break it up into many different smaller uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=672s"},{"start_seconds":679,"text":"smaller sub goals that you want to prove for example and then then you need to have a language to express it in i mean it's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=679s"},{"start_seconds":686,"text":"the same thing if you write if the first thing that happens to the program is that you it will be expressed in this um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=686s"},{"start_seconds":695,"text":"mathematical specification of the language if the specification is also part of the source code then the same thing happens with the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=695s"},{"start_seconds":704,"text":"specification the specifications derived from the source code but the first thing that gets put into the actual formal verification tool is going to be this","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=704s"},{"start_seconds":714,"text":"it's going to be written in you know some specification language that is usually more powerful um and you want i mean if you're doing","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=714s"},{"start_seconds":722,"text":"formal verification you probably want to be able to you know write your own specifications that you don't have to go through the source code to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=722s"},{"start_seconds":731,"text":"implement but actually if we talk about languages uh i think uh usually there are like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=731s"},{"start_seconds":740,"text":"formal languages in like in in the form of formal grammar","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=740s"},{"start_seconds":749,"text":"standing behind the language and that's kind of one layer of languages but actually uh with languages there is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=749s"},{"start_seconds":757,"text":"associated around time semantics and certain behavior behavioral characteristics","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=757s"},{"start_seconds":764,"text":"and the question is which part of the language is actually to be addressed by the formal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=764s"},{"start_seconds":773,"text":"verification is it is it on time behavior is it like a certain uh syntactical properties","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=773s"},{"start_seconds":780,"text":"of the language well i can't really think of anything that would be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=780s"},{"start_seconds":788,"text":"all that interesting to uh verify uh just using syntax i mean usually most languages try to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=788s"},{"start_seconds":798,"text":"have a very like straightforward uh and not too complex and undecidable um grammar like if you want to write a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=798s"},{"start_seconds":805,"text":"parser you'll write an lr1 parser like you know that's parsing techniques um but then to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=805s"},{"start_seconds":814,"text":"give meaning to your language uh that's sort of where the magic happens so so to speak uh and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=814s"},{"start_seconds":824,"text":"that's also you know where languages become more equivalent any touring complete language is essentially you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=824s"},{"start_seconds":832,"text":"are essentially the same to some extent and the way you define what each construct in the language does","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=832s"},{"start_seconds":841,"text":"i'd say that's the that's the more interesting part i mean i'm thinking whether there's something that could be very","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=841s"},{"start_seconds":848,"text":"interesting to verify as like what a programmer usually thinks of the pure syntax but i mean if it's rejected by the parser then","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=848s"},{"start_seconds":858,"text":"you're probably going to have a parse error and resolve that and that's i mean the parser is a verifier it verifies that your","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=858s"},{"start_seconds":865,"text":"what you're giving it is something that is expressible in the language syntactically and the type the type checker is a verifier","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=865s"},{"start_seconds":874,"text":"it verifies that uh you are not doing anything that's considered illegal by the languages type system yeah","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=874s"},{"start_seconds":883,"text":"yeah okay so like on a different level layers or levels of of the language","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=883s"},{"start_seconds":889,"text":"uh there are different rules like on the lowest level uh there are like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=889s"},{"start_seconds":897,"text":"pretty much syntactic rules of of the of the formal language on the on the level of the type system there are different uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=897s"},{"start_seconds":905,"text":"different computation essentially expressed in a type system and i think a significant part of of the language research","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=905s"},{"start_seconds":913,"text":"like during last 50 years was put into into essentially making a type system such that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=913s"},{"start_seconds":920,"text":"uh most of the semantics are are actually caught on on the level of of the type system and and so my question about like like the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=920s"},{"start_seconds":929,"text":"formal verification as a technique is is essentially how it augments uh the research because like every","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=929s"},{"start_seconds":937,"text":"everybody knows how to write parsers many people know how to do like a type system","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=937s"},{"start_seconds":943,"text":"and how to how to perform uh like uh like that type checkers on on lattices","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=943s"},{"start_seconds":950,"text":"and so on but uh i think uh not so many people at least not myself are aware how to go on on the next","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=950s"},{"start_seconds":958,"text":"semantic layer which which is which is higher than a type system so how to express uh formal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=958s"},{"start_seconds":966,"text":"statements in that area which builds like a complete exchange system which which could be actually used for","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=966s"},{"start_seconds":974,"text":"uh as as input for any like reasoning machine which","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=974s"},{"start_seconds":981,"text":"which any formal verifier is and so that's that's pretty much my question","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=981s"},{"start_seconds":990,"text":"just so i understand you correctly you're you're trying to like figure out what what's what's what's the gap between you know the the type level kind of verification that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=990s"},{"start_seconds":998,"text":"a programmer is expected to do and what the things that we usually call formal verification where you know you hire a formal verification engineer to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=998s"},{"start_seconds":1006,"text":"prove properties of your program i mean really yes pretty much it's like it looks more like uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1006s"},{"start_seconds":1014,"text":"the for example type verification is absolutely like mathematical procedure it's an algorithm you once you have a described","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1014s"},{"start_seconds":1022,"text":"system uh for the language and it's usually in some form it's formalized as a part of the language uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1022s"},{"start_seconds":1028,"text":"you can verify that the types type attribution is correct in a particular program and that's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1028s"},{"start_seconds":1036,"text":"mechanical process and you don't need any additional uh operation and it's not important in the program","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1036s"},{"start_seconds":1043,"text":"uh like on the same language if if it's like a word processor or web server the type syst the type","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1043s"},{"start_seconds":1051,"text":"system manipulation will be exactly the same and because because it's compiler and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1051s"},{"start_seconds":1058,"text":"which does the verification and so my question is um imagine uh if you have a form of verification","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1058s"},{"start_seconds":1066,"text":"or what is the formal system against which verification happens so like how","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1066s"},{"start_seconds":1072,"text":"how uh how it could be built how it is built in in your tool or not in other tools","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1072s"},{"start_seconds":1081,"text":"um well so in in our tool um it's built through something called matching logic","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1081s"},{"start_seconds":1089,"text":"which looks fairly similar to most logics that people may have encountered but it's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1089s"},{"start_seconds":1096,"text":"slightly more slightly more expressive um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1096s"},{"start_seconds":1103,"text":"but say for example in isabella hall you are using a slightly","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1103s"},{"start_seconds":1110,"text":"more familiar probably higher order uh logic to express the um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1110s"},{"start_seconds":1120,"text":"the meaning of of of programs and i mean","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1120s"},{"start_seconds":1126,"text":"it's not really the type system and like these kind of formal verification uh things we generally do are not really","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1126s"},{"start_seconds":1135,"text":"in uh competition because the idea with the type system is usually that it's supposed to be uh fully decidable","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1135s"},{"start_seconds":1143,"text":"like i mean it should be pretty straightforward for your type checker to just say this well typed or it's not well typed","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1143s"},{"start_seconds":1150,"text":"uh and might be unification like oh you're doing addition and you know it's going to see that you know one uh actually this is a good","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1150s"},{"start_seconds":1158,"text":"whiteboard moment like if you have if you're doing one plus one somewhere in your program or rather if you're doing like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1158s"},{"start_seconds":1167,"text":"p plus q and the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1167s"},{"start_seconds":1174,"text":"type checker can infer that this is an int and this is an int then you know this expression is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1174s"},{"start_seconds":1181,"text":"it's well typed but that for that the um the type checker must be able to infer","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1181s"},{"start_seconds":1188,"text":"the type of every every expression the program uh which puts a limit on","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1188s"},{"start_seconds":1195,"text":"the type system's expressiveness if you want to have a type system that can express","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1195s"},{"start_seconds":1202,"text":"any anything then you move into undecidable territory now type checking becomes undecidable and i","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1202s"},{"start_seconds":1209,"text":"mean this this limitation here that you will sometimes end up in don't know that's just like a sort of mathematical","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1209s"},{"start_seconds":1217,"text":"threshold you cross at some point things are no longer decidable decidability means","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1217s"},{"start_seconds":1225,"text":"there is an algorithm that can decide this and will always be successful regular type checking is something like haskell or rust or java is decidable","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1225s"},{"start_seconds":1235,"text":"because the type checker will always succeed to tell you whether your program is well typed or not","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1235s"},{"start_seconds":1241,"text":"but if you want to have a slightly more expressive logic system uh things become","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1241s"},{"start_seconds":1249,"text":"undecidable so a question you're saying it's undecidable when it's theoretically undecidable not something","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1249s"},{"start_seconds":1256,"text":"that your tool cannot uh infer because of there's some computational limitations well i mean i mean obviously there can","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1256s"},{"start_seconds":1265,"text":"be computational limitations like i mean there is there is definitely a uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1265s"},{"start_seconds":1273,"text":"i mean in practice for example i think in isabel there's a tactic that i think is called blast which is technically","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1273s"},{"start_seconds":1280,"text":"uh you know it can take certain i think linear formulas let's call and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1280s"},{"start_seconds":1287,"text":"do and check if they are uh true and it's like a com uh sorry i lost the word it's not is it","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1287s"},{"start_seconds":1296,"text":"you don't say that it's complete well you know it's it should always succeed in theory but in practice there's obviously a timeout limit some some somewhere the children give up","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1296s"},{"start_seconds":1305,"text":"but there is also um i mean the halting problem and so forth exactly the halting problem is like the example that you know like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1305s"},{"start_seconds":1314,"text":"if if i give you the simplest if i make the simplest turing complete language or if i give you lambda calculus and say well you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1314s"},{"start_seconds":1321,"text":"will this program ever terminate for a great deal of programs that's pretty straightforward uh but there are there are going to be some programs","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1321s"},{"start_seconds":1329,"text":"where it's not straightforward so for example i mean people often confuse this and think that oh you know the halting problem is undecidable","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1329s"},{"start_seconds":1337,"text":"therefore they can't be you know it's meaningless to try but honestly in many cases i mean if you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1337s"},{"start_seconds":1345,"text":"if you're writing a smart contract and your contract just looks like this it's just like straight line code then i can tell you well you know if and this","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1345s"},{"start_seconds":1353,"text":"contains no calls and no jumps then i can tell you you know this is going to terminate but if you have a jump in here or you have a little","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1353s"},{"start_seconds":1361,"text":"while loop all of a sudden uh then it becomes more complex maybe i","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1361s"},{"start_seconds":1370,"text":"won't be able to decide whether this terminates or not","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1370s"},{"start_seconds":1374,"text":"but for and the way many tools work is that they make sure that you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1374s"},{"start_seconds":1381,"text":"uh when you write like certain functions for example in isabel you also have to provide a termination","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1381s"},{"start_seconds":1388,"text":"proof but if you if you just define your functions and start using certain simple","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1388s"},{"start_seconds":1396,"text":"structures then the program can automatically tell you sure this is going to terminate and if you want to do something more complex","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1396s"},{"start_seconds":1403,"text":"then it's your job to also provide a proof so the loops also include like loops in","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1403s"},{"start_seconds":1410,"text":"let's say standard arithmetic operations mathematical operations like let's say hash computation","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1410s"},{"start_seconds":1417,"text":"right or or like signature computation i mean like if if we use it somewhere in our code","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1417s"},{"start_seconds":1425,"text":"then we might end up in this done don't know state um what was your example","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1425s"},{"start_seconds":1434,"text":"well i mean let's say we have like a very simple example that our our program verifies certain uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1434s"},{"start_seconds":1442,"text":"hash or like certain signature right and like we want to prove that the assertion","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1442s"},{"start_seconds":1449,"text":"that says the hash doesn't match never never fires in the program and so we cannot really prove it for for the input because you need to literally","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1449s"},{"start_seconds":1458,"text":"pre-image the hash which right and but but like hash but this is like an example of like a very simple","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1458s"},{"start_seconds":1466,"text":"program where you just have a hash computation and you just cannot prove that the program will not panic because the hash has been like one","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1466s"},{"start_seconds":1474,"text":"way function has been is being used somewhere in the code but those one way functions are like incredibly popular in in smart contracts even like basic","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1474s"},{"start_seconds":1482,"text":"like asset manipulation like defy contracts so wondering whether if someone drops in this kind of like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1482s"},{"start_seconds":1489,"text":"crypto function will it automatically you know uh make it unusable that they formulification usable","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1489s"},{"start_seconds":1498,"text":"oh oh no and i mean for example you i think you can scroll down a bit maxim i'm just yep let me scroll down below","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1498s"},{"start_seconds":1505,"text":"uh there you go that's my terrible like what you do in general let's see where you are okay","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1505s"},{"start_seconds":1512,"text":"uh what we tend to do is like we if if we have um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1512s"},{"start_seconds":1520,"text":"i mean often you're doing something called symbolic symbolic execution which means that instead of like put inputting specific values","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1520s"},{"start_seconds":1527,"text":"into your program you are inputting um let's see there we go","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1527s"},{"start_seconds":1534,"text":"uh you're inputting like a variable x right and so say","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1534s"},{"start_seconds":1540,"text":"your your input to a program is x and then at some points you get to a place where you do hash","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1540s"},{"start_seconds":1548,"text":"x oops since x is unknown we probably won't be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1548s"},{"start_seconds":1556,"text":"able to call this function so what we'll do is we'll just leave the symbolic variable hash x here and now we know certain things about","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1556s"},{"start_seconds":1564,"text":"this value x for example it's between 0 and 2 to the power","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1564s"},{"start_seconds":1571,"text":"256 minus 1 or something right and we also know that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1571s"},{"start_seconds":1580,"text":"if you do if you also have y and you do hash oops i mean the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1580s"},{"start_seconds":1588,"text":"because you you're just defining it as a function and if you say well let's do hash y then we have the same situation but now","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1588s"},{"start_seconds":1596,"text":"i if you ask me to prove can you prove that uh hash oops sorry it's a bit of a lag on my end","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1596s"},{"start_seconds":1603,"text":"so this becomes pretty ugly uh if you ask me to prove given that x equals y that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1603s"},{"start_seconds":1613,"text":"hash of x and hash of y are the same","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1613s"},{"start_seconds":1620,"text":"i can do that because that's a work that's i i just have that as some assumption of my specific hash function i i write like a lemma saying that you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1620s"},{"start_seconds":1628,"text":"know this hash is correct and that's usually what you do you you're i think it's tony that said something like uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1628s"},{"start_seconds":1636,"text":"the job of formal methods is to elucidate the assumptions upon which formal correctness depends that's a fancy way of saying well","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1636s"},{"start_seconds":1645,"text":"the way you're doing formal verification is you're trying to figure out that something is correct given certain assumptions","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1645s"},{"start_seconds":1651,"text":"so for example if you if i'm verifying a smart contract i will often assume things about cryptography","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1651s"},{"start_seconds":1659,"text":"because i'm not really proving things about cryptography and proving things about the program and i will say this program is correct given that the cryptographic","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1659s"},{"start_seconds":1667,"text":"primitives are correct like you know if i do encrypts x with a key","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1667s"},{"start_seconds":1676,"text":"that's a key and then i do decrypt with the same key","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1676s"},{"start_seconds":1685,"text":"i have a lemma saying or like i have an assumption essentially saying well you know that's going to be the same thing as x if i encrypt it and then decrypt it and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1685s"},{"start_seconds":1693,"text":"i use the same key that's going to work i will also have or i might have a lemma saying the opposite but you know i mean i guess there's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1693s"},{"start_seconds":1701,"text":"usually a chance that there is some probability that the problem with crypto with cryptography is that it's very probabilistic","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1701s"},{"start_seconds":1708,"text":"so for example if i'm computing if i'm storing two values let's say x and y are not equal and you ask me","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1708s"},{"start_seconds":1716,"text":"is hx equals to hy the answer is maybe unfortunately we could just add as a an assumption","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1716s"},{"start_seconds":1724,"text":"saying that oh you know if x and y aren't equal their hashes are not going to be the same basically there are no pre-images that's not true but you can say that you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1724s"},{"start_seconds":1733,"text":"know given that you're not getting a house collision your program is correct and then you can decide and then you can employ your reasoning","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1733s"},{"start_seconds":1740,"text":"about that to say if that's good enough for you if if your data is longer than","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1740s"},{"start_seconds":1747,"text":"uh 256 bits then for 256 bit hashtags you are guaranteed to have at least one collision","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1747s"},{"start_seconds":1755,"text":"that's uh like uh that's obvious so yes i mean so the the point is and and that's why i","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1755s"},{"start_seconds":1764,"text":"come back to this this horror quote is that what you're doing is you're usually not saying you know this program will","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1764s"},{"start_seconds":1772,"text":"always work in every circumstance because you know there are physical there's a physical world out there and things can go wrong","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1772s"},{"start_seconds":1779,"text":"and you know no it's just going to work correctly given that every node fails in the same way at the same time","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1779s"},{"start_seconds":1786,"text":"maybe not but you can if you just have encode that as an assumption that you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1786s"},{"start_seconds":1793,"text":"your virtual machine is deterministic or you encode as an assumption that you will never have a hash collision then you can prove certain things","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1793s"},{"start_seconds":1801,"text":"but that also means your proof doesn't work unless you state that as an assumption and that's valuable right um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1801s"},{"start_seconds":1809,"text":"and you can remove that assumption and say oh no our contract works even if there are hash collisions uh but either either way you can","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1809s"},{"start_seconds":1817,"text":"i mean you're not you wouldn't you probably wouldn't state that you know there are no such thing as hash collisions because that's i mean that's patently wrong you could","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1817s"},{"start_seconds":1826,"text":"use like you said the pigeonhole principle to prove that wrong and now your whole system is unsound but you could add an assumption saying","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1826s"},{"start_seconds":1833,"text":"well for these particular values x and y they do not collide and then you can prove that you know you're","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1833s"},{"start_seconds":1841,"text":"you're no one no one is able to steal your tokens given that they can't produce a pre-image for example","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1841s"},{"start_seconds":1847,"text":"um and actually like i really like our discussion however it gets very","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1847s"},{"start_seconds":1854,"text":"uh very theoretical and probably uh close to like mathematical problems","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1854s"},{"start_seconds":1861,"text":"or even like foundation of computations let's say so so if we","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1861s"},{"start_seconds":1869,"text":"i have i hate to be kind of a moderating person here but but i guess to make it more like closer","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1869s"},{"start_seconds":1877,"text":"to the theme which we which we aim to discuss uh we probably can discuss more like a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1877s"},{"start_seconds":1884,"text":"practical aspect so so imagine that in our case p is like a rust smart contract uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1884s"},{"start_seconds":1893,"text":"could you give an example what would be an s in your uh verification example and how uh how does it bring the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1893s"},{"start_seconds":1900,"text":"value to uh to the like a normal developer who's not mathematician not a formal logician but like like a smart","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1900s"},{"start_seconds":1909,"text":"person writing smart contracts um sure i mean if so if you're writing a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1909s"},{"start_seconds":1916,"text":"program in rust and um i mean the my standard example is it's a token contract and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1916s"},{"start_seconds":1924,"text":"i mean history has proven that history like the last 10 years have proven that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1924s"},{"start_seconds":1931,"text":"even something as on the surface simple as a token contract can have all kinds of","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1931s"},{"start_seconds":1938,"text":"really bad bugs in them a program that looks super simple can you know accidentally mint tokens","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1938s"},{"start_seconds":1946,"text":"um and so i mean that that's that's an s that i usually take as an example that uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1946s"},{"start_seconds":1954,"text":"the in a token transfer the the outgoing sum of every um of every","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1954s"},{"start_seconds":1964,"text":"address touched or the outgoing balance of every program touch is equal to the sum of all the in-going balances","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1964s"},{"start_seconds":1972,"text":"so if uh a on the inputs plus","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1972s"},{"start_seconds":1980,"text":"b on the input plus you know forever is equal to if if these are all the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1980s"},{"start_seconds":1987,"text":"the addresses that are sent as input to the transfer function","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1987s"},{"start_seconds":1995,"text":"uh and you know these can be very complex you know it can be like oh it's delegating to someone somewhere and it's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=1995s"},{"start_seconds":2002,"text":"you know giving something to the um to the contract owner address and whatever but i can say that you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2002s"},{"start_seconds":2009,"text":"the in-going um the in-going transfer or the balances has to be the same as","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2009s"},{"start_seconds":2018,"text":"the outgoing balances and i mean this fails for all kinds of reason i mean you could say","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2018s"},{"start_seconds":2024,"text":"you might or you know the transfer might fail an excellent example of course is overflow i mean if one of these","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2024s"},{"start_seconds":2033,"text":"if one of the addresses overflow during the transfer then this doesn't hold um and so you might say that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2033s"},{"start_seconds":2041,"text":"okay this is going to hold assuming that all the uh none of the addresses there's no overflow in here and you have","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2041s"},{"start_seconds":2050,"text":"to express that as a property like assuming that you know the changes in balances don't cause overflow uh this works this is once one property","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2050s"},{"start_seconds":2059,"text":"you want to hold but another property you want to hold for example is that all the all the balances uh oh sorry","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2059s"},{"start_seconds":2067,"text":"all the out balances should be uh oh wait sorry","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2067s"},{"start_seconds":2075,"text":"actually let me do this by text that's easier so a i a i","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2075s"},{"start_seconds":2084,"text":"uh b i etc uh the outgoing balances are larger","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2084s"},{"start_seconds":2092,"text":"than zero or so that the ingoing balance are a lot larger than zero that's going to imply that all the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2092s"},{"start_seconds":2100,"text":"outgoing balances are larger equals zero for example and that's another property you might want to prove um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2100s"},{"start_seconds":2108,"text":"and from from this you might want to prove that you know the um the the total amount of tokens","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2108s"},{"start_seconds":2117,"text":"in the contract is always the same this might not be something you want maybe this contract is supposed to do minting um but i mean","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2117s"},{"start_seconds":2124,"text":"from this perf you might be able to extract quite easily the property like okay if you do a transfer the transfer doesn't","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2124s"},{"start_seconds":2132,"text":"affect the number of tokens in the contract um and i think one way this can help a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2132s"},{"start_seconds":2140,"text":"developer and we often have this conversation it's like how can we make formal verification easier one way to make format verification easier is to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2140s"},{"start_seconds":2148,"text":"make sure you're always very explicit about your assumptions and you try to like at least give enough information in your comments or your","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2148s"},{"start_seconds":2156,"text":"specification documents or by the way you name things or whatever that or by assertions","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2156s"},{"start_seconds":2163,"text":"uh that uh it make it look very clear that these kind of things can never be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2163s"},{"start_seconds":2171,"text":"be violated but i mean if you just write a straightforward transfer function","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2171s"},{"start_seconds":2178,"text":"there are many ways that can go wrong but if you write this down this kind of specification and then try to just look at your code","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2178s"},{"start_seconds":2187,"text":"you're going to there's probably going to be places in there where where this is violated and then you need to start thinking okay am i sure that this is going to go back to uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2187s"},{"start_seconds":2195,"text":"a proper state like there might be there's going to be somewhere where the value of ace balance has been","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2195s"},{"start_seconds":2203,"text":"decremented without the value of these balance have been having been incremented and so on so i think like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2203s"},{"start_seconds":2210,"text":"until we get i mean our tools are improving rapidly we're in like a formal methods renaissance","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2210s"},{"start_seconds":2217,"text":"but for the programmer on the ground right now i think starting to familiars become a bit familiar with formal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2217s"},{"start_seconds":2225,"text":"verification and maybe with like property-based testing is an excellent way to make use of this right now","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2225s"},{"start_seconds":2233,"text":"because if you just start writing down your assumptions and your invariance then you're probably going to catch","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2233s"},{"start_seconds":2241,"text":"yourself making certain mistakes or or end up i mean if you if you write down an invariant that's saying like for example say you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2241s"},{"start_seconds":2248,"text":"never want your contract balance to you want it to be constant and you just look over your contract and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2248s"},{"start_seconds":2255,"text":"you're trying to like make sure that that holds if there's one function where you're kind of scratching your head and saying oh i'm not sure but yes i think i put it","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2255s"},{"start_seconds":2264,"text":"i think i thought it through once and it should work then maybe you can rewrite that function to make it clearer and convince yourself and others that um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2264s"},{"start_seconds":2273,"text":"that it's correct so i i think the formal methods thinking and approach is valuable to everyone and i mean especially in the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2273s"},{"start_seconds":2282,"text":"defy world yeah yeah i just i just wanted to say that it's like it's what you described sounds like a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2282s"},{"start_seconds":2290,"text":"very good hinging which most good programmers i i'm aware of pretty much follow even without without","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2290s"},{"start_seconds":2299,"text":"much of the for training in you know formal verification so like i know that good programmers writing complex systems","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2299s"},{"start_seconds":2307,"text":"always write a source so like like checking your invariants frequently as possible is is very common and very good","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2307s"},{"start_seconds":2316,"text":"habit that's uh that's i'm fully agree but this kind of uh gets back to the previous question which","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2316s"},{"start_seconds":2325,"text":"i had so don't you really believe that uh the best practical form of verification","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2325s"},{"start_seconds":2332,"text":"is where at least languages for p and s coincide all mover even where uh the pia and that's itself inside so","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2332s"},{"start_seconds":2340,"text":"where uh the formal verification must be a part of the program yeah i would even add","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2340s"},{"start_seconds":2348,"text":"to that because i was going to ask in the same kind of lines the question that you know when engineers design a program and have","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2348s"},{"start_seconds":2357,"text":"invariance in mind they they enforce them through asserts for the assertions right and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2357s"},{"start_seconds":2365,"text":"the the way they basically the assertions that express the invariance is the is the s","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2365s"},{"start_seconds":2372,"text":"for the engineers like that's what i think nikola is going with is that you have a program right you wrote a program and then you go over and you try","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2372s"},{"start_seconds":2380,"text":"to make sure that the invariants hold and your ass is actually a set of assertions that you put in the in the strategic spots in your program","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2380s"},{"start_seconds":2389,"text":"and since they have to do it like anyway like good engineers right they have to they need to be aware of the invariants","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2389s"},{"start_seconds":2396,"text":"and have to add the asserts everywhere um where does the value of the formalification comes in since","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2396s"},{"start_seconds":2404,"text":"we enforce the invariance through the asserts like why do we need why do we need to prove them additionally on top of that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2404s"},{"start_seconds":2412,"text":"um i mean that depends i mean i guess there are two kinds of asserts one one kind of assert is like you know sanity checking that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2412s"},{"start_seconds":2419,"text":"everything works and if it doesn't abort like you know checking well is someone trying to transfer money to themselves then you know we","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2419s"},{"start_seconds":2427,"text":"you can abort for example or that kind of thing but another way we could use a search that isn't that isn't really meant to be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2427s"},{"start_seconds":2436,"text":"functional is writing down these research that should never be violated and you believe that there is no way they can be violated","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2436s"},{"start_seconds":2444,"text":"uh those are the kind of research you probably want to remove at compile time it depends but i mean those could cause","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2444s"},{"start_seconds":2452,"text":"your contract to to um dost like you know well if if you have an assert that you think can never be violated","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2452s"},{"start_seconds":2459,"text":"and all of a sudden you know and you know that's say in the transfer function um and somehow you're wrong and that ends","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2459s"},{"start_seconds":2468,"text":"up being violated uh and there's no and the only way to modify it is by you know calling transfer then you know you're","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2468s"},{"start_seconds":2476,"text":"never going to be able to transfer anything with your token contract again and now your token is like worthless probably","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2476s"},{"start_seconds":2483,"text":"yeah um so i i say there are two kinds of research like people will often like you know write a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2483s"},{"start_seconds":2491,"text":"cert like sanity checking your input like you call this thing correctly and you're not going to break anything if that's wrong we're just going to if this is his theory we're going to eat","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2491s"},{"start_seconds":2499,"text":"your gas or you know it's it's your problem um and but that's that's input validation","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2499s"},{"start_seconds":2507,"text":"and that's that's saying and that's exactly like you're saying every like or most good engineers when they're not under the very like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2507s"},{"start_seconds":2515,"text":"some certain very tight deadline or something they should have those in place um but they're also the the system invariants and i","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2515s"},{"start_seconds":2525,"text":"think i mean my i i haven't been over all all the all the contracts all the different platforms but i think","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2525s"},{"start_seconds":2533,"text":"those are usually less not present as much and those are really","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2533s"},{"start_seconds":2541,"text":"the kind of things you want like you want to be able to say that your system will always be in this consistent state your","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2541s"},{"start_seconds":2549,"text":"your deposit contract is never going to lock up you're never going to lose these funds or so on and those aren't really like input","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2549s"},{"start_seconds":2556,"text":"checking a search those are a search of your system and like and if those are violated if it's your system is probably designed around those always holding","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2556s"},{"start_seconds":2565,"text":"and if those are suddenly violated are you sure that you know you have the correct fallbacks for that um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2565s"},{"start_seconds":2573,"text":"and i mean and i mean if that's all you take with you like oh i'm gonna i'm gonna if you want to say i'm gonna show those those uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2573s"},{"start_seconds":2581,"text":"former verification engineers that i don't need them and i'm gonna write a search and i'm gonna say well if this invariant is ever violated we're gonna call the fallback function","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2581s"},{"start_seconds":2589,"text":"and all our things are going to be liquidated and everyone's going to be reimbursed then great like you've added some great some great","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2589s"},{"start_seconds":2596,"text":"um panic handling basically but you did that by trying to like think what are the variants i expect to always hold where can they","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2596s"},{"start_seconds":2605,"text":"be violated am i sure that i can handle them correctly because that's the kind of thing a verification engineer would find like you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2605s"},{"start_seconds":2612,"text":"you assume that this would always hold well it won't hold in this case you say okay but if in that case i'm going to deal with it like this and that's great now we have better","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2612s"},{"start_seconds":2619,"text":"software um yeah and and actually in this regard i have like related questions","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2619s"},{"start_seconds":2626,"text":"because uh one of the like uh i'm a practical engineer in the sense that i","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2626s"},{"start_seconds":2634,"text":"uh i did look for various like complex systems and uh it showed that there are like two very","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2634s"},{"start_seconds":2642,"text":"powerful practical techniques for verification one is the sword which i mentioned and and other is some form of a virtual machine because","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2642s"},{"start_seconds":2650,"text":"because you can put some invariant checking actually into into your execution","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2650s"},{"start_seconds":2656,"text":"uh engine for example things like a for jvm","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2656s"},{"start_seconds":2663,"text":"there is a form of formal verification of of stack manipulat manipulation correctness for example so","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2663s"},{"start_seconds":2671,"text":"so that like it's a stack machine so when you when you put values on on stack and from stack you essentially ensure that stack","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2671s"},{"start_seconds":2680,"text":"is balanced and properly typed and uh similar thing exists in in many other","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2680s"},{"start_seconds":2687,"text":"virtual machines so um so some some invariants could be checked","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2687s"},{"start_seconds":2694,"text":"and insured by uh by the virtual machine so uh so what uh what do you think of formal verification could bring","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2694s"},{"start_seconds":2701,"text":"to the virtual machine for example if we have like wasn't virtual machine do you think there could be something uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2701s"},{"start_seconds":2709,"text":"which we could add to this virtual machine to execute smart contracts in a safer way","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2709s"},{"start_seconds":2717,"text":"um i mean what you're talking about i mean if i understand it correctly this sounds like runtime monitoring like checking that you know uh certain things","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2717s"},{"start_seconds":2726,"text":"like checking at runtime that things always work and maybe like executing this exercising the system and running a lot of things and making","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2726s"},{"start_seconds":2734,"text":"sure that things always work is is that correct it's not exactly continuous","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2734s"},{"start_seconds":2742,"text":"no no for example if you look at the john virtual machine uh it has a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2742s"},{"start_seconds":2749,"text":"bytecode verification but verification is essentially uh before executing the the code","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2749s"},{"start_seconds":2757,"text":"the bytecode you check that the the manipulations with stack uh are correct correctly like balanced","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2757s"},{"start_seconds":2764,"text":"and so on and uh uh and and so uh there are other chats like uh memory","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2764s"},{"start_seconds":2773,"text":"manager in this in a sense is is something which helps perform modification because it ensures that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2773s"},{"start_seconds":2781,"text":"objects for which the reference being held are not actually disposed which could happen in language like a c or c plus plot","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2781s"},{"start_seconds":2789,"text":"uh and i mean so this web assembly has four more things yes","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2789s"},{"start_seconds":2799,"text":"yeah and i mean and i mean those are kind those are properties that are super good to verify and are actually also kind of","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2799s"},{"start_seconds":2806,"text":"relatively easy to verify again they're decidable you can say that these uh you can just look","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2806s"},{"start_seconds":2813,"text":"at a a sequence of um jvm um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2813s"},{"start_seconds":2820,"text":"uh jvm bytes and say okay these are not going to violate you know yeah","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2820s"},{"start_seconds":2827,"text":"cause stack underflow for example and that's because it's a decilable property and it's also you know it's well known","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2827s"},{"start_seconds":2835,"text":"that that's something you can do if you just design your language correctly uh but some things are not decidable and especially like if you're","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2835s"},{"start_seconds":2843,"text":"if you're an engineer writing writing contracts it's very hard to design a general process","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2843s"},{"start_seconds":2851,"text":"that is going to check some meaningful property of every proper possible program you can you can construct","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2851s"},{"start_seconds":2858,"text":"i mean essentially like formal verification is you know applying applying all these formal methods to things that are","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2858s"},{"start_seconds":2866,"text":"not easy or rather i mean the thing you're describing is also sort of formal verification but it's the kind we take for granted it's the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2866s"},{"start_seconds":2873,"text":"same way we take um type checking for granted it's something we know how to do there's nothing we can do well it's something most people will be familiar with and therefore we","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2873s"},{"start_seconds":2881,"text":"do it obviously um there is no real such process for uh checking these kind of","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2881s"},{"start_seconds":2890,"text":"specifications of a token contract if there were we would just apply them and every every uh program on the evm or the near","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2890s"},{"start_seconds":2899,"text":"virtual machine would you know be guaranteed to satisfy these properties but since we don't have that we","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2899s"},{"start_seconds":2908,"text":"need to do whatever we can and that's usually takes some human ingenuity and in 30 years in 30 years we're going to have","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2908s"},{"start_seconds":2916,"text":"a lot of cool new decision procedures to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2916s"},{"start_seconds":2920,"text":"automatically verify a bunch of things that we think are important for smart contracts but right now you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2920s"},{"start_seconds":2928,"text":"no one's thought of them yet so what you're describing are a bunch of properties that are very important to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2928s"},{"start_seconds":2935,"text":"verify but there are other properties that are important to verify","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2935s"},{"start_seconds":2942,"text":"that are not as easy it's not like the the in in algorithms like i mean there's a bunch of algorithms there's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2942s"},{"start_seconds":2950,"text":"there's p and mp like there's a bunch of things that are easy to do uh and there's a bunch of things that are not easy to do but the things that are not easy to do might still be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2950s"},{"start_seconds":2958,"text":"important therefore we're applying our ingenuity to try to solve the best as we can even though we know that there are some","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2958s"},{"start_seconds":2965,"text":"or okay we don't know but even though we assume we think that there are some basic limitations to how how well we can do it we still want to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2965s"},{"start_seconds":2974,"text":"do it so even though we don't we know that there is no decision procedure for whether a program halts we want to be as good as possible","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2974s"},{"start_seconds":2981,"text":"in detecting halting and we want to be as good as an automatic as possible in detecting important properties of smart contracts","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2981s"},{"start_seconds":2989,"text":"and when they're violated and when they're satisfied and that's sort of where the research is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2989s"},{"start_seconds":2996,"text":"happening yeah yeah that's that's absolutely correct i just","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=2996s"},{"start_seconds":3003,"text":"uh just wanted to like uh understand the practical uh consequences","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3003s"},{"start_seconds":3010,"text":"of uh formal verification for uh for engineers so what would be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3010s"},{"start_seconds":3018,"text":"uh the best practices i guess we we can understand one of the best processes which which is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3018s"},{"start_seconds":3025,"text":"uh asserting uh other probably would be uh adding more checks uh into into vm but","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3025s"},{"start_seconds":3032,"text":"uh um that's as as you said it's it's on the lower level so it's it's less on the semantic layer","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3032s"},{"start_seconds":3039,"text":"and more on like on just execution engine layer and and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3039s"},{"start_seconds":3046,"text":"so if we talk about uh like semantic related or formal gratification so what would you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3046s"},{"start_seconds":3054,"text":"recommend people to do here essentially how to other than think about the before the program which is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3054s"},{"start_seconds":3062,"text":"probably very valuable suggestion but still um it's hard to do in general it's sort","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3062s"},{"start_seconds":3070,"text":"of like saying you know what are the principles you should adhere to to make good software i mean it depends on what software you're building if you're building a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3070s"},{"start_seconds":3078,"text":"website or you're building a a nuclear missile launch system you have different practices um and there are some things that are","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3078s"},{"start_seconds":3086,"text":"you know obviously always good like you know document your stuff and think through things","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3086s"},{"start_seconds":3092,"text":"um and i think it comes down to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3092s"},{"start_seconds":3101,"text":"being clever like i mean that's you know keep it simple stupid principle like i mean if you want to do something really really clever","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3101s"},{"start_seconds":3110,"text":"uh something that optimizes something in a really smart way but it's that is not obvious","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3110s"},{"start_seconds":3117,"text":"you need to convince yourself and ideally convince someone else that this holds so i mean code review is a great example i mean","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3117s"},{"start_seconds":3126,"text":"if you if you make sure you do good code and honest code review like people actually don't just you know let your stuff go through like people actually","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3126s"},{"start_seconds":3133,"text":"say i'm not sure this works can you show me and convince me 100 that it works if you can convince them and you just","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3133s"},{"start_seconds":3140,"text":"like write that down in a comment or in a document somewhere uh then you know you're i mean you're","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3140s"},{"start_seconds":3148,"text":"essentially doing formal verification on paper if you if you can write i mean mathematics is essentially writing convincing","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3148s"},{"start_seconds":3155,"text":"enough stuff um but also you know try to convince i i think we often stop in this place where okay","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3155s"},{"start_seconds":3162,"text":"it's probably true and i can't i can't think of any way this would not work um whereas of course verification deals with the problem of","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3162s"},{"start_seconds":3170,"text":"like am i 100 sure this can never be violated um so but i mean","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3170s"},{"start_seconds":3177,"text":"and then i mean i also think one shouldn't be too hung up on formal verification as like you know the holy grail either i mean there are all kinds of","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3177s"},{"start_seconds":3186,"text":"things that are in between i mean in essence you have like uh let me let me grab the whiteboard again uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3186s"},{"start_seconds":3195,"text":"you're gonna have this uh let's do an arrow oh it's very laggy sorry let's see","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3195s"},{"start_seconds":3204,"text":"uh that's a bad arrow like more and more","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3204s"},{"start_seconds":3211,"text":"better verification uh and i mean if you do testing if you write unit tests","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3211s"},{"start_seconds":3219,"text":"and integration tests and everything great you've you've taken a step in the right direction right um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3219s"},{"start_seconds":3227,"text":"and if you do um like runtime monitoring","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3227s"},{"start_seconds":3234,"text":"or like you know you know you're always checking at runtime that things are working properly","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3234s"},{"start_seconds":3241,"text":"uh that's a step in the right direction and there there's all these things that happen on this scale and i'd say where the more formal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3241s"},{"start_seconds":3251,"text":"verification stuff starts is things like uh bounded symbolic model checking","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3251s"},{"start_seconds":3262,"text":"and say um symbolic execution like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3262s"},{"start_seconds":3272,"text":"uh you you find a symbolic execution engine and run your program on different inputs and try to verify things","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3272s"},{"start_seconds":3279,"text":"or use you know state-of-the-art tools there's every step to the right is probably an","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3279s"},{"start_seconds":3288,"text":"improvement but i think we tend to get stuck in testing and then this fluffy thing","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3288s"},{"start_seconds":3297,"text":"which is you know just oh hang on this is not going well uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3297s"},{"start_seconds":3304,"text":"here we go this fluffy thing which is hard to place on the scale which is auditing right that's someone","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3304s"},{"start_seconds":3312,"text":"looking at things and saying oh this probably works and this falls best practice um i mean one thing we're working on is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3312s"},{"start_seconds":3319,"text":"trying to make a tool called firefly which focuses very much on um using the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3319s"},{"start_seconds":3327,"text":"existing test suite like your your existing program test suite and our formal methods to find","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3327s"},{"start_seconds":3334,"text":"make sure that you know you've exercised every branch in your on the bytecode level and we can also use those","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3334s"},{"start_seconds":3342,"text":"that testing to do symbolic execution and check for properties getting violated and you can write like invariants of your","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3342s"},{"start_seconds":3350,"text":"system like saying your my system should never violate this property and then we can have that invariant and we're going to keep it with us","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3350s"},{"start_seconds":3357,"text":"as we are running your test suite and we're going to make sure that that always holds so essentially your tests we did not is not","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3357s"},{"start_seconds":3364,"text":"only testing the things that is that it's supposed to test in a sense it's also uh making sure at all times that all","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3364s"},{"start_seconds":3374,"text":"your systems variants are not violated and i think it's important to not not get stuck in like full formal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3374s"},{"start_seconds":3382,"text":"verification because full form modification is valuable but it's also harder than these other techniques","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3382s"},{"start_seconds":3389,"text":"and it's therefore right now it's sort of reserved for the most important things the things that can absolutely never go wrong","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3389s"},{"start_seconds":3398,"text":"uh like you know the beacon chain contract on ethereum like making sure that you know that is going to work and making sure that whole certain properties hold of it uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3398s"},{"start_seconds":3407,"text":"that's a good place to employ for more verification if you have the the tools and the means but it's not going to work for everyone at","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3407s"},{"start_seconds":3415,"text":"all times yeah could it give like an example how um because this sounds uh like a super cool idea","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3415s"},{"start_seconds":3423,"text":"to uh to what you just described to uh to actually take tests and like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3423s"},{"start_seconds":3430,"text":"uh essentially uh do like factorize it in a sense so instead instead of","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3430s"},{"start_seconds":3437,"text":"of actual uh values used in tests just use equivalence classes","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3437s"},{"start_seconds":3444,"text":"of of the text which which leads to like the same or different uh program behavior","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3444s"},{"start_seconds":3451,"text":"uh could you please explain how how it uh how it works in in the file","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3451s"},{"start_seconds":3460,"text":"so i i'm not sure i understand the question you're saying how the how you can automatically generate tests or how","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3460s"},{"start_seconds":3468,"text":"um now how how could you like translate test from the actual execution to symbolic execution i think","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3468s"},{"start_seconds":3476,"text":"if i understand what you described here you you essentially use use a test as an input to symbolic execution","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3476s"},{"start_seconds":3485,"text":"uh engine so that you kind of understand what's what's going on yeah okay yeah so i i don't i don't work on","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3485s"},{"start_seconds":3493,"text":"firefly so i don't pretend to be an expert on this but the way i understand it is that what you do is you have uh we just have a specific contract","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3493s"},{"start_seconds":3502,"text":"uh and if you are calling that within firefly we're going to catch that and give you a symbolic value back or initially we're going to give you a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3502s"},{"start_seconds":3510,"text":"random value back just so you can do some random testing but then we might also give you a symbolic value back but if you run the same test in say","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3510s"},{"start_seconds":3518,"text":"ganache then uh it's just going to give you a specific number at all times or maybe a random number","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3518s"},{"start_seconds":3526,"text":"so the way the way the way i think firefly does is is like you ask for a random value from a specific point and if firefly","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3526s"},{"start_seconds":3534,"text":"sees you doing that that it's gonna uh turn that into symbolic value if i understand correctly um so essentially like you're you have","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3534s"},{"start_seconds":3543,"text":"to write your tests and or like you write your tests as a property-based test like a randomized test uh and then i don't think this f","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3543s"},{"start_seconds":3552,"text":"uh feature is fully implemented but in the future uh we're gonna turn that into a symbolic or we can turn in a symbolic value for","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3552s"},{"start_seconds":3559,"text":"example but i mean so i mean it's it's it's all just standard like you know programming tricks using hooks and you know checking work","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3559s"},{"start_seconds":3567,"text":"which environment you're in and um so i mean formal verification is just it's very similar to programming i've i i identify myself as like a software","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3567s"},{"start_seconds":3576,"text":"engineer day-to-day because like it doesn't feel that different it's just working on a slightly different domain","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3576s"},{"start_seconds":3582,"text":"it's like i'm building the tools to help specific development work um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3582s"},{"start_seconds":3590,"text":"and it's and i'm just doing it in a specific special language that has some neat features","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3590s"},{"start_seconds":3597,"text":"um so i mean i i don't i i think it's important i know that formal verification doesn't get stuck in","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3597s"},{"start_seconds":3605,"text":"an ivory tower of like you know i i know i talk in very abstract terms sometimes because i want to make sure i don't i i","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3605s"},{"start_seconds":3612,"text":"stay correct and don't say things that are like probably wrong but uh i think i mean a problem with formal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3612s"},{"start_seconds":3620,"text":"verification sometimes is that it can be a bit too abstract and i think what we're doing what i like to do is just you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3620s"},{"start_seconds":3628,"text":"show the tools i'm working on and say like hey here's what this can do and it it looks like you're doing functional programming which is","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3628s"},{"start_seconds":3635,"text":"probably not that scary and it's something you probably should do like just kind of putting it in the hands of people and making sure like i said that people start thinking","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3635s"},{"start_seconds":3644,"text":"about uh oh i wanna i wanna prove something and then you start by saying oh what is you wanna prove right because people often","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3644s"},{"start_seconds":3652,"text":"come and say oh can you prove i just to prove that my contract is correct and then you asked have to ask well what does that mean what does it mean for your contract to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3652s"},{"start_seconds":3660,"text":"be correct and like well half the time people don't really have like oh but you know i know what it's supposed to do well you know then it's doing what it's supposed","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3660s"},{"start_seconds":3668,"text":"to right i mean unless you have something written down that you can check it against um you can't really do verification and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3668s"},{"start_seconds":3676,"text":"unless you have that it's quite possible that you haven't fully thought through what your system is doing and it's also even more possible that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3676s"},{"start_seconds":3683,"text":"it's going to be hard for you to explain it to someone else so i have like um and this is a question here","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3683s"},{"start_seconds":3690,"text":"yes sorry nicole and that's also about the practical aspect so we talked about the financial","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3690s"},{"start_seconds":3698,"text":"contracts here right and uh you might have heard that many financial contracts were","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3698s"},{"start_seconds":3705,"text":"broken or abused not because um you know there was some bug in the code but because people were able to find a way","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3705s"},{"start_seconds":3713,"text":"to combine them somehow together or to do some manipulations on them in such a way that they at the end they come out profitable","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3713s"},{"start_seconds":3721,"text":"like or oracle manipulation and like with like flat phones for example yeah like flash flash loans like yeah whatever just like you know like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3721s"},{"start_seconds":3729,"text":"some temporal manipulation like you can you can like you know like jack up the price then then you know the dump it and all those","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3729s"},{"start_seconds":3737,"text":"kind of things right and call out some other contract and yeah manipulate the price ask you yeah and your thing like even without going you know like in","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3737s"},{"start_seconds":3745,"text":"those areas where we talk about the cross-contract you know interaction everything how would you go on with trying to prove that your","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3745s"},{"start_seconds":3754,"text":"contract cannot be financially manipulated in like in temporal way in such way that someone can somehow","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3754s"},{"start_seconds":3762,"text":"come out profitable at the end by just doing some a bunch of like atomic operations on your contract","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3762s"},{"start_seconds":3770,"text":"um well i mean always start with the simplest way of doing things and i mean the simplest way","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3770s"},{"start_seconds":3777,"text":"of doing things would probably not be you know to do full formal verification on all the code and all the contracts it would probably be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3777s"},{"start_seconds":3785,"text":"probably be something like uh set up a model like just a little graph of the different contracts how they interact","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3785s"},{"start_seconds":3793,"text":"and um like and and again like you have to come up with well","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3793s"},{"start_seconds":3800,"text":"like you said how do you make sure someone doesn't walk away profitable well how would you you have to come up with a way to specify that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3800s"},{"start_seconds":3808,"text":"and it kind of depends on exactly what you're trying to uh what you're trying to specify one thing you could say like for example i don't","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3808s"},{"start_seconds":3816,"text":"know these all these facts in like in the specifics but you say like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3816s"},{"start_seconds":3823,"text":"you want to prove that someone will not be able to manipulate the price of","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3823s"},{"start_seconds":3829,"text":"a uni-swap uh swap as their you know in the body of the code for example yeah i mean like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3829s"},{"start_seconds":3837,"text":"yeah sorry i mean like before we go into the details like the reason why i like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3837s"},{"start_seconds":3845,"text":"express this concern because it sounded like to me at least it should be intuitively really easy to formalize something you know like like something","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3845s"},{"start_seconds":3853,"text":"like a property of like some energy preservation thing where you say like something that we're trying to talk about uh which is like you cannot mint or or like your total","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3853s"},{"start_seconds":3862,"text":"supply stays the same something in in the lines of you know whoever interacts with the contract loses took the gas","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3862s"},{"start_seconds":3870,"text":"or like always you know it it's it's more like you know like some some law of thermodynamics he interact with the contract","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3870s"},{"start_seconds":3878,"text":"you always come out you know at least losing the assets for the gas okay and it's and like in the direction you're going with","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3878s"},{"start_seconds":3885,"text":"is is trying to say like well uh trying to formalize is too abstract so you need to express more specifically what are the properties","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3885s"},{"start_seconds":3893,"text":"in there and then try to for like to prove formally that they they hold well well i'm saying can we can we come up with some set of like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3893s"},{"start_seconds":3901,"text":"almost like a laws of thermodynamics but for the financial contracts that we can formulate overall for all financial contracts and then just run","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3901s"},{"start_seconds":3910,"text":"verification independently what is the body of the contract is uh that's a really cool idea um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3910s"},{"start_seconds":3919,"text":"yeah i mean definitely get a committee on that just like trying to figure out what are like figure out the thermodynamics of financial contracts and you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3919s"},{"start_seconds":3928,"text":"make sure that i mean again since like you know i can publish a financial contract and it's term complete and you can do anything not all contracts are going to adhere to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3928s"},{"start_seconds":3935,"text":"it but we can at least put down you know some best practices saying like all these things should always be respected by any good um financial contract that would be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3935s"},{"start_seconds":3944,"text":"really cool i don't know what that would look like uh that would be really cool and it would i think definitely be amenable to um the formal","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3944s"},{"start_seconds":3953,"text":"verification one problem with smart contracts is that they like to call out to other contracts which is a good thing that's you know composability","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3953s"},{"start_seconds":3960,"text":"but it also means that you have to extend your assumptions to other contracts so you have to say like if you are doing","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3960s"},{"start_seconds":3969,"text":"if you're entering a specific function and that calls out to another contract and you want to make sure you don't violate the laws of thermodynamics","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3969s"},{"start_seconds":3977,"text":"you also have to assume that the other contract doesn't violate the laws of thermodynamics but what if your contract call can be pretty complex maybe like there's you know you're calling out a different","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3977s"},{"start_seconds":3985,"text":"contract and depending on you know the world state there are four different paths you can take and each one of those paths call out to a different contract","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3985s"},{"start_seconds":3992,"text":"all of a sudden like now you have like a pretty complex you might come up with a pretty complex system of interacting contracts","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3992s"},{"start_seconds":3999,"text":"um and and and of course you know users can define checks to say oh please call this contract","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=3999s"},{"start_seconds":4007,"text":"in in the in the course of all this and i think it in practice it can be hard to do that like at code level","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4007s"},{"start_seconds":4014,"text":"co-level verification um unless like we have all the code which we usually don't because you know often you can call arbitrary","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4014s"},{"start_seconds":4022,"text":"contracts it's usually not a white list that you can only call these um and that's why it's often good to model it in a more abstract sense like make an","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4022s"},{"start_seconds":4030,"text":"abstract model of the system as interacting interacting objects and so on and try to work it out from there and that's i mean you know","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4030s"},{"start_seconds":4038,"text":"definitely if you're if you come from physics or something then for complex adaptive systems then that's i think that's a","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4038s"},{"start_seconds":4046,"text":"great exercise but then you know it's it's also interesting how do you bridge that gap because oftentimes you do verification at like a protocol level or a systems level","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4046s"},{"start_seconds":4054,"text":"uh and well what i do is usually i do verification at like the code level and there's definitely room for error","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4054s"},{"start_seconds":4063,"text":"in in the gap between those uh where like you know you have some implicit assumptions in your in your big model and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4063s"},{"start_seconds":4072,"text":"those are slightly different in the code verification and you know that can be violated but basically you know if you if you're expressing your system","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4072s"},{"start_seconds":4080,"text":"in mathematical terms mathematical terms and doing some reasoning and proving things about your system you're doing formal verification and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4080s"},{"start_seconds":4090,"text":"that's i mean that's just the description of the the action and whether it's usually useful or not depends entirely what you're doing","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4090s"},{"start_seconds":4098,"text":"just like in math there are absolutely you can do things that are not very meaningful you can do things that are really really important like you can","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4098s"},{"start_seconds":4105,"text":"calculate you know the triangular theorems in graphs that don't really have a strong application or you","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4105s"},{"start_seconds":4112,"text":"can calculate you know the stability of bridges and uh you know security of","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4112s"},{"start_seconds":4119,"text":"financial systems and so on so actually i have very similar question to what marx had asked just","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4119s"},{"start_seconds":4127,"text":"just from another standpoint but exactly about exactly the same problem i mean uh if when you started","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4127s"},{"start_seconds":4134,"text":"talk about formal verification as essentially mathematical modeling i think humanity has very long","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4134s"},{"start_seconds":4143,"text":"experience of mathematical modelling and especially in area physics and in physics we quickly realized","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4143s"},{"start_seconds":4152,"text":"well uh in any physics like one of examples um i was thinking about like","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4152s"},{"start_seconds":4160,"text":"like uh like gas dynamic for example or thermodynamics as as max said it's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4160s"},{"start_seconds":4166,"text":"it's the same so you can in theory uh solve like a dynamic equations uh for every molecular in","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4166s"},{"start_seconds":4174,"text":"air to to to essentially make make a statement about uh uh like absolutely","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4174s"},{"start_seconds":4181,"text":"perfectly valid statements about uh about the air around you but that will be first uh absolutely","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4181s"},{"start_seconds":4189,"text":"understandable by a human uh who think about that and secondly it will be absolutely useless or you can say that it's like 25 degrees","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4189s"},{"start_seconds":4197,"text":"tells you in in this room and it will be like very simple statistic property which first makes sense and um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4197s"},{"start_seconds":4207,"text":"and relatively easy like measured and and computed so so my point is that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4207s"},{"start_seconds":4214,"text":"was exactly the same so from human point of view so if if you make a validation of very complex","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4214s"},{"start_seconds":4223,"text":"uh software models they became useless it's very easy to make to make a mistake it's not important how","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4223s"},{"start_seconds":4230,"text":"how smart is a particular person it just means that uh the like the complexity have to be like a little bit","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4230s"},{"start_seconds":4237,"text":"bigger and uh and and the brain will will break our brain is not that powerful","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4237s"},{"start_seconds":4244,"text":"technology and so we have we simplify and and like um the trick here is that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4244s"},{"start_seconds":4252,"text":"are there a way to not to not model or not even precisely model but quite the opposite uh uh to model in in a way which","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4252s"},{"start_seconds":4262,"text":"uh uh which avoids uh like the then they need to understand every behavioral aspect of the program","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4262s"},{"start_seconds":4270,"text":"right still be useful for yeah absolutely absolutely and i mean that's that's i mean if you're doing like protocol verification that's often what you're doing you just have actors","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4270s"},{"start_seconds":4278,"text":"that uh that way that's more more discrete deterministic thing uh but again like i'm not coming from","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4278s"},{"start_seconds":4286,"text":"the realm of physics and like if you get a committee together and decide to work out like a theory of thermodynamics for these kinds of systems","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4286s"},{"start_seconds":4294,"text":"and a way to model you know your smart or the smart contract platform um where you can like look look for pro","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4294s"},{"start_seconds":4303,"text":"these kinds of properties that would be really cool um i'm not like again i'm not it's not my area","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4303s"},{"start_seconds":4310,"text":"of expertise so i'm not 100 sure what the use cases would be i can i can imagine something like okay that would be","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4310s"},{"start_seconds":4317,"text":"that would be great like you know money you know value isn't destroyed anywhere for example or even if it moves around in interesting","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4317s"},{"start_seconds":4325,"text":"and complex ways it doesn't like go up in smoke or so on but uh all i can say that it's that it sounds really cool","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4325s"},{"start_seconds":4333,"text":"but uh and no i not but it sounds really cool and i hope you do it and get back to me when you do um but i also","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4333s"},{"start_seconds":4342,"text":"want to counter your point on saying like you know oh if you're trying to verify a system that's super it's super complex uh then you know the brain is going to explode because it's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4342s"},{"start_seconds":4350,"text":"so big and it's so hard i mean that that can be true but i mean verification one of the powers of verification is that you can","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4350s"},{"start_seconds":4358,"text":"ex you can have very complex systems that do a lot of tricky stuff and it's very hard to prove that they're right but the statement of correctness can still be quite","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4358s"},{"start_seconds":4367,"text":"simple like a famous example is the four color theorem um so basically the idea that any","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4367s"},{"start_seconds":4375,"text":"any world map or any possible word world map can be colored in using only four colors uh without having adjacent countries um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4375s"},{"start_seconds":4384,"text":"having the same color i mean that's that's the layman's statement the proof is immensely complex like super complex and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4384s"},{"start_seconds":4392,"text":"it's been verified with like you know proof assistance and but the thing is the thing is the","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4392s"},{"start_seconds":4400,"text":"statement is pretty straightforward and i i absolutely 100 believe the four caller theorem not because i can","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4400s"},{"start_seconds":4406,"text":"understand the proof but because i can understand at least somewhat the um","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4406s"},{"start_seconds":4414,"text":"the proof checker and someone says like i have a long string of you know that represents a proof we","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4414s"},{"start_seconds":4422,"text":"pass that through a very simple kernel that is a proof checker that only does like some very simple logic","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4422s"},{"start_seconds":4429,"text":"and won't allow you to do anything uh anything like obviously bad","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4429s"},{"start_seconds":4436,"text":"and it's going to say in the end oh yeah i've seen you've actually derived this simple thing you you here this is something that you have a simple statement and i can","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4436s"},{"start_seconds":4446,"text":"attest to that this complex body that is the proof actually proves this theorem and now we're done so i mean","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4446s"},{"start_seconds":4454,"text":"it and and your head doesn't have to explode around the theorem even though like the proof of course took like a huge amount of people and","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4454s"},{"start_seconds":4462,"text":"a lot of years to work out uh and i think that's one of the powers of verification because we often talk about how like the number of bugs","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4462s"},{"start_seconds":4472,"text":"in code scale with the number of lines of code and i'd say that you know the more","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4472s"},{"start_seconds":4479,"text":"complex your theorem statements are the easier it is to make a mistake if you have a lot of complex assumptions","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4479s"},{"start_seconds":4486,"text":"and complex encodings of states then it's going to be easy for you to make a mistake but oftentimes","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4486s"},{"start_seconds":4494,"text":"your your theorem statement can be quite small and the process of verification is often taking these more complex statements","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4494s"},{"start_seconds":4501,"text":"like for example we did here with the uh the transfer function i mean the statement the transfer function you know doesn't","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4501s"},{"start_seconds":4510,"text":"violate the loss of thermodynamics like the the amount of tokens stays constant or shrinks or whichever one we choose uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4510s"},{"start_seconds":4519,"text":"that's a simpler statement than saying every variable that is used somewhere in the body of the program has these properties at the input output","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4519s"},{"start_seconds":4528,"text":"that's a i'd say that's this the second statement of the problem leaves more room for error but you can use that to then","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4528s"},{"start_seconds":4535,"text":"prove the bigger theorem and i mean that's pretty common in mathematics you have like you have to","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4535s"},{"start_seconds":4543,"text":"if you're doing group theory like lagrange's theorem is really really easy to state and prove you can do it in a tweet but you have to create this more complex body of other","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4543s"},{"start_seconds":4551,"text":"things first but then the actual statement and the proof are pretty simple and i think that's one of the really cool things about verification is that","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4551s"},{"start_seconds":4559,"text":"you can kind of get this very high assurance because you have a very very small statement and you have i'd say absolute assurance","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4559s"},{"start_seconds":4567,"text":"that your statement is true um so yeah","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4567s"},{"start_seconds":4575,"text":"yeah i mean but in practice especially with smart contracts you often end up saying like you know well this is through given these and these assumptions because obviously it's","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4575s"},{"start_seconds":4582,"text":"a software system and this can be hard to encode these assumptions in an intuitive way yeah","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4582s"},{"start_seconds":4589,"text":"this sounds natural yeah so i guess we actually already like to 20 minutes before","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4589s"},{"start_seconds":4599,"text":"our like land deadline however uh i guess uh we have very interesting discussion i i personally","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4599s"},{"start_seconds":4607,"text":"truly truly enjoyed it and and like the ideas which we discussed here and so i","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4607s"},{"start_seconds":4614,"text":"want to say say thanks thanks a lot to eureka to to max","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4614s"},{"start_seconds":4621,"text":"for for like for for joining this this talk and and so maybe","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4621s"},{"start_seconds":4628,"text":"uh we can we can continue discussing uh this uh this manners","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4628s"},{"start_seconds":4635,"text":"in matters in","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4635s"},{"start_seconds":4639,"text":"in some in some other format uh because because it seems to be very very deep and very","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4639s"},{"start_seconds":4646,"text":"uh they say uh uh strangely it's very practical in a sense because because what we do we","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4646s"},{"start_seconds":4654,"text":"we we all write a complex system and we and we regularly and routinely verify them so so","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4654s"},{"start_seconds":4661,"text":"probably discussing it with uh","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4661s"},{"start_seconds":4665,"text":"from more like a distant point of view maybe very uh very enlightening for any software","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4665s"},{"start_seconds":4673,"text":"engineer so thank you a lot thank you so much it was uh fun all","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4673s"},{"start_seconds":4682,"text":"right see ya thanks around for listening","url":"https://www.youtube.com/watch?v=SWtAwPPBGoI&t=4682s"}],"youtube_url":"https://youtube.com/watch?v=SWtAwPPBGoI","url":"https://near-pedia.xyz/videos/SWtAwPPBGoI"}