# Formal Verification of Smart Contracts Made Easy (Devcon5)

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 1:11:00
- Topics: blockchain, smart contracts, distributed ledger, ethereum
- Watch: https://streameth.org/watch/yt-tq5XH3JedqM
- YouTube: https://www.youtube.com/watch?v=tq5XH3JedqM

## Description

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more.
https://archive.devcon.org/archive/watch/5/formal-verification-of-smart-contracts-made-easy

In this hands-on workshop, we will go through the process of formally verifying smart contracts. The attendees will learn (1) how to formally specify relevant functional requirements of Ethereum contracts, such as "the sum of deposits never exceeds the contract’s balance", and (2) how to verify these using existing analysis tools for Ethereum.
First, we will show how to formally specify the intended behavior of smart contracts. We will look closer at safety temporal properties, an expressive class of properties for capturing which sequences of contract states are considered correct. We will present common requirement idioms, including access control, state-based properties, multi-contract invariants, and others.
Next, we will provide an overview of existing testing tools, such as tools based on symbolic execution and fuzzers. The goal is to understand how they can be used to identify violations of the formalized properties as well as their limitations in providing unbounded formal guarantees.
Finally, we will learn how formal verifiers go beyond testing and can provide unbounded formal guarantees (for any sequence of transactions). We will take a closer look at the specification language used by VerX and its automated verification method, which is easy to use and does not require in-depth knowledge in formal verification.

Speaker(s): Dimitar Dimitrov, Anton Permenev, Hubert Ritzdorf, Petar Tsankov
Skill level: intermediate
Track: Security
Keywords: technical

Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum
Learn more about devcon: https://www.devcon.org/
Learn more about ethereum: https://ethereum.org/ 

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. 
Devcon 5 was held in Osaka, Japan on Oct 8 - 11, 2019.
Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/

## Transcript

[Applause] as everyone for coming who have now a workshop on the form of replication of smart contracts and maybe before even typical of topic so how many people have done any for modification of contract so far maybe this raise the hands so very few so I guess all the remaining ones will attract it by the last part that's supposed to be easy and hopefully by the end of this workshop everybody manages to have a hands-on depends on exercise and everybody should be able to verify some form of properties on contracts so the people who peed in the workshop we have Demeter there his previous student it is during a joining chain security now parents demand for modification and problem analysis then we have also hunter permanent so he is the lead developer of the very far we'll be using today in the workshop and also who were visiting back there city of chain security and myself as well so who we are we are a chain security we are a spinoff from ETH Zurich ETH the University not the foundation based in Zurich Switzerland and we focus on the objects activity we have worked with many blockchain projects so far we can them over 80 audits not only smart contract always but also product of all its platform on itself as far as a cup of very visible ie IDs I think many people are recognized the chain security name from you know some of those earpieces we have reviewed in the past and so yeah we also have quite a few already security products with platforms at the CTO Foundation polkadots silica and fewer than some chains where we focus on building security tools you know tools for finding boxes no enfant as far as for modification tools for for these platforms all right so it's part to the work we have done quite a couple of systems so far so I have listed some of those some of them on this light here and so this is the name to achieve different goals we typically combine techniques from various different domains such as tactical asset dynamic analysis we also use quite a lot of fun everybody thinks of machine learning to to you know to build these systems so some of you are familiar with the Sakura fight this was the first system that were built back in 2017 it's a system for finding generic on the abilities in smart contracts and yeah so that's was basically addressing all these puzzles were popping up regularly every couple of weeks in 2017 in all these you know parity walnuts and many other contracts so this is what that system was addressing and so this system along with other system I think they made a difference in the sense of 2018 we will actually so much fewer facts because of such generic like really simple boxing contracts so another system we have builds is with every wedding system that addresses the problem of ensuring functional correctness so we're going to talk a little bit more about what functional corrective correctness actually means and we have fuzzing system that essentially generates transactions and tries to find violations of the specific security properties that we're trying to to check for or for a small conference and the main system that we will be talking about today is the direct system which is the first automated verify for for verifying smart contracts this we have a demo on variance of CH we have some few other instances of this system that's one for the exercise later today and for people that are interested really in depth on how that system works what guarantees it provides so we also have a research paper which will appear at the to Boise possible security and privacy so that's one of the main security conferences one of the main academic security conferences so if you go on our webpage chase younits.com I go to research you can download the PDF and read all the details about the verification technique that is being used in that system alright so before we actually do I you know go into the hands-on exercises it's important also to mention why are we actually doing this and the main reason is that I mean where they initialize how many people have verified contracts I think they worked about two three hands and the reason this is is that you know thermo replication used to be this very difficult time-consuming task or you have to be really an expert in formal verification have a PhD in logics and so on to to to prove that a contract is correct and if we are to make form of ratification mainstream you know a lot of developers also adopting that approach then you have to be building a system we have to be building systems that allow people without this background to write functional specifications and prove the contracts correct and that's exactly what this very very very far aims to do so it eliminates this nest needs to know in-depth knowledge of form of verification and takes down this reduces also significantly vacation time because I suppose it's really not a very hard task to to verify contracts with such systems so we said a system if you take something like a standard ear seat when it's open which will look in-depth in the exercise you can literally no formal ratification for all the main properties you will care about a token you know in a matter of a couple of hours that we done with with the ratification ever visit here some of us some someone that we have verified we have more on our main webpage a spirit of calm / audits or you can find some of some of these reports where we have done proper verification of those all right so the workshop will continue as follows so we'll start with some very more high-level introduction to what functional correctness means and why is it challenging to formally verified properties with functional properties and what are different techniques that different tools are introduced in that space what's called a different person guarantees today so also will cover here of course that the correct system and then in the second half you'll switch to a hands-on exercise where Demeter will talk walk you through how do we specify properties and verify them with with a verifiable Eric's and so we've also about many other people from the chain security team back there so they will be assisting you while doing this exercise and then in the last part depending on time we'll try to get into some more detail about the actual verification methods and how this is being automated by the various verifier alright so let's get started and functional correctness so what is functional correctly so usually when people think about security tools they're these kind of tools where you just paste the codes and then they show you a bunch of on the business that founds so this is not what we're talking about here so we're not looking for more dynamic movement were talking about functional correctness and what this means is that whether the problem of functional correctness has two parts so honest you have this hard culture that you want to prove that if you wanna you want to make sure it's correct and then the second piece of information that you need is the functional specification of a smart contract so a function specification is that this is the thing that this defines what is what is the intended correct behavior of that smart contracts okay so to make this a little bit more country's here on the Left imagine you have a smart contracts that typical year z22 so you have all these terminals that balances total supply order a couple of functions that allow users to to transact with the contracts and then the functional specification typically consists of requirements such as the seventh caller balances equals the total supply okay so don't even this specification says that all the tokens are assigned to users somehow there are no missing tokens on the side to know about the sign to end user another common example is that often tokens are immiscible meaning that you can increase initial more tokens and often you wanna show not only certain users can exercise its functionality and if you want to make sure that if the total supply increases then that was triggered by a transaction issued by the owner of the contracts okay and then typically you would have a huge list of those requirements that you would have to you would have to check that whatever the implementation of these functions is it is indirect with respect to these functional requirements okay so technically how does how do we actually check that the the code is correct and they're roughly speaking two steps so the first step is well to essentially transform this English description of correct behavior into something that's to take them down and to specify them at the level of the source code okay so for instance if we take the first requirement that says that the server balances has to be power supply then this is written in the specification language that we'll be using later and exercises of the very excess specification language and this is how it will look in the actual specification language so fairly intuitive they'll succeed some keywords onto the mapping that we're trying to sell and then we have a quality with the focus of okay last that number one is inevitable you know you have to be able to transfer formally state what the property means and once we have formalize it then if we have a particular state of the smart contracts then we can check the whether this property holds or not alright so for instance if we look at a state where we have two users having balanced 50h and we have total supply one other than the property holds with us that's what it says and here would be an example where the property down the hall because this sum of these two balances actually exceeds the total balance specified in the contract et cetera so a step number one define the property step number two is to actually check that this property holds for all possible states that your contract could reach okay now what does this again technically mean well once you deploy the smart contracts on the blockchain it is always initialized by the deployment speed so it will end up in being some specific initial space so that's what these days and you would have to make sure the property goes there so for instance you deploy and for that initial state the sum of balances would have to be equal to the total supply okay that's one thing the next thing is that once deployed the users could send consent a transaction to the smart contracts and each transaction would modify the state of the smart contracts so they can for example with submit a mean transaction with different you know different policy s arguments and so on and let's be a little bit more precise what these arrows and boxes here represents so what these boxes represents is the actual state of the contract and the are started I'm triggered by the transactions submitted by the users and how are how is our disposition defined this is defined by the implementation of the of the functions in the contracts so for example if we have here we start from a state where total supplies of hundreds we have an older user with address extend and then we have two users with balances 50 tokens each and then main function is defined such that it would increment the total supply by the number of dollars water two means and then it would assign the new totals to the to the owner of the contract so here if we have this means one fiblets tokens issued by the user base bill the normal supply will be incremented as defined by the function and then the balance of the owner who has addresses euro extent would be incremented from 52 also number because that's how many additional conservation so that's what this allows you me alright so here comes immediately the first immediate challenge when you talk about functional correctness is that even if we want to consider whether the property will hold after one single transaction after the first transactions entered a contract that already gives you so many different ones actually to put that would be the test to be accounted for that it becomes infeasible to put foresee it's not possible to another these transactions into actually check them in all these things the property will always cause and challenge number one and we cannot stop here because after the first transaction is the user would submit second and third and so on transaction and in fact there's not lots of predefined bounds on how many transactions this contract would process in his lifetime so to consider number of transactions you were to formally verify that this property would always hold their two fundamental Chinese heroes all right so let's very quickly go over what are different techniques that could be used to address this problem of taking these formal properties and how they different types of guarantees and so I ordered a based on reliability so starting from least reliable going towards more more reliable techniques well the bottom we have the menu reviews always the human can look at the codes understand what it does and try to find violations so this is a successive penetration testing property try to try to crack the contracts and the disadvantage here fairly well and also it's a time consuming problem even if you have especially we have big contracts that would take a while for for the security expert to understand exactly how these things how of the functionality of the contract is then let's move over to model 26 so next level would be to do some form of automated testing and then primarily in general for software but also in the space of contracts two techniques for testing contract so one is based on fuzzing and the second major technique is to special support execution so let's briefly see what this what what these techniques would do to this problem of objective functional practice and so starting for fun with fuzzy here's basically what's happening so fuzzing is a testing technique or a puzzler would generate random transactions and then it will execute the transaction some of the contracts and by doing so the buzzer would observe different states of the smart contracts all right and by doing so we can for all the states that have been observed after posting these transactions that we generate we could check whether the property is violated or not if it happens as we reach a state where you get a violation then the father would also return that sequence of transaction that triggered the violation and the developer could see you know reproduce the buck and try to fix it there are many many fathers have been deployed that are available online to do exactly this this thing the Challenger typical is how to generate transactions in a smart way so you get verified coverage over at least a very high code coverage over the contract which is already pretty challenging in contracts which tend to be very stateful and complex preconditions of the transactions and so on so what's funny was no idiot would not give you this full guarantee that's why it's a testing technique because in every time there will be some states that you would not not observe simply because the puzzle did not generate that specific sequence of transaction that would transition the contract to the states so it's a testing technique essentially now symbolic execution that's something different symbolic easy techniques that it is based on this symbolically special technique it simply would not scale to reason about such depth of transaction so typically if you the symbolic symbolic to you would give it as a mouse so it would run for maybe thirty minutes one hour and then you would stop and then it would reach certain level so it is better at this kind of breath exploration and but if the bugs are hidden deeper like after five ten transactions which could happen even in simple contracts across cells were you have to transition to example two some refund face where you exercise it on three week on functionality so this typically tend to be somewhere lower that are harder to explore with similar tools so I have listed here some other open tools that are available that's to do this okay it is clear so far if there any questions just raise your hand you can also go to this point itself all right so that's the best thing and then the highest level would be the formal verification what this workshop would be about and this is really the point where you have a slip from testing to for verification meaning that you could actually prove this property for whatever sequence of transactions we would make it would always holds no matter what okay measure difficult happens at that point all right now so let me show you what this means is that you cover all possible states essentially and if you will check out of them and if you check mark all of them you grab this for guarantee right so that's what the variant system does and you will be losing its own and the input system is as we solves the smart contracts as well as the specification because we're dealing with functional characters here and the main thing of that what the making of verax does is it it's fully automate this process of fully optimize the process of verifying in the sensors it's if it's successful it verifies the property it can down give guarantees a is for it is fully verified and if it fails to verify the property then it doesn't give a guarantee whether the property does well they're not so it could be like you have to help a little bit to actually verify the property or it cook another property is valid and then you have to pick the contracts so we'll see some example so now sighs later all right so to give you a bit of something that we actually spent quite some time is to ensure that verax has a very intuitive and easy-to-use facilitation language because that typically is one of the bottleneck when we talk about functional correctness is again to use functional correctness in addition to the contract you have to write down what the contract is supposed to do and if this is very hard and tedious of specifying you you know you will end up not not really using the system so I will get a few examples of specifications that we have seen to very frequently appear in real world smart contracts so this is something we just observe doing audits and verifying contracts and so this is a this is literally what the specifications are so you don't have to write some elaborate scripts or something very complicated to formally state of property so common properties are things like access control or you wanna ensure that certain functions can be involved by particular users is he saying that in always in the contract if there was a transaction to deposits then that was that transaction was made by the owner of the contracts another common party that we observe is that very often it's not about who is sending a transaction but it won't in universe states the contract is so for instance here we say that if the current time exceeds the refund time by a week and users are never no longer allowed to submit refund transactions yes state machine properties is as well so again contracts are very stateful there's explicit state variables that define how the states how the contract in addition to the different states so you have to make sure that these transitions are implemented correctly in the contracts we saw an example earlier I suppose so we have some over basically aggregations over mappings in a race now also tend to be pretty common so that's we have at least explicit keywords in the language to allow users to to run these properties and another common pattern is that so typically we have a project it's not implement the full production of our contractors in several contracts and often there are certain invariants that software dependencies that are exists between the contracts and their properties that's capture these dependencies we have to verify that they are implemented correctly in the conference ok so again you will be writing some of these so these specification so a bit more technically four he went the cinematics of the specification level is actually based on something on a fragment of that product which is very well that it's a specification language if you go back take the case of research in this soit is very well understood complexities and expressivity and so on alright so I want to depth on how how the verifier actually works but in 30 bit combines two techniques one technique is it does use this symbolic execution technique which is very good at handling dealing with many different I contribute you submitting transactions and then to deal with the unfounded depth that users will use something called predictive abstraction that allows it to fully capture all the possible that is very large unbounded three to capture it with some finite representation so the plane equal time we may get you know it's more details about that disease alright so that's what the fellow intro and now we're going to transition into the actual exercise on how to use vericsson to specify these properties so hand over to me to introduce an example uses yes okay amico yes and now we can here with a small exercise to use Ebonics by the way if you have any questions at any time this raise your hand and we can ask the questions the goal here is to make the exercise more inter and not so careful okay so so the first step in proper verification is to actually specify the properties informally this means that we specified any natural language whether it's English or some other language you just need to have some clarity over what's this smart contrapposto right and in this exercise we'll look at two main confidence what is your C 20 okay the other is kind of standard ground zero of course simplified because we don't have too much time okay so first we'll go over specifying functional requirements informal right and we we go this is fragmented of your C 20 interface for those who are not so familiar with the contract si si dimensions one is total supply how many tokens are in circulation the average gamma so you can put in how much tokens given others or accountants and the actual main function here is the transfer function with well descended of the transaction right can transfer some tokens from its own account to the recipient so we have the other service recipients account and self amount affected or any tokens sorry not that these tokens add water that's right and now whenever we are specifying behavior of contracts we do it over the contract and not over the interface so here at the relevant parts of the actual contract right so the functions we have the balance the total supply and Varmus become fields in the copy right so these are not private field search total supply l mapping which says for every other issue account how many tokens these others possesses right so this one is new and which is among others right and here we have some specification pension transfer now when we're thinking about the context of this specifying its its brightness me at least as abrasive belt when I am doing this piece I never looked it into the implementation right so for me the contact is a black box and that's why I specifically omitted the body of the transformation hey Cheryl ago is to just come up with a couple of properties hopefully food center properties that specified the core behavior of people okay good so let's do this a little bit more interactive first properties on me right so we already saw in our tree it says GC formally in English of course my always equals simple powers right so these pans services specifies an invariance will invent me that the holds of all states and we are content something that you like the false you know we need to specify invariance about the transfer function right so suppose suppose when you start a transaction with a given transfer function you have a specific recipient a specific amount and what will be the usual case of so I will move like yes so I would say the amount under of the sender needs decrease the amount of the recipients needs increased by the amount the balance of the recipient needs increased amount and the total supply is not allowed to trade the total supply is not allowed to change yes you're right yes so this is very good requirement we can elaborate a little bit more so just to repeat right you decrease the sender's accounts by the given amount you increase the recipients account when you give on the mouth and total supply it should remain the same right but one thing for example of abilities so we said the total supply should be the same with these transfer could have transferred tokens from another account right so we didn't specify this so what we get is a partial specification right so in addition to that we need to specify that all other accounts remain unchanged it's now is the total supply and as a consequence the totals of 1 will also remain unchanged okay okay so we also do this in the case the sentence you can't raise sufficient funds right sufficient amount of tokens if it doesn't have the function should not do anything right so the first case a little bit more elaborately right if the message center is not equal to be recipient right otherwise you don't have anything to do and there is sufficient amount of tokens in the balance of the message sender then the most eccentric account the balance should be decreased about the balance of the recipient should be increased by the new amount and all remaining balances should remain unchanged this is kind of a fairly straightforward in formal specification so what will be the remaining days so we have one more kids balances yes yes you're correct number of boxes should be the same as the other specie spent implicitly assumed so if we go back a little this is kind of implicitly assumes we have this mapping it is kind of continuous containing account for everybody every possible address in the world it's very large amount of all possible addresses it will help the idiom kind of fragmented Sarika language takes care of this is exactly yes so what we do is we consider the alternative things right so weak at least deep in alternative is the logic indicates the conditionally which means that intimacy center is the recipients or the powers are not sufficient right all balances should remain and modified right yes overflow at this point I'm not taking into account overflow at this unit yes you are absolutely right so when you're doing specification is very easy to miss um well also the same way as your problems nothing for example here it could happen that these conditions here are satisfied when over hopeful happens because we have modular arithmetic here within a volume with addition and subtraction everything works fine even if you overfall something and the bronies will not work or something the actual amount is not the only it's generally not the gorgeousness attack so in this example I don't take into account so what you can do with verax is depending on your property you can specify the situate that it will automatically fail to verify the overall Stefan right but what we currently do it very easily we don't explicitly check for goals but you need to write your property situated okay and the other thing is you can think of the specification then formula was referring to actual integers where there is no overall tonight this is energies the informal that when you go to actual formal verification you cannot think means this way right okay so this is your formal requirements for ESD point okay now let's go through with something slightly more elaborate we have a constable and the girls help is the bow feels so accountant self conflict the multiple enter which is raised the goal at which you want great and because in faculty culture and behaviour of the conflict is that whenever somebody sends money to the invest right this is a parable function the console control deposit is ready into the escrow right and it's when somebody walks close and it's about time to get close right after the tall stack has passed and the many countries we have two options either the goal was raised in which case the beneficiary of the tunnel cell and we drove the money from the escrow or the goal was not produced in which case the investors can play different for the actor which will be said and this logic should be realized in the tester ownership so here what we do that is marketed deposits our money how much I turn each other is deposited into escrow and to beneficiary who in case of success will receive all the way so on let's let's try to specify this again important right so again let's do the placement so the goal and call time always remain the same right so so this might look like a stupid in formal requirements but in incivility these things can change like the skills of your contract decent stuff in storage potentially they can change so because of this we need to be explicit about which things do remain constant or shapes can change that services a requirement that is all all optimists and people other suggestions right so just to implement the logic that we informally is tied now in the informal language no need to be very sensitive sorry close some we will only work in the past the first time those who only work if you ask because yes so what does this mean because we only work if it was to close them sorry now first time well if not with less than clothesline call the co-sponsor must be done successful yes yes so you can specify that this this is one option oh let me see what's the like nice property I specify here is because yes but maybe maybe it's something along the lines of close so what does it say soon if you know it's it's something else right itself so here just for the sake of the workshop I have the properties fixed so welcome to say any proper cases I will add them to the slides images work with something says the properties and property B here's a similar investor proposes equals the vector in escrow unless to be successful so this means that you can also grow or change money from SPSS okay so let's see sound something more escrow never allow the pot with drawing and painting the movements I said this was one of the requirements we and more yes investors cannot claim refunds after council goal is reached and thank you you can figure out what would be the complement to this no problem and the complementary for the next property needed to talk about this this behavior gets beneficiary can withdraw after cross so beneficiary can only withdraw off the cross cell voltage yes beneficiary can only withdraw a nice color could tell sahabis reach you can say something in many ways stone yes but it's the same so when efficient cannot be dropped before L cell voltage so we have these I now this is most likely in complete specification the behavior of the calcium so providing the full complete specification is a difficult exercise and whenever you have defined your context you don't need to do it depends but this means you should always keep in mind the facilitator finished some news so now we have a bunch of properties and what we can do is we can just attempt to formalize them and specify them in the barracks specification language and try to verify ok any questions one question is as you're going through the requirements is you saw that if you go back to the specific interface for the contract the crowds tale there are three states open his success and refund yes but there's there another state where you've reached the goal it's closed but the beneficiary hasn't gotten around to claiming the thing so it's kind of ending is my my question is with regard to the interaction between this code and the specification you go back to fourth and change the this code based on your understanding of the specification so we feel we can develop the content together with the specification yes this is going it's going to the you you look like and for a variety of the requirements you see that to be something you will change the codes and maybe on the other cats you did some in the specification which is wrong and recovery price it correctly interchange the specification it's so this process you can be shown cuz it seems like here there would be some kind of limbo state where there will be a ballistic yes opportunity there'll be any with states was the girl's back is an inch and these girls matter who is not to call this right the escrow will still be in an open state and you cannot do anything basically you disciplining the state's suspending the beneficiary never gets around every day you've got paper eyes and that's you know so it remains a little stay forever show okay so then you need to make a requirement you can expect a little spent in make the next requirement as I said specification waste is incomplete so there is something else ready to go shows what it said you can escape the the you know state this is total - property rights cannot verify - probabilities they different techniques and what we focus on properties of these kinds which are called safety both of these yes but yes does this kind of reverse should we have the formal requirement perfect depends on your style thought hell develop the codes and so some people refer to an idea called so they understand the program you might benefit and then you go the specification some people try to develop the specification before they understand it and also if you're providing an audit service you're not writing the code you're you're hired through yes delight respect exactly this is sure what people eat a snake yesterday they don't taste the cold or they do suggestions in public illusion was in general yes we do like the specifications sometimes based on the clothes sometimes based on requirements given by the plans yes what about investment in list yes after the whether you can invest after the goal is arranged it should not be possible you should not be possible to invest once yes yes absolutely I said the specification is right so ideally we'll get the complete specification but theses and of open-ended sources require something okay so this one the whole point of this is to emphasize that before you start with formal specification it's good to have informal good sure okay let's move on my findings with Erics we try to formalize these properties in the specification languages by sports I see whether they verify okay so how things get into the specification language and the product is based on something called the linear temporal order so this might sound something very natural so it in fact it is a brief explanation so many most of you are familiar with classical loading which is our everyday logic that we use and you can express formalized properties for example the H is lose the nature for TCU right so classical logic defies the relations between individuals in this case revelation is that the zoom over two inches is even right and how would you write this formally in plastic project you say there exists some integer sisters antibodies who is the ancient ball is wisely seen together Thank You snow you say the things are even this is fast apology and therefore logic adds a lot of dimension to this which is titled right so now these are not a statically laid out in the perfect ideal world but we also have promise and temporal body forces could be violations in most states so you have usually initial state in nineteen point zero point one another state and so on is itself now you can define the relation and here we just as an examples that you'll make accessible and so is the case the ATO bodies which is the danger is even so we've just changed to property very slightly by adding the movies and pepper operator to express this this relation which is an across time not just within a single state right so you see that this this this relation is not in the real world right is he always the same pages or even somebody the same increment H one guy income as night the same will become all right so this is an example property result because it's not always the case so yes that is what this is you and me - yes okay so just to say what you are specified with the temporal logic what you do have is this model panel you specify properties of places for me and each place is the sequence of space right the index of the sequence gives you can discrete time some time progresses from 0 to infinity going in increments of 1 right so for example this could be the desert state or some people might like to come from one because respect and this is the second step this is interesting so this is kind of what your specified in temporal logic and each state we have randomly divided two worlds or two parts that are the constants in servicemen's and the variables of slightly and as an example Alice as a person is a constant which means that if this object does not change across time policy advice is in all time points right the same goes with reverse osmosis and 27 rotate so this insert constant they never change the cross and the other part in the state variables this is our position so variables can change this piece is really kind of water state contains contains personal right and on when we write a formula like walking group itself statement amongst time it is good tool to say what the mental model is and how you liberate those things so here is the different example we have temperature right so we have States and our state the base constant and the variable is the temperature in this paper so time could be days in this case so we did not specify in what units the time its measured its out the screen I think water spicy food the penalty see is this property here which says in virtually always real antigen is at least 11 degrees right so it has some property and you don't to see whether this is true for these things so this is the thanks I need to see whether this is true what we do we start evaluating the the truth of the still ordinance of the parts of the sentence across the states and for example that we kind of the innermost part is technicalities at least 11 degrees right so how would you see which states this statement is true within each statement we are kind of almost like classical logic to the movie right and here we can see the temperature is on degrees in the first state in the Penn State and the last two states here so time can continue opera assume the temperature remains at least 11 degrees or so this is where this part of our statement posted now you don't see in which states the always at least 11 degrees holds true we need to look at the same formula and see whether it always right so always means it may be but after four this is passport right so we can ask the question is it always the case the temperature is at least 11 degrees in the initial state is all true because in the subsequent state the temperature is 10 degrees it's no longer at least 11 right so it's not always the case that the temperature is the place to learn degrees in the initial spin it's also not always the case that it's in all these states until the temperature stabilizes or let's say goes below 11 degrees for n so from these points onwards this part of the formula will evaluates to true right so let's be straight so is the case with temperatures based learned agrees and out the final careful temporal operator the root canal to hear is eventually the case is always temperatures these 11 degrees and eventually is true in a given space in the reason future state when the soup sentence your Navarre is so in which space is the full sentence and so it is yes everything everything yes because no matter which state I evaluate this this formula here there is always a future state where it's always the case that the temperature is at least 11 degrees and this yellow light dungeon in which space honest it's all these I guess I don't understand the meaning of that future state because how do you know it's turn up because there's the heat death of the universe that's where the temperature will not be so - so this is just an example it's an example but there is no that is not saying that we don't know there's going to be a deep death or not so okay okay you're absolutely correct so for these sentences shows we cannot require it but the wording liveness property spherification form of is need is more questions okay good so let's do a small quiz register receipt of this temporal logic queries right and if you this is very unfortunate because this should be a circle so we have two squares which is very important it's all printable character yes he has response Donuts anyway both oh it's the walls right so we use the small square to say always how do you say the diamond to say eventually and the Botsford is next something is doing the next step so what does this sentence say right you have two formulas or two predicates P and Q and this thing says be advised that eventually to write these purposes so of how do you interpret this informally with what we understand okay let me tell you either there's pee there will eventually here will happen yes there's pee yes soul soul yes I put this example just to represent something when we are a volunteer for dinner will ever I think it's always in the initial state right so there is a slight something in this sub script written by we're always about the initiative site so you're almost yes right we operate these militia say if initially P is true then you start with your moment or the current moment eventually song is for the current moment coupons and what you said we can formalize with it's always the case he holds eventually so no matter whether its initial state or initial state for every state in this boat okay so what about this one always eventually they just get some alternative description of this yes it's a possible 4p never happened yes you can play with the de Morgan's laws yes yes this is alternative descriptions but it's another game with alone this is purely off exactly yes so you can interpret this because we have to have time for anything theory you say P is 2 infinitely offer me it's always the case eventually P holds but if we eventually result in some futures that it also must eventually also this will be different right and what about this one if we swap venturing always because yes okay I just wanted some floral oh that is $50 off a shelf a face spell on what is written in these little oddities this basically says it eventually be stabilizes and from certain moment onwards P will always be okay well we have Sigma show so we got into this one so what does it say it's from any state that is produced through that state every state over in every state after and why is these days this is this is this is the boss next but it's true actually what you said right so if you interpret this next as next right it's always the case right if P holds that in the next case parents never P sorry P will never be true why do you know then the next state would be Q and they are not mutually exclusive I'm officially exclusive then also that I just fear is always followed by yes P is always followed by the decisions right and now you have what you said right is if P holds afterwards all words and to infinity Q will pop good socially sure most of us one of us we put so many buddy okay so this one is more complex it says it's always the case there is some constant and signals in this case the block equals them and in the next case rocky possible possible yes the closest value and yes the clock always increments by 1 this is decision all these property steps and assorted so this is kind of food temporal logic right you can write many complex formulas and statements in temporal logic code always ticks ticks by one increment is correct yes around three four four four four is down the dog it doesn't move okay it's okay good so now how all these applies to smart companies right so what we do here we need to fix you up kinda needs first first and foremost and what we do is we do the following we have world space in the world states are the states of the whole ball chain in between samples right so whatever you're gonna depend somewhat change to always around the thing inside the transaction and our space will be the boots length of the book chain and diamond comment means the execution of a single transaction right this is what we do and we don't support the food that parolee we serve on Jesse primarily which is called canonical safety bragging but are not gone in details and roughly looks like this he always your formula soup of this form always P will be some formula of the point shape so you have logical conjunctions p.m. you have distinction people it has implication P implies you have this very interesting operator which is temporal operator one speed which means that once in the past it was called this is the primary person of the eventual operator so we can eventually meaning in future moment P will call this reason in the past few scope or the current speed yes who is one who are these ones of those swans so it's not exactly wants me that these ones so II some possible this is what we do and finally whenever you have some expression you can refer to the previous value of this expression so this is similar to the next operator so in the previous states the weight of this expression was something right so nearly one refers to the previous value of the expression piece of the pie spins by the way what happens in the initial statement there is no previous thing what do you think so when there was no initial stages for simplicity we take the previous method with equipment in the usual state remember it is very sometimes okay and now we have some specific because we after all drinking some video so all these we support suma topics right so universities among a few second token contract we can refer to the same of all these things function reduce the the name of the function which is called in this transaction the top level function feminised of course we kind of start business that goes away we can refer only to the top level transaction the transaction we can refer to function rights so this is the syntax for defining the function name we can also affect the balance of functions so since this is a little bit emphasized we are going to be moving in the future so this is the zeroth argument the title information and if you know what you do is you know canonical name of the function so this is the name of the counterplay of the function and here for the signature of the function with addresses and this is what Evers yes okay so we don't support specification of love invariance so all we do with spaces specified let's go a transaction in readiness starting our thoughts across transactions what if we have known Toulouse in the country it's shown in some cases we can rewrite us rewrite them without whose but if you have not develops we unfortunately don't support it yes yes oh I have forgot that yes they sell something Asian soon yes I build a negation yes so we've got business but you said earlier that you know you evaluate formula always in the initial C in classical temporal yes so what is the semantics different Allen know is the same age is that we support formulas of the shape always be like yes if we're always evaluating in the initial state I'll show you all right evaluates the top level of the formula in the initial state right but it could happen that when you say always this means that the inner part of the formula needs to be a warranted in all states this is the semantics of the always operated so from formula to say formula you change the point at which you've already right depending on the semantics of the temporal operators you change the point that one of which you evaluate the formula right so always change is the point at which you're worried you'll by borrowing in all points from the current point onwards and does the so you have alright form is always nice you know state okay good so now let's move on to duster small quick question next on the box on the left you have once the previous there's no next there's your next we don't support it yes we're somewhat limited but many things that you can express with next actually you can express in this way just you need to massage your formula but you don't we require always to be the top level right so never again yes you cannot think it never again yes this is always a and ease even maybe simplex always have rewards you always sorry you write it down yes we even write it down in this formulation is contract authorities all 13 variants exactly and say this way is but he also can refer to the positive x service as kind of coating so this Pierce of why not next I mean there's there I'm not familiar with the verification technology so is there a technical reason why next is more difficult than previous so for modifications its item only you need to do some gymnastics okay and when you are eventually becomes more difficult way more beautiful because once you always look by that number of steps in the past because in the past time is limited is bound but in the future its empowerment when you are eventually things become ready of their very infant good okay so maybe we'll just go quickly order exercises so now it's time to formalize what we need and just to solve ours our verifier we have two servers in which you can remember X there is an interface let's say this part of the room uses but X 1 and the other part of the room is very soon as can we do it like this because services power forwards notifications yes okay ever will the books [Music] sorry I've just can't miss vericsson online too long here's that down with the Maltese don't like a up associate in the future don't get your servers and for verax index you can treat these things and check out [Music] yes [Music] okay so so if you open if you open the links you see this this kind of interface products on the Left what - that is the list conflicts posit specifications so we pre-loaded Maddux with about context and currently with office on the ear see plenty when you see sorry and council right so we have two contexts which we focus on and the latest service which solution are the solutions to those exercises right we have three extra exercises which you can do but maybe not maybe that would be no time for this day now they have no solutions you need to [Music] what was I'm wondering how do you do these state credit society the state pretty good success define one as a user for a sense okay my PC babies maybe yes so you give police the formulas make them we'll talk about those remaining focus but what's important is the first for me so the first of all really is your problem and it has this form always and then some point so whatever your specify something and then you have a paper which gives you more details the seasons and for example you can refer the contact is using computers its we can equal to the context and this way I for girls family simply sneakers right also you can refer to my seat sensor you can refer to the current time and time yes I guess I stay pretty good spacing I it's like they will try and you had an example of like success or refund that's a big prep it's upon the success fee around the region on the state for something done oh yes okay let me just give you a short demonstration about the first property I taught us my always equals the same imbalances so [Music] okay so it's better we write the first property right this one is simple same always okay so he's the case that the civil bosses equals the whistleblowers and but education thanks subtitle can see that the property so you need to verification takes some time so if you know it's not have to say a two-way get immediately packages education like when you have delegated its you