Formal Verification Panel

Transcript

all right this is going to be the spiciest FV panel ever well we'll see if we can deliver on that all right so the general context for this panel is how can formal verification improve web3 security and I thought we would maybe start by just having all the panelists introduce themselves say a little bit about you know the you know the project they work on or how they use formal verification you know day to day just so you can kind of know who we have so you want to go ahead and start Gila I work in Centura I actually have a vast experience from the web to security this is where I come from I was eight here in

this field and um sartora is first of all a security company and this is what we do we want to protect the web free ecosystem and we use formal verification in order to do that we have a lot of formal verification experts in our company and of course we implemented the sertor approver which is based on formal amplification and also one of our goals is to educate people to use formal verification in order to check the security of a smart contract so this is also kind of our mission when working with the community so I hope it answers your questions so nice to meet you

um okay great hi I'm John I'm the CTO of verdice and so veridice is a security and auditing company and so we perform audits in a number of different parts of the blockchain ecosystem including like smart contracts uh ZK circuits low-level blockchain implementations and so on and so we're also particularly interested in building tools because that's what many of the people in the company you know have a background in and so we commonly use tools in order to Aid in the auditing process and one of the tools that we use is formal verification and so that means for things like smart contracts we will formally verify

critical portions of contracts in order to make sure they're secure and that there are guarantees and then for ZK circuits we commonly use more semi-automated or manual methods in order to formally verify that circuits are actually constrained correctly and are implemented in a way that's consistent with the developers understanding hello I'm Fraser I'm the CTO at Cubist and I'm also faculty at CMU I actually do more verification in my academic life where I focus a lot on verifying small pieces of security critical production systems um but at Cubist we've been working

recently on a key management system and we're using verification to prove properties of that system we've also used the serator approver to prove some properties of liquid sticking contracts and we're collaborating with very dice potentially on some policy Checkers for user policies around Key Management I'm grigora rocho I'm the founder and CEO of runtime verification also professor of computer science at UIUC my specialties programming languages formal methods formal verification and runtime verification was the company that first ordered the uni swap formally verified uni swap also the beacon chain

the deposit contract we develop formal verification tools and techniques and foundations for us foundations are very important we need to understand why things are correct and why even formal verification tools are correct because we've seen so many bugs in verification tools we saw Paulina stock many formal application tools don't find the bugs or if they find a bug sometimes they are just false alarms it's important to understand things from a very foundational perspective in our view performance yes is important but to us performance was never the critical aspect it's more important to have the right techniques correct by

construction and then performance always comes this is something we humans are really good at to improve performance once we know what we're doing cheers um hello I'm Julian so I'm the head of formal verification at nevermind so nevermind does a lot of things in the web 3 space but on the security side we focus mostly on auditing monitoring and full verification which is what I do and currently on primary focus is on CK circuit verification so we have a variety of extractors for various ZK circuit description languages into various proof assistants particularly the lean proof assistant and we then can do partially automated and then par with

some uh what you call it interactive manual assistance for the verification and currently which is something I'm quite excited about we're working on verifying the risk zero ZK VM all right great so a lot of interesting backgrounds here on the panel and I thought maybe we'd just kick things off with you know just very directly like why should web 3 projects use formal verification at all you know so many other tools out there um you know I came from web2 we never really did formal verification there um so so why should web3 be using formal Tech methods anybody want to take a start I guess I can do it uh go for it yeah so

formal verification is very important because basically what you have is um you've got very complicated code and uh people are writing these protocols that have very or that requires some very strict and variance hold and if those invariants don't hold then the entire protocol is going to break down and so that's where Proto or formal verification is very useful it can verify uh in a very strict sense that the invariant that you need to hold in your protocol will hold at all times and therefore that is great for preventing hacks and stuff like that because there's a lot of people who you know are very incentivized in order to try to make sure and variants don't hold

or Corner cases are exploited and all of these things are things that formal verification is built to reason about and to formally ensure you know are consistent with your understanding and that your logic is actually implemented correctly I would like to add something here I think that the web 3 ecosystem actually is a very good application on where a bug can be very expensive first of all the exploit itself usually involves some stealing of money so this is why it's very important to have the the code properly verified by a formal verification and also fixing the backpack can be extensive too because

we're speaking here about upgrades and we had a lot of talks about that and how complicated upgrades can be and also I think it's a very good application because in first of all the code is open source so it in a certain sense it's also more vulnerable because many people are looking at that and looking for bugs so it's very important like to have like many eyes looking on that also good eyes and of course formally verifying the properties that we're interested on and of course the fact that the code is open source makes also um it makes easier to have it formally verified for from many different people and also from Auditors and the third

thing which applies to the web free and it's not always right for the other areas and Computer Sciences that decoded smalls so we know that formal verification is actually a hard task and can be hard to do it like a very complicated system but usually in smart contract since like the price of having B code is high because of the gas then it makes the code like it's smaller and it may makes the life of the formally verification tools easier so this is why I think it's like a very good application in of formal verification yeah great answers there um any other panelists want to add anything to that I guess I just want to Echo that third

Point like you can that's amazing I mean if you're working on a web browser good luck you can't formally verify anything that kind of sucks for you but here you can do it so why not at least try right there are plenty of good tools that just don't exist in other areas so worth a shot all right so sort of moving on logically so we've pulled projects why they should be using formal verification but now they say okay well I've got formal verification that's one thing you know but I want to also do security Audits and I want to do fuzzing and I maybe want to do some economic simulations and you know I want to have funds left over for a bug Bounty and you know but they often operate on under constrained budgets you know unfortunately

then we wish we had unconstrained budgets right so so when you look at the trade-offs between formal verification versus these other tools and like you know maybe a Project's looking like oh do I get an extra audit or do I like pay to have some formal verification done or something like that how should they kind of prioritize formal verification versus other techniques you know can you just do formal verification and nothing else does it replace everything um or you know how do you think about those trade-offs yeah so I think there's a lot of things that can be said there so formal verification I mean despite the fact that it definitely scales a lot better in this area it can still be a lot of work because um I mean I I think Giannis pointed it

out at one point like you you need invariance and variants are very important here because sometimes even though the code is you know smaller size and is actually more tractable there are things that can mess a verifier up and so depending on the type of technology that you're depending on non-linear arithmetic can get very complicated for at least automated verifiers um there's a question about asked about that earlier you can also have issues with loops and stuff like that and so really what at least we recommend to clients typically is anything that is security critical so anything that is going to be like storing money or maybe routing

money or anything like that should probably be formally verified so you have those guarantees but you know other tools are also great at you know Finding bugs as well so for that reason we commonly use fuzzers static analyzers and stuff like that and so like early in the lifetime of your project it's great to use a static analyzer it's great to use a fuzzer and property-based testing in areas that maybe aren't as security critical and then for those components that you really need to make secure that's normally where we recommend formal verification and then for ZK circuits we always recommend formal verification uh personally I can add that I don't think that person that formal

verification replace anything and but it cannot also be replaced by anything I think that there was a talk in the 101 maybe it was yours that Define actually security by like layers and you have to be or you have to have all of them because each each security layer will have like some holes so it and each and no one of them is sufficient to have a whole security uh a security coverage this is why I think that it's great to use formal verification but when thinking about having your code secure you cannot you cannot give up on anything this is my thought

and now we are doing formal verification but actually we are doing a lot of other stuff which needs to [Music] um complete it and also auditing it's it's something very important after formal verification and of course also verifying that the specifications are correct it's also very important so this is how I think it applies for formal verification so um yeah agreed with everything um one aspect of formal verification that doesn't seem to be entirely clear because many many think that oh I formally verify my code so it is correct is that formal verification really what it really does for us is to help us

identify the assumptions under which the code has the properties we think should have and that's extremely useful because it makes us aware how things can can go wrong and also what to monitor after deployment as well so formal verification yes is a tool an excellent tool that puts some rigor in the process it helps us on many aspects but we believe that the most effective use of formal verification should be under the hood we believe that tools should be easy to use by developers and they should use formal verification without even realizing those form of verification same like you have type checking and programming languages right

user type Checker without realizing that you use a very complex algorithm under the hood that does something really that people put a lot of effort into same should be formal verification we believe that should be a smooth process from writing programs writing tests then fuzzing then formal verification then more properties so you shouldn't be like formal verification or no formal verification that's how I think it should be and but also you should have the full arsenal formal verification tools at your disposal if you really want to do heavy formal verification to specify absolutely everything and very fast with everything you should be able to but most of the tools should just be consumers a formal verification

techniques and we should all put an effort into educating the our clients how to use these tools themselves if as Auditors we should audit specifications not code that's what I think we should do I think that's a fantastic answer and this doesn't I'm now not talking exactly about smart contract verification but um a Cubist when we're working towards verifying um user policies we start with these invariants you're talking about and we can actually reuse them for fuzzing first then we can use them for lightweight static analysis and then one day we can actually build on them for full-on verification and we get like the benefit of that initial specification

throughout the lifetime of the code and we get stronger guarantees over time so we found that really really useful yeah I love the points about you know auditing specifications as well as you know just the code itself like I know of instances we had at maker where you know there was a bug in the code and the spec had just the exact same bug so you needed another technique to catch that either review or unit test in that case there really should have been a unit test in that one but that leads me into another question I wanted to ask which is kind of like you know okay specifications and provers like these are yet more codes on top of the code we already have you know how can we have you know High trust and you know if the

software approver or the kvms you know spits out and says yeah the spec you know is accepted it's it looks good how can we trust that um you know what measures are necessary so I can answer about the circular approver so first of all it's really important as you said to review the specifications okay in certain we also offer tools but you can also have your own tools for instance to mutate the solidity code and just to make sure that if the solidity code as a bug then the specification finds it because sometimes this is not the case because as you said you can have a bug in the specification so this is this is a one option which is like to make muted the solidity code and

then another option and this is something that also we truly believe in it is have as many people as possible to review the specification this is why we are doing like these contest in which like as as many people as possible are writing specifications and recently we're even awarding people for writing specifications because approver can be amazing but if the specifications are not good then the the the the security of the God will be as good as the specification so this is a very important thing and of course I truly recommend just to look at the violations I mean okay so if you have a violation let's just look at how it looks like

does it really represent a real example that can happen in your contract and another option also to look at the proof I mean we also offer a way to to look at the pets that were actually evaluated and this is something that we are working on and we really want to give to our customers but I'm sure that also other tools offer that so it's very important to as you said as you can think be paranoid about everything from the code itself to the specifications so this is my point of view on this yeah so debugging specifications and also

debugging verifiers in general is a very hard problem because you know verifiers tend to end up being a very complicated set of code I mean it's normally relatively large and it normally has a lot of dependencies because you've got an smt solver you might be trying to perform optimizations with abstract interpretation so there's a lot of areas where things can go wrong and so what's important at least in order to validate that your verifier is actually doing what you want it to is to have like a proper Benchmark set and I think right now most likely all of the companies that have verifiers have their own internal set of benchmarks I don't think that we really have a very good set of external benchmarks that everyone's evaluating on I mean in other areas there are verifier competitions which we

don't have in this area but I imagine every single company here has their own set of benchmarks that they're evaluating on internally and at least for us when we are checking to make sure specifications that we write are correct we go through a very similar process where normally if something says verified then we start doing we we normally don't mutate the code but we mutate the specification and start changing the specification slightly to make sure that if we mutate the specification in particular ways we end up with expected counter examples so um oh sorry very loud uh so uh the techniques that we use at nevermind are

mostly based on interactive theorem proving so our trust base is the dependent type Checker of whatever proof assistant we're using typically the extractor because we'll have something some piece of code that extracts your code into into some version that lean or whatever proof assistant can use and of course actually the uh formal definition of the language inside of the proof assistant so for the the extractor typically it's a very simple piece of code there's a sort of a one-to-one mapping there obviously we set up very large uh test sets Etc but it's something simple enough that you know it's it's not considered to be too dangerous part of the trial space the dependent type Checker in our case we use mostly the lean proof assistant which has one of

the largest corpuses of mathematics being formalized into it so in terms of the amount of stuff that people throw at it to find bugs I think it's you know one of the better places to be and in terms of the formal specs we tend to of course make sure that our specifications for the languages formal definition is executable in some sort of way and therefore we can actually just like John described run it against some conformance tests do fuzz testing do a specification mutation all of these sorts of things to see if we get the expected so yeah similar situation um I've been in this field for 30 years maybe that revers my age maybe and I've never seen

communities of formal methods people agreeing on a specification language so I think the only specification language I've seen probably the smt lib which is also used in the safety competitions other than that there are lots of tools for even for very simple formalisms like linear temporal logic which has only five constructs and difference in taxes different completely different names for the same thing um I think that would be a challenge um also for coming up with benchmarks for our tools and I take this opportunity to say that again all my years I've designed lots of specification languages and I approve lots of theorems which turned out to be

useless in the end it's very important to pick something simple that connects quickly to your audience mind and I confess that I really like tools like Foundry they are not formal verification tools by Design but they are excellent doors into the formal verification field so if you write smart contracts you should test and if you test you should go to the next level you should write property tests parametric tests and you should use fuzzing yes and then just push another button next to fuzzing symbolic execution formal verification and then you do form a verification without even realize you do formal

verification and I want to actually maybe kill a myth there is a myth that property tests are weak you cannot express any properties so no that's incorrect actually property test is powerful as horror logic preconditions quote post condition assume code assert so you can write any word triple as a property test so it's not like they are not expressive enough they're expressive and they are practical and easy to use that should be the entry point I think that that we can build up on and I want to add on this I was just discussing with security people actually hackers think by properties

this is why it's very important that when you want to verify the security of your code you also need to think by property in order to to think about all the possible initial State and middle state that the the contract can get into because this is how like attackers eventually will think like so this is how we we want to protect our code so this is why I strongly agree with you and this is why I think it's a myth and I think that even if it's a myth we need like to to start doing that to make our code more secure I love it yeah I've personally experienced you know thinking and variance or property is

very powerful When developing and I also like you know the vision of it should just be something you know you just kind of do you've already written a test why shouldn't you get a way to formally prove things I know that yeah there are a number of of efforts along these lines I mean even at maker um Paulina actually gave the last talk right experimented with integrating symbolic uh execution into Foundry itself but this is actually a good lead into like the next question I wanted to ask because you know we aren't at this like you know Space Age future where you've just you know you've written some property tests and you know you just hit another button or you know run the right command and it's all automatically proven for you right now there are a lot of different ways that

projects can decide to apply formal verification you know they can hire a company to like write all the specs for them that company may or may not also be accompanying that with some sort of manual auditing effort they might you know use a SAS tool like and write the specs themselves they might do some sort of hybrid method where a company writes the specs for them but then they maintain them afterwards you know they can also do this earlier or later in the development process Etc so there are a lot of different ways projects can can use formal verification I'm wondering if the panelists have any thoughts on you know which ones are optimal or which ones they would recommend in different situations depending on the needs of the project

big question I know so feel free to collect your thoughts so developers definitely can and should be using formal verification like if they're right now we don't really have a button that can press in order to you know perform symbolic execution from Foundry but I know that's something runtime is working on and that would be something very powerful for developers but you know developers aren't going to have the security mindset and so really uh one thing is developers should try to do whatever they can to find bugs and then after that it's the security

Auditor's job to go in and basically try to exploit everything that they haven't and you know I am of the opinion that Auditors should be using tools like formal verification fuzzing and stuff like that in order to bring higher Assurance audits to their clients because all of those tools will one help uh you know the clients feel more let's say comfortable with the results of the audit but also it's something that clients can then keep and you know move in the future and or use in the future and so uh yeah I think that essentially it's

important for everyone to do whatever they can and I know that's not really a very satisfying answer developers should be using it they should be uh you know probably not using it quite as effectively as like security analysts but it's still useful and important to do and there are going to be people who are going to become very proficient at it and then for the properties that they're not able to verify because you know you eventually are going to have to fight with the solver at some point or something like that that's when a security company can step in and complete the form of verification and also review the specs that they have written and find the holes that they've missed because you know with some or with most formal verifiers if they

haven't thought of an edge case and none of their specifications Target that edge case then it's going to be missed I completely agree here the only addition that I would like to add is that um I don't think that formal verification needs to be done only once I mean probably like the the goal should be to have it in your CI because we actually so with our customers that the code gets changed and maybe they're working on another version of the same contract and things break like even the simpler invariants the simplest environment can break and this is something that actually a CI can be very helpful in detecting it because having like the old

code being audited again can be very expensive but once you had like the all in the whole process as you and you had like the whole specification then but very easy to just rerun the like any formal verification tool on the same specification to just make sure that nothing broke so as John said I think that I also think that should be like from the beginning to the end and baby also in the deployment itself I mean like I think it should be ideal to formally verify that also the deployed code a to the original specification because we thought before that something actually gets broken during the deployment so having me I think that

also we should even verify the code that it's deployed in the blockchain because it can be also very helpful there yeah I think that's a great point about you know verifying the actual deployed byte code because you know it is actually public you know you know you can't usually verify what's uh you know running on the servers you're interacting with but in ethereum you can all right so I think we've made the case to everyone that you know they should be using formal verification you know there are lots of options there are lots of ways to trust it um there are lots of ways to do it um

then how do we actually increase adoption of formal verification web 3 like I think it is steadily growing but you know not all projects are using it yet and you know what needs to happen I think Gregor already answered that question ease of use yeah I think there's one other facet here which is um we're doing pretty well on the smart contract front but there's a lot of other code that touches the ecosystem that is really really important um and also not formally verified and they're you know maybe we think of this as more of a web 2 problem it's like okay your key manager code that's just some Rust code or some C plus code or

whatever but that's really has to be right right or like your MPC wallet implementation that should not have bugs in it so I think more focus on the non-smart contract pieces of the ecosystem would really help everyone definitely agree there that's good I think that I agree here but I would like to add a point I think it's also we are like a community of formal verification and the thing that that it would be great like to motivate people on why it is important so like publish everything that it can be it can could actually was found it was actually found by former

amplification so we need to educate also about the motivation and why formal verification is important and I think that like we are pretty sure about that here but probably the people the people in the ecosystem they're not they're uh they're not enough convinced yet so I think that like having like motivating can be like publishing things and explaining where it actually helped and in order to educate it more people about about why it's important yeah I think publicity can help a lot like the more bugs that are found with formal verification I think goes a long way like the the talk from netnell

earlier about finding the bug in prb math right I've audited code bases that use BRB math and usually you know you're told like oh don't worry about the math just focus on the business logic because you know the time is finite but you know it turns out you actually take a close look at that and write some specs oh there was there was some bug in the math and you know that that's the best Marketing in my opinion all right I thought at this point I mean I can keep you know interrogating the panelists a bit but you know FV is you know mysterious um hard to understand I thought we'd open it up maybe and see if the audience had any questions and wanted to ask any there's one there

yeah at some point uh one of you guys mentioned that blockchain is a great place to try for notification because the code size is small but with all these like scalability stuff we expect that gold will actually hopefully at least in my vision should good as complex as a webto server uh or how does formal verification scale uh going ahead in the future yeah so code might get bigger code might or the the size of the contracts might increase but that doesn't necessarily mean that um I mean your transaction size might also be able to increase but really people have been able to do a lot with uh this kind of asynchronous model that we end up seeing here where you know in a lot of cases there's a lot of

functionality that you want to provide where you want to provide someone with an entry point that's going to be doing something very specific and so normally people are already I would say to my frustration designing code where you have an entry point it does something very complex it triggers like 20 actions and then that is just going to make things uh more dangerous so even though technically you know things might increase that also could end up having other side effects like making the ecosystem less safe I would say and not that it's necessarily safe now but uh I would be hesitant about having people write you know this really complicated

function where uh you know someone's going to be I don't know executing a million instructions in a single transaction I just don't think we're gonna also or I guess another way of putting it is um say if proofs get good enough that we can really scale to huge systems that means something fundamental has changed and the relationship between like proofs and verification is deep enough that probably means something has changed on verification too so and I guess another technique that we could use at that point is abstraction because I think that's an area that hasn't necessarily been explored that much in this particular area because for the most part we've been able to reason

very precisely about these things because of the code size but we can always abstract over contracts in order to perform larger verification which is what is kind of commonly done for larger systems anyway so formal verification is an old field has been used in many other domains before particularly in Hardware verification there are entire chips that have been formally verified and the key Insight not almost all instances or a form of Education was successful on large systems was compositional verification or divide and conquer split the system in components verify them independently and you can scale that way I think formal verification in the

blockchain space is just scratching the surface it just started there are Fields where very large programs have been formally verified already yeah so if I can add to that oh God sorry I can't get used to this um obviously we're as I mentioned earlier we're verifying the uh risk zero ZK circuits and that is of the order of hundreds of thousands of constraints right and so a lot of the techniques that we've been talking about here would would not scale very well to this so once again we rely very very heavily on abstraction being able to break down things into sub gadgets write specifications for them and then really in the end uh we're not when when we think about the high level circuit we're

not really reasoning about circuits at all anymore rather just how these specifications interact these human readable specifications interact and yeah so I think in ZK circuit verification particularly where you can have very very large circuits like this compositionality abstraction is incredibly important although at that in mind we do try and apply these same techniques to uh to a small contract verification too because yeah as we said you know they're getting bigger without another scaling Solutions so I think we're also in a good position where there's been a lot of verified software already and so we can build on what's already verified that's great it's kind of different from say the you know Os or

browser world or something where you have like millions and millions of lines of Legacy code none of which is verified and if you're just staring down that Behemoth it's like okay where do I I even with abstraction like good luck so we're in a much better beginning point so how does the the complexity and difficulty of formal verification compare to the difficulty of figuring out what you know actual humans are going to do with this system and how that's going to go wrong and and how to what's the relationship between spec rating for formal verification and working out what crazy

thing a user will do that you know turns out to be disastrous there are some Works in that area where you combine you actually formalize humans and they they satisfy some physical constraints you cannot very quickly move your hand from here to here things like that but in general same like with verification in general you have symbolic variables and then you do constraint analysis humans can do stupid things and you have to take them into account but there are

people who do research in that area human computer interaction and have formal models of humans even of organs in humans like formal specification of your liver and they you know so yes thank you for the panel does it make sense to formally verify over component of the web with trigger system for instance blockchain clients definitely so uh yeah uh Julian and I both mentioned how we formally verify ZK circus all the time uh those can be integrated you know kind of in with the smart contract or it can be with the

blockchain and uh when it comes to formally verifying aspects of blockchains that's definitely important one of the first audits that we did actually we performed some like lightweight modeling and formal verification over that model of a blockchain because it can be really important to understand how monetary assets because again money makes people greedy and then hacks but how monetary assets are being exchanged because you can end up with really bad bugs in blockchains like double spin vulnerabilities and stuff like that and so again with blockchain it gets a lot harder because it's bigger but that's where it comes down to isolating the critical components and then performing formal verification over

those critical components and then having a model of how other aspects of the system should interact with those and maybe not verifying but you could perform a more lightweight static analysis in order to ensure people are interacting with that component in a consistent and correct way um in the same level of thoughts is there some way that we can have a verification form of verification for economic models well I mean we can create invariants for codes but is it something that can be applicable to economic models or is this

something that is completely out of the scope actually this is something we do even more runtime verification then verifying actual code we work closely with our clients to formalize their business logic and then we prove properties about the models or consensus protocols you can prove properties about them like they don't Fork without even looking at any line of code yeah starting at the model level can be really important as well because if you're able to formally verify a model then that can actually be used to help formal verification in the future so if you can have specifications that describe the the model then when you

actually write the code you can actually reuse those specifications and then another thing is at least in this area if you have some sort of abstract model or some you know kind of high level model of what is going to hold and one thing that we see pretty commonly is people mocking other contracts that you then have to formally verify against in some cases which can be dangerous because that might not be the actual behavior of the contract and so if you have some sort of model that you've performed formal verification on and you have verified that your underlying implementation is consistent with that it means that now other protocols can even make use of it to abstract away your specific behavior and then use that when they are developing their own

protocols which would interact with yours yeah I think in continuous cases you might have to accept some level of approximation because you know for example if you're really trying to address like a high level economic behavior like is my lending Market always solvent well you've got to model price Behavior you've got to make some assumptions about that like are you going to assume geometric Brownian motion well like that's not really true in practice right um and so you may be limited at some point by by assumptions but you know you can usually do something right hi uh thank you for a great panel um so I'm coming from the perspective of a smart contract developer and not a security auditor there are lots of different

types of uh tests to write so standard like unit tests fuzz tests and variant tests Etc and each of those comes with a certain model of uh how to like look at the code look at the design of the system and structure that test do you have any tips or general approaches towards extending testing from just that to using the symbolic tests of tools like homos or similar I think that it really depends on the language in which you are writing the specifications because for instance in territorial like the civilian language looks very similar to the solidity code and so it should be like I'm not saying that it's easy but it should be it should be quite intuitive to write a

specification for one person or actually familiar with the solidity language so I think it really depends on the on the specification language and um so going from test to going to specifications is actually something very powerful and something that we use when we're developing uh specs for clients because tests end up encoding the intended Behavior normally you know there might be some edge cases that weren't considered but it at least gives you an idea of what the developers were thinking about and so a very easy way to go from test to let's say a property-based test is to instead of testing against a concrete value make

that more of a symbolic value and now you can use symbolic execution you could perform some sort of property-based testing and so just even removing those concrete values it can already get you part of the way to something more powerful than what you were starting with all right we've got about a minute left I wanted to sneak in one question of my own which is actually inspired by the previous but kind of flipped on its head so if you're writing detailed enough specification you're really getting into all the expected behaviors why do you actually have to write the code maybe you just write the specification and generate correct code from it is that is that science fiction or program synthesis okay no that that's a separate field of study where uh you you write

the specification and then you have something generate a provably correct code and so uh issue my advisor is very interested in program synthesis but that will take longer to discuss so not feasible yet oh no it's feasible people do it all the time it's just uh it also has some scalability issues and so like one of my projects that I did a long time ago is I wrote a synthesizer that went from our specification to Smart contracts but I think to synthesize an erc20 circuit it took about four hours uh but you know that was something that I wrote in like a month so actually I'm a firm believer that people should not write code they should write

specifications and the code should be generated or actually when I before before being a professor I worked at Nasa as a research scientist for two years and what I've done was synthesis was schema-based synthesis and we generated very large programs thousands of lines of code I think the largest was 50 000 lines of C code and it was provably correct because the fragment of C probably correct from specifications for uh for a Markov models so it is durable especially for domain specific domains like smart contracts of a certain kind all right well that would be really cool anyway we're out of time so let's have a round of applause for the panelists

[Applause]