Formal Verification in the Ethereum Protocol: Current Status and Future Directions | Devcon SEA

[Music] okay just a quick reminder uh we are using uh mcut app for Q&A session so please prepare it ahead of time and the panel will be 45 minutes and we have a 10 minutes uh secured for Q&A great thank you can we awesome thanks uh everybody for being here uh um so yeah we are going to be here talking today about formal verification which is a topic that I think all of us love a lot the chat already before has been intense so that's good um so yeah uh so we'll start I think just start by introducing everybody so we'll just go around uh and just everyone to give us a bit of a a background of the you know background and form of verification and the kind of thing that they work on um so yeah so maybe start with Julian and we'll go around yeah so um my my background is uh I actually did my initial Focus was I did a PhD on formal verification for concurrency I was looking at termination so you know very very uh different concerns from what we mostly focus on in web 3 but uh after I finished that I came to work at nethermind and uh yeah it was sort of um it's a it's a very interesting system where um there is actually a lot at stake while in some ways some parts of the system are relatively tractable and so can actually be verified and so I was really excited to uh to be able to contribute to that and in particular uh apply try and apply hard formal methods to try and really get the highest uh degree of certainty and that's I guess what my uh what my team focuses on and just just to clarify the the tools that you use mostly in your work uh yeah so we we primarily use the uh lean proof assistant and uh and easy Crypt so these are very should I should I add a little bit about or we wait till l oh okay okay okay cool cool cool yeah sorry go ahead um so hello I am Zoe um um I did my PhD in uh compiler verification and for this part I mostly used uh proof assistance in particular cul and for the last couple of years I've been working on building uh tools for verifying smart contracts and for that part um we use a combination of proof assistance and smt solvers to um automate verification tasks um yeah and you're part of the Argo Collective as well and I am part of the Argo Collective um the recently fored uh Argo Collective um from former EF employees who are like building languages and tooling for the ethereum ecosystem and I'm also an assistant professor at National Technical University of Athens um where I like specialize in programming languages and verification cool thanks yeah hi I'm eigor OV I'm an independent researcher now previously I worked in the cosmos ecosystem for like four years so I'm not new to blockchains but I'm kind of new to ethereum actually and my primary tools are model Checkers I'm a model Checker guy using explicit State model Checker checking symbolic State model checking but also simulations uh randomized stuff and and and things like that so yeah I worked on model checking of tenderman consensus for instance checking some property there uh checking agreement accountable safety also worked on verification of smart contracts but that's not like the coolest thing I have did I guess I have done and this year we actually had a project with the serum foundation on checking accountable safety of the new three slot finality protocol yeah great thanks Eagle Okay so we've got a few questions that we're sort of going to go through um and there will be a Q&A session at the end don't forget to post your question you know if you have questions post them to the QR code um and then they will be read out at the end um okay so yeah so the first question which is I think possibly like my favorite question um is about tooling and so I'm really interested to know you know the tools that you use um and in particular you know what you think their strengths and weaknesses are you know where are they really do they work really well and where what are the pain points that you're really feeling um so I don't know who would like to start that or we can just go around yeah I'm happy to start yeah so so as I mentioned we use a combination of lean and easycrypt for very different things easycrypt is a domain specific proof assistant which we use primarily for um cryptography verification and then lean is a general purpose proof assistant which actually well this is a bit debatable but I would say that it has the largest formalization of mathematics in in existence Hall users will obviously be screaming at me they're wrong so um for so the the reason that I say that is that the whole library is not very well organized they have a lot of theories maybe it's the largest coherent Library exactly the largest Cod so Hall is very disorganized lots of like replications of theories with sight differences and then proofs that say hey these theories are equivalent so you can like cost theorems between them and these sorts of things but uh so so technically it has more theorems but as you said not really cohesive so there you go um so yeah so so and lean so our goal with both of these is basically to actually be able to verify and you know I imagine Eagle you'll talk about this more about automated the improving and these sorts of things of course but uh our goal there is to verify I guess the really complicated parts of the ecosystem so we look at verifying like uh complex safety and liveness properties and protocols we look at verifying cryptographic safety safety property these sorts of things which are things that um typically are too complex for automated theorem proving to be easy able to easily approach without a significant amount of guidance essentially so so where do you find where are the pain points that you've sort of hit excellent question so uh in so easy Crypt has uh access to smt solvers and these sorts of which which um typically allow us to automate away these sorts of like small detail things of of like the Practical implementations of programming languages like hey the sum of these bit two bit vectors doesn't overflow or something like that right and and proof assistant typically reasoning directly about these things mostly because actually until recently these this had formalizing these sorts of things haven't been a big concern in proof assistance so it it can be uh it can be quite painful and in fact uh when we were working with rero we had one engineer working for two months continuously on formalizing a bunch of theorems about B vectors and most of them were just like through Brute Force unfolding and it was extremely painful and a lot of these things can be done in like minutes or hours with the right smt solver and and then all of that broke when lean the M lean's math Li changed the definition of a bit Vector so but anyways they've since improved that library and now we don't need to do that anymore but that was a painful moment yeah that sounds challenging that was unpleasant yes um yeah thanks sorry um so uh I use a combination of um proof assistant in particular and smt solvers uh both are great in their own ways uh the good with proof assistance is that whatever can be proved you can prove like sky is a limit the user's ability is a limit and as smt solvers are great because they can automate very tedious tasks that they would be very hard to be to like um for the proofs to go through otherwise and they can be used for like symbolic execution for instance which is very useful like to find like assertion violations or um for errors in the code um this is extremely useful but then if it doesn't work then there is not much you can do about it uh so yeah so so comparing that then to the interactive theorem provs like you know what is the challenge that you find there um in theorem provs or in smts no interactive theor Prov the proofs are hard very hard it's it's the time that it takes to actually get the proof yes it's like it requires a lot of like expertise to like carry out proofs and proof assistance to encode problems to encode specification problems in proof assistance so it's time consuming and yeah but it it's also very rewarding um for a proof to go through so yeah another interesting difference is that um inof assistance you build a proof the proof is there forever you can take it at any point smts will not in general produce a proof that is teable so you need to rerun the smt every time you want to uh prove something which can be like uh time consuming in terms of uh resources Computer Resources and also like it can introduce some non-determinism yeah we've certainly had experiences where upgrading to the latest version of zed3 has meant now the proof doesn't go through for exactly yeah awesome thank you e yeah I'm using CLA plus um as a as a specification language that's temporal logic of factions by Les Lampert he invented it like some decades ago and there are like actually several tools there one is a interactive theorum PR called C APS I don't use it much I'm not the guy who can write proofs for PRS basically um but there is also an explicit State model Checker which just numerates States and if it ter it's good right you have Prov the property if it doesn't what do you do right and in most cases if you dealing with something like consensus it never terminates right because the state space is huge The bantin Faults introduce a lot of new States and everything and like there is a third tool which I have been developing for like since 2016 it's called apalach that's a symbolic model Checker translates t plus into smt but many of you guys I guess imagine Quantified smt and everything our translation is very stupid it actually removes all quantifiers everything is like bounded right it's bounded M checking yeah there are only constants uh and we we just analyze executions up to like 20 steps or something like that uh if you if you're smart you can use induction there to reason about Unbound executions but that's that's kind of hard because you have to invent inductive invariance which is as hard I guess as proven it some point yeah and like the strengths the that you can just run it right you just throw out your spec you push the button it runs the weakness that it can run for days and you have no idea whether it's going to terminate or anything so basically there you have to apply a lot of tricks like introduce additional abstractions if you see it even doesn't work for simple things like reach interest in states have to introduce abstractions make it faster uh observe like which which of the transitions take a lot of time in smt and all of that so so it feels like you you do spend quite a lot of time sort of trying to tweak those parameters to help the proof go through yeah yeah and I guess like the main benefit that you're trying to like to find bugs as fast as possible these tools so you really start with very small input space to like trigger you know interesting behaviors to find problems and then when you're convinced it kind of works you start increasing the states space and see what happens cool thank you okay so next question so I think this is one uh that you know maybe the audience might appreciate as well um so what are the challenges that we've you know that you have faced and getting formal verification to be adopted you know within your organization I think that's the first bit but also in a kind of broader sense within the community you know because I certainly feel that there are a lot of challenges here um yeah so I think in web 3 one of the key issues is that uh the technology and the space are moving so fast and everything we do has a very high cost in terms of tooling it takes a long time before you can develop formalizations of the new languages the new systems Etc so that we can actually practically verify things and that that's I think true whether whether using interactive automated they're improving to some extent um and and so the thing is uh it certainly feels like I'm playing a bit of a guessing game sometimes as to what is actually going to be useful next to figure out where I should actually be applying my team to actually developed new tooling and it's happened a couple of times uh I think I can think of two instances where we have invested like 6 months plus of work in a tool only for it to be essentially deprecated the moment it's released so I mean this happened with a tool that we had that was called Horus for CYO zero which was the first stocket language and literally I think a week after it was released a stocket stock announced that there was this Kyo one language going to be released and Kyo Z was going to be deprecated and we spent six months developing that that was pretty painful I can imagine that sound yeah very unfortunate yeah so there's that and then I think uh I mean this is more true for the kind of techniques that I use um where uh our techniques are not necessarily so I mean we um we were talking about you know the difficulty in embedding things inter active their improvers and there's truth to that but also uh it's also true that you know modern interactive theor improvers you can embed all sorts of automation into them and you know if you find the right set of automation you can make things a little bit more generic a little bit more well much more robust in theory um I mean there are examples of for example uh the verification of Cairo which is written in uh in lean actually apparently it's I mean the details are not all public but this has been developed by Jeremy avad at CMU and the proof generation is apparently almost entirely automated uh inside of so so uh so that that's uh so so there are sort of some uh interesting things sorry interesting things you can say that you can do in that direction but the there is a difficulty with robustness where like if clients change implementation significantly we have to redo a lot and presumably it's not just you know you mentioned languages but presum it's not just languages so you know I know that you work in the ZK space quite a lot and so it's actually new algorithms as well that are coming along you know you've got plon you know turbo plun there's all these different things coming out and so it takes a lot of effort to understand them to understand them and to understand hey what are what are the properties semantics they enforce Etc uh and also because we're doing verification on the cryptography decide like how what are the cryptographic guarantees all of these sorts of things so yeah I spend my life reading papers on a variety of different things so there you go yeah well things you could be do the worst jobs to have so cool thanks Julian sorry so uh as Julian said yeah it's very time consuming and there is a step learning curve even within experts to go from one tool to the other so if there is a team working in formally verifying something with a tool then like abandoning the tool and going to something else it's going to take a lot of time um so but there is also a lot of Maintenance burden like it's hard you build something then the code changes then you have to adjust the specification the verification that can also be um very hard yeah sort of like maintaining the proof alongside the artifact itself yeah exactly and uh things St quite quickly in this space so yeah that can be tough um so yeah do you feel like there are any strategies to help kind of mitigate that you know like to make it easier to maintain as artifacts change or so I think programmers should program with verification in mind or at least specification in mind like I think there is a lot of value to writing specifications even these are not going to be formally verified they can be tested I mean there is property based testing we can test specifications and that's actually quite useful and productive in terms of code quality thank you thank you uh egole yeah I mean when I started working at a company like for five years ago you know doing stuff for for Cosmos I I talked to a lot of Engineers and actually I expected them to complain about performance and all these things but it wasn't the case they complained about usability because basically usability I shown them t plus and if you have seen it it's kind of lat like Mazi syntax and they all kind of questions like what is this thing looks like what is this mountain doing here what this like kind of strange questions but usability was number one issue there you know like uh what do I write how do I write it why do I write it this way why don't I write a loop you know all this stuff so I think it's the number one issue there and at some point we introduce the surface Syntax for plus it looks like a programming language and that changed a lot people stopped complaining immediately they were saying okay this we understand that's fine oh that's t plus that's fine it's like very good so really like focusing on usability I think is number one thing so kind of connecting to what people already know makes a big difference yes exactly exactly if people come even have seen like a simple functional language it's much easier for them to connect to what C+ is unless they have been rising proofs in Mass you know which is very unlikely if you're talking to Engineers so that's one thing and another one like what you already mentioned it's kind of time to Value you know if you tell them I spent like three weeks write in a specification and then I check it they will be super disappointed because at some point maybe it doesn't check you know nothing happens and it's very important to give them results like on day one basically you start writing the spec you tell them look I can generate an example I can show you an example where where you know an algorithm reaches some State and I super excited about it because before that they were drawing it on a whiteboard which is super time consuming if you can generate an example like in 5 seconds and they can read through it's amazing right now so time to value is super important and like randomized randomized exploration I found it super useful before you try to do any proofs just try to break to sort of find that low hanging kind of FR exactly exactly and do you like do you feel um like you know there's a challenge here in in getting people to appreciate the value of formal verification I mean I feel like that sort of what you're talking about there that helping them see results quickly will help them see the value yeah I guess it's it's a bit more than that I think it's kind of a problem of trust because if you if you write a program you kind of can run it and get your confidence in that it does something useful if you write a specification it's just a piece of text and it's it's hard to understand what it makes any sense the same for PR I guess right unless you prove something right and it's really you have to give them a way to gain trust in this artifact very quickly and whatever execution random simulation helps a lot it's it's really because for them it's kind of a detached writing on a wall which is not running and all Engineers because they're used to running things so I think it's it's kind of yeah okay thanks you know um if you don't mind me just interjecting um the analogy that I've actually used for it fairly often is that I I feel like actually formal verification suffers from a lot of the same problems that vaccines do in genuinely genuinely in the sense that as I said people don't really understand them right and the thing is if they if they work correctly then nothing happens and no genuinely if if we if we do our job right the point is nothing bad happens and you never feel like you needed to do it in the first place then right yeah exactly maybe maybe nothing bad would have happened if I did nothing you know you don't know so yeah I I I see where you're coming from there yeah okay okay um so this uh I feel like this is yeah okay pretty similar or sort of related question um so obviously formal verification is often seen as quite difficult and costly to apply I think we've already kind of covered that something but I guess the question here really is you know as a community what can we do about that going for forward how can we try to lower those costs you know what are the things that we can do um and I think Eagle already did touch a little bit on that but but interested in in more thoughts that you have um I don't know who would like to go yeah zo go yeah I can go so um as language designers and implementers I think we should build languages and tools with verification in mind so once you have a language that has like integrated support with verific ation then things will become much easier for programmers to like get used to adopt trust even like languages for instance with support for like but real world languages not just like um very Niche languages that are used in academic environments but like real world languages with support for writing preconditions post conditions having Rich type systems like being able to write in variants even if they are not proved uh like automatically or directly even if they are tested there is a lot of value to it to like for people to learn the discipline yeah so so we were talking about this actually yesterday in the formal verification hangout um and in particular talking about solidity and solidity has this kind of extension called scribble where you can write pre- and post conditions as comments so you know it seems to me you know what you're suggesting there it would be really nice to see that kind of solidified and turned into part of the language itself yes exactly and then and then it will be easier to reach more people it will be easier like for people to think about it when they write code which is extremely important to make formal verification like viable great yeah I actually completely agree with that I think you know using some lightweight methods just to to help people get into it and to see the value and to catch that low hanging fruit I think that that definitely is a win and I think um success story is R which has like very rich types typ is verification basically and it's widely adopted and like people love it and I think it will be nice to have more examples like that even for like languages compiling to evm cool um you go yeah yeah I mean what I wanted to say yeah I mean really providing faster feedback loops that what we could do you know to give value to the to the users but also maybe maybe the community could help us explain what they do not understand because it's it's also maybe people are a bit afraid of saying it because it all looks complicated PhD level stuff you know and people should be just up front saying like this I don't understand and this doesn't work for me maybe you should simplify it I had conversations like that it's sometime sometimes it hurts but it's very useful to to hear it actually yeah I mean I definitely agree you know academic papers in particular can be very hard to read and understand and even coming from me I've got that background right you know you know so yeah anything that can help bridging that Gap but also having like open conversations like we have now about what works and what doesn't that's super useful cool uh junor yeah yeah so so the following in the same vein I think yeah accessibility is super important one of the things that we've done actually is writing um property testers that allow us to extract well what do you call it uh We've written a property testing extractor essentially from specifications that we write in lean so we can write specifications for a smart contract and as long as they're decidable we can automatically extract a property tester from it um so like um like input values for example is that what you mean yeah yeah yeah so so basically it uh gives you like a generator for input values and then a relationship a decidable relationship between the input and output States and then we just run it on execution client and and see see if it's satisfied run the decide function and and so yeah having this sort of feedback uh being uh sort of you know developing these specifications in conjunction with the engineers to see that for them to really see how you are solidifying their intuition into mathematics uh and as you said Zoe may be integrating more into the process but I mean I I think that there well okay I mean maybe it's convenient for me to put the blame on others but uh I do feel like there's also a bit of resistance from the developer community in a sense on that because they feel that there's a small cost to it and it slows down the development and often we've experienced some degree of push back sometimes so um yeah I mean I I definitely personally see the value of testing you know straight away right and automated testing you know if it's easy to apply I think to me seems like a win right for sure for sure so so one question I think of here is you know like if I think about the developer community and I think about lean you know my experiences of lean lean it you know is very powerful but it is also very challenging to use it and I'm wondering you know how you would see that Gap being bridged yeah so uh I I I I don't see uh an immediate future without so in domain specific cases sometimes we've been able to develop like enough uh automation that plausibly with enough training someone who isn't an expert in interactive the improving could actually prove some basic things so but but for sort of general purpose tasks that's probably not happening tomorrow certainly but what I do think uh is nice about lean and that makes it more accessible than many other interactive fa improvers is that it has this uh elaboration step where essentially so so lean has lean compilation has multiple steps and the first one is called the elaboration where basically the vernacular the high level language is compiled down into a core syntax and the thing is this elaborator is itself arbitrarily meta programmable inside of the language and so basically I can give arbitrary strings of Unicode uh meaning right and that means that uh you can embed domain specific languages for example yes yeah yeah and with with arbitr Unicode and and so in particular with like maths we can get uh you know you can have a sum over a set and uh with with some function and these sorts of things and we can write it in a notation where I can show my friends who are you know mathematicians have never touched a programming language in their life the statement of a proposition and they'll understand what it means they won't understand the word of the proof but they will understand the statement itself and I think that in itself is is a very is a good is a step in the right direction okay um the other side of it is that if you have genz developers some of them will use emojis as variable names and you know there's nothing wrong with that uh hard disagree so cool I don't know if any if any of you guys want to add anything more to that about bridging that Gap um like one can like build automation inside the improvers they someone could like offload things from the the improver to an smt solver things have been done in this direction not very like it's not very widely adopted but there is stuff to do there another thing that I've been thinking like for some time now is like um like integrating AI into the proof process because AI can write pretty good damn code and there is a very well understood syntactic Corr respondence between writing code and writing proofs so if AI can write pretty good code they can write pretty good proofs and you got the advantage of course that that if it writes it you can check it right yes exactly exactly you don't have to trust it and you can you don't even have to trust the code that it writes if it writes a code it writes a proof you check the proof if it works happy times so I think there is stuff to explore there but not not only in the ethereum ecosystem or blockchains but in General I think that's a very promising direction for formal verification okay thanks okay uh we'll get back onto the script um so so yeah okay so focusing now on the ethereum ecosystem itself and you know so you've all applied formal verification at different levels of the stack in different areas ZK smart contracts consensus so I'm wondering you know where do we feel like where can formal verification have the most benefit in the ethereum ecosystem how do we feel like it where where is the where is that kind of sweet spot where the cost value benefit is best thoughts for for me the answer is obvious it's infrastructure level stuff right so like ZK verifiers Checkers these sorts of things where there's going to be a huge amount of uh the ecosystem whose value will throw flow through that and uh you know if that is exploitable it's a sort of a um a single point of failure where just everything will break right and so so cryptography uh obviously Consensus These sorts of things right um like uh like uh contracts that things like wallets and these sorts of things that mediate a lot of value flow I I think that's really the place to focus yeah um and of course these pieces of infrastructure tend to uh change less over time than say you know like some defi smart contract or something that is sort of inactive development shall we say yeah and I guess you would say that that you know for example you know think about ZK EVMS it's just a good example in this case um that it is possible to verify at that level like it you know some people may see it as as actually something that couldn't be done yet but actually it is possible to have success there yeah yeah absolutely I mean um we we haven't worked on zkm specifically we've worked actually mostly on risk 5 uh uh ZK VMS but uh but yeah I mean we we have actually I I would say pulled off some fairly significant uh results so as of yet because in lean there isn't a full risk five spec yet so we haven't done like a full stack verification yet but like for risk zero we verified some very important parts of the instruction decoder making sure that that it matches the formal spec we've uh verified some important parts of the ALU these sorts of things and yeah it it can be done and I think though are where I mean EF is currently as everyone in this panel is probably aware uh funding a fairly big grant program to enable just this and I think we're probably like and mostly year away from having fully a fully verified R 5z KVM so yeah cool zoie um I agree infrastructure is a huge thing like to have formal verified code because it's easier like to have experts doing that and it's very important and it can like Inspire others to do the same thing for like user codes smart contracts then it's like it's building some um discipline that others can follow uh um for me it's also verified compilers and languages with well defined semantics that can people like use to write code that they understand well that's the first step and then they can verify yeah so for example the solidity compiler would be an example you know like there certainly have been a number of of you know significant bugs in the compiler and trying to eliminate that would be super helpful yes yeah and also I guess um you know in terms of smart contracts themselves um there are a number of kind of fundamental contracts like the deposit contract and I know that there are a number of contracts coming out for the Petra upgrade for EIP 72 for example um you know those kinds of things are high value targets I guess yes and it would be extremely good to have reference implementations at least that are verified if not the actual implementations that would be even and it would be nice to to see you know like in the EIP document itself for examp example to see some reference to that to say yes you know we have invested in formal verification maybe maybe I don't know some of the artifacts maybe some proofs or I'm not sure but something to so it was more visible yeah yeah yeah yeah totally cool thank you yeah I mean we have seen quite a bit of success in smart contracts already I guess so maybe we shouldn't invest that much into them I don't know but the smart contract people disagree I guess right uh obviously consensus yes but also I would say it's kind of whatever you cannot write in code this should be verified because there are a lot of hidden assumptions usually about timing about interaction of different components and this is usually written in English right you can write it in code but it becomes tricky because there is nondeterminism there are some kind of external inputs which you cannot control so this kind of stuff that is usually written in English I think it really requires some kind of if not complete verification but at least specification and an attempt to to understand whether all these constraints that we have in mind whe they make sense maybe they're even contradictory so so you're almost describing a sort of a a mind shift away from writing our specifications in English sort of predominantly in English towards you know making something that can be mechanized even if you know the individual doesn't do the mechanization at least other people can then do it right exactly exactly I'm me the a lot of hidden assumptions in in many of these protocols because we tried to to like go from English to to T and you uncover a lot of things you know so in terms of consensus layer Protocols are there any sort of mechanized protocols for example um I mean there was some proofs in in C I guess uh raft was proven to be correct in in C as far as I know um pxo incl proof system it was proven correct and for the rest I guess m checking you know what we did at least showed some results for for small parameters which is also an achievement because it's hard to do it for for the general case yeah okay cool thank you okay so just now moving into the sort of final part which is uh I guess looking a bit more into the future um see I guess how do we imagine the you know the role of formal verification evolving within the ethereum ecosystem like where where are we going from here you know what do you think how do you how do you see it going I guess it's me look like it yeah I'm not going to lie I don't have well h i i as as I said in my previous answer right I think it is absolutely because like it seems that the ethereum community their goal overall is to I think at some point in the future be a significant important part of mediating the transfer value of our society as a whole right uh and so if that is the case and we have you know so many of our interactions mediated through this system um it can't go wrong like there would be very serious societal consequences if we got to that point and things go wrong and so yeah I I uh I do think that if that is really a goal for the ethereum community that they should continue pushing this and particularly in the infrastructure I mean okay I'm kind to push back a little here actually cuz I feel like you know your answer is sort of idealistic in a sense right completely interested I'm interested in like but where do we you know are we actually on that trajectory like is that the direction that we're going in at the moment do what do you think I I think there a question more for the ethereum community and less for me you know you are part of the community I I am I am of course but uh I work on something pretty Niche and uh you know in terms of uh you know there are people out there who are looking at all sorts of governance problems how these can these can actually be used to in a decentralized way actually manage real resources in the real world and I'm I I'm not this isn't a focus of mine to understand these sorts of things right so so I I wouldn't consider myself an expert but as I said I do think that certainly if uh i' so I I do feel that this is from things I've heard from people in the community this is a significant goal of the community and if that is to be the case well we should really make sure that it's actually correct and safe and we're not going to suddenly wake up and you know all of our what do you call it accounting of Valu is completely lost as a society right okay um I think within the ethereum ecosystem um the adoption of formal verification is quite impressive compared to other like to the industry in general so that's great um so that that's the thing that attracted me to the um space at the first place and I think going forward so I mentioned this before but I think it will be quite important to build languages with verification in mind like clean semantics like well defined semantics uh Rich type systems uh support for verification for writing specifications I think this will be quite important going forward to like people who have haven't heard about formal verification before to start adopting and like building a me a mental model for it and being convinced that it's something useful so so really you know ethereum has actually made a really good start so far that's what I'm hearing totally and it's really about you know as we move to that next level you know really trying to push it further into all of the languages and systems that we're using yes yeah and I know that they are for example interested in in in looking at solidity and and trying to think about what they can do there so that seems like a really good opportunity for yeah exactly that's an amazing opportunity that we have in front of us to like um make the adoption even wider and it will be very important for people who are not experts in the field to start learning it so um building the right tools the right languages and also training people to use them cool thank you yeah I also have an impression that ethereum is probably the blockchain ecosystem that has the most adoption of formal methods that's like my impression and that's really cool um yeah I think I would say yes we should apply formal verification everywhere but it's impossible right it's just too much uh we should focus on on the most critical things first right that's obvious uh but maybe what is less obvious we should also give small examples of what works because what I have seen in CLA plus people complained that okay you have this huge specifications of consensus it's so hard to understand we don't understand what consensus is can you give us a simple example like a ding philosophers or like this River Crossing you know and show how it works step by step so I think it's also important you know to build this bridge between the developers and users and formal verification people to show small examples yeah so that's about sort of spreading the word about formal verification and and kind of easily understandable chunks rather than only having these big examples that are that are very difficult to to get exactly I mean if you look at at proof written in all the serum PRS you don't know where to start right yeah yeah yeah cool okay we've got a few minutes before we go into the Q&A um so I will just dig into one more thing that something that I've kind of heard on the grap vine when I've been here in Devcon so you know it seems at the moment uh you know many people doing formal verification related work are working uh you know doing sort of auditing of um you know system but contracts ZK systems and so on um but it does seem like in many cases uh you know people coming to audits you know they they don't have specifications for sure but they also don't even for example have test cases sometimes because you know they're they're pushing it to the wire so much and so it does feel to me like you know if we're struggling to get people to write like tests then we're going to be struggling to get them to do formal verification and what what can we do about this how do we how do we address this thoughts it's a difficult question uh who wants to go first yeah go on go these are absolutely write specifications test them it should be mandatory um yeah so building nice I mean fuzzing property based testing like this will be quite important and like it's the first step towards like formally verifying like formally specifying testing the formal specifications and then moving to formal verification of these specifications is a is the right way to go I mean you cannot start by formal verifying a spec you have to convince yourself that it's true and testing is a very good so it's a key stepping stone really yeah yeah yeah okay yeah I in my back con we were also doing audits when I work to the company and now even right um and at some point I was thinking like maybe we shouldn't require that if you don't have an English document describing what you're doing we don't do an AIT for you if you don't have tests we don't we don't do an AIT for you because it's an absolute requirement if you don't have tests it's just you cannot do anything right it's most likely broken if you don't have tests very likely right I mean it's obviously hard for companies in a position where you know they want to take on clients and so on like they are I think at the moment sort of managing that by adding test themselves or you know reverse engineering the specification in some cases um I mean in some sense it raises the costs of the audits as well you know like if that's part of what you have to do before you can even do anything more verification um yeah okay thank you uh Julian so yeah I mean I I'd like to Echo what Zoe said if uh anyone in the audience we were talking about you stop it um but yeah and and also as you said I mean we we have faced some interesting situations with clients who obviously in this situation will remain less where they've told us hey here's something we want you to verify and then when we've asked them about it they've said well we actually don't don't know how this works anymore the people who wrote this left and it's literally we've had to reverse engineer fairly piece like complex pieces of well I'm not going to give too many details once again but we we've had to reverse some fairly complex pieces of software because just the client themselves didn't know how this thing worked anymore and uh yeah it's a problem um but yeah the other thing that I kind of wanted to to float with the other panel members was one thing that I've been thinking about recently is that like modern proof assistants now offer the ability to embed like very fully featured dsls into them and one thing I have really been thinking about so particularly in the context of consensus right is that um I it feels like the linga franer for a lot of like consensus research and specification is like a simple subset of python and i' we've been thinking of like embedding this into lean so as to be able to then reason about safety and liveness properties and that is a way that maybe that we can we can create you know a tighter feedback loop and a a closer relationship with the developers through the sorts of things just an idea I've had I don't know if that resonates for you guys at all yeah yeah totally okay so I think that probably ends the formal part of the panel and we'll now move to the Q&A part and um I guess there with questions from the floor cool U thank you and uh please give a big round of applause to our panelists um as a PhD researcher myself I also um kind of uh value when people like uh make time in their schedule to come out and talk with the community about you know their experience and expertise so we have quite a few questions and I think the panelist cover most of it but still you know people in the audience are not convinced like why should we go this and do this extra step to implement formal verification so the first question would be please share the elevator pitch to engineering teams to implement formal verification as a hard gate that care about velocity of shipping code and how can we make this easy for engineering teams to lean in and you know uh do this method so if anyone um so writing code that is correct and does not introduce unexpected failures is like the elevator Pizza I would say it's something very valuable on its own end um and then again like I really believe in writing spec and testing it before anything else so if anything that that we can do to convince engineering to write better code is like specifying it formally specifying it with like some specification language and then testing the specification and then that would be a great step already towards having better code in in like a viable time frame not like spending three years to verify a piece of code uh well this happens a lot um I think to all three of us at least this this has happened or four of us um yeah so I really believe in the value of specification yes yes yes that would help immensely to have native support from the language that it's a language that people use and like it's like um a common ground for everyone to like yes it's not something nce it's not a weird tool that very few people know and understand it should be something that is widely adopted and has support for writing specs and clear formal semantics okay uh next question is kind of similar uh what metrics are used to measure impact of formal verification on the on the security and reliability of ethereum if you can maybe give us more information how can we measure the impact of formal verification I think it is what Julian said before like if it works nothing good nothing happens right so I mean you you can also uh so certainly you know when we formly verified things we have at times found some fairly serious bugs uh and and so certainly you can when you do find these bugs you can uh sort of evaluate the uh the impact in terms of hey what would be the worst case scenario here right and certainly uh you know uh we we found uh bugs in CK proof systems we found bugs in defi smart contracts which would have potentially allowed them to be completely drained or Frozen and these sorts of things so there there there's perhaps an economic value that you can put to it but as you said once again what we do is making sure that things don't go wrong and so it's difficult to quantify hypothetical futures or hypothetical you know parallel presence in which things went very wrong yeah I mean one thing I have seen in consensus which is very cute you can actually just add a bit more folds and in this case the algorithm should break and that's like very easy to show people just have one more fault see what happens it crashes all possible ways you know and that's like an easy metric you know but another metric like in in code verification is just how many bugs you have found basically and and there is like another metric which is saying how fast you you have found this bug you know okay thank you um we still have time and uh uh also have still a lot of questions and U the next question would be have you had experience formally verifying uh ZK proof systems and the cons at constraint polinomial level and to what extent does Lan have to be modifi it to express theorems in that context yeah yeah I think I'm the best person to hit this one so yes we have done that uh how much does lean need to be modified not at all it has uh Notions of finite fields and polinomial built into math Leb um now uh We've also actually written some like uh custom decision procedures for finite fields and these sort of things that do speed up the uh verifications of these these properties but yeah other than this it's mostly actually just uh extracting from whatever your ZK DSL is writing that extractor from whatever your ZK DSL is into a set of a polinomial constraint system in lean but as I said there's primitive support for that in the standard Library the the one the one issue that I think is a bit more interesting and where we're hoping for some more language support particularly in plony 3 is that a lot of the ZK dsls as they are now that tool chain is not at all modular so it basically it goes through a bunch of ation steps and right at the end it just dumps you you know thousands tens of thousands of constraints sometimes in one big in one big one Big Blob right and there's no notion of oh this came from this chip Etc and so one one thing that I think will be uh good in terms of helping this kind of verification scale better it's more actually on the ZK DSL level is actually having uh a more a better notion of these sorts of modular boundaries this is a chip these are how these are wired together yeah sorry so no no so just just following on from that because at the formal verification hangout yesterday um you know there was mention of uh it was called LL ZK which is lowlevel ZK which is about bringing a kind of Intermediate Language that all of these dsls could compile down to and then the verification work could come off that that's sort of what you're talking about uh yeah yeah exactly exactly I think this is actually a great idea the one issue that I I would issue in quotes that I would have with this is at this point in time the proof systems are evolving so quickly that it's unclear that any DSL that we were right at this point in time is really going to be able to cap capture all of the constraint systems going forward uh but uh from my understanding this LL ZK or whatever it seems like very honest like a very solid attemp by very di doing this for the moment and I'll be very curious to see their progress yeah okay the next question is what is the first baby step you and Tool you recommend for engineering teams to start on a journey uh with the formal verification hm well I mean uh most for most developing teams are already using formal verification to some extent in the sense that often they use type systems and that is a very simple form of formal verification right um and I think as Zoe pointed out rust is becoming like more and more popular and actually I mean linear type systems certainly I think within smart contract development has uh actually have a lot of potential because I mean most smart contracts are actually kind of like about managing resources moving money from A to B making sure that I haven't uh you know I haven't double spent any of that money I haven't not spent any of that money right and so I think that there's a lot of uh on a very low level there's a lot of capacity for just using basic type systems to en forc properties are useful um I think lightweight verification tools is a great start um they should use atvm to symbolically execute their smart contracts um it's like easy on the programmer end to like convert their tests to symbolic execution like assertions and then take them formally with a symbolic execution so this is my recommendation um yeah I also think like simple tools and I mean no Shilling but you can check Quint that's like the surface syntax fa plus it has a random simulator like starting very easy I would say but something like that in general yeah um and um one more question between wiper and solidity languages which one is easier language to formally verify is the last question can the answer be neither uh I mean neither of these languages have fully formal semantics right and so this is this is a key issue that we have is that typically uh you have to go to Ule or the evm to really have formal semantics so actually have an actual fixed meaning of what the language means otherwise for both of these really the language semantics are defined by well whatever the compiler chooses they are and uh and and so the answer at least for me is neither you just have to compile them to some other representation which does have a somewhat fixed semantics and then reason there uh none I think uh but I think there is a huge opportunity here to build languages with formal semantics and verification in mind I think that's a huge step step towards making formal verification more widely adopted in the space uh thank you very much sorry thank you very much and uh