Formal Verification: Finding Hope in the Impossible | Jonan Scheffler - Certora

[Music] hello everyone thank you for coming down to hear me talk today about formal verification and finding hope in the impossible I think it's a good time for that story everyone needs a little more hope these days um I just want to see that out of a the audience we have here raise your hand if you've used formal verification like if you actually used formal verification in your software s Tor people you're cheating okay a couple people so some of you are here to learn brand new and that's good because I'm going to I'm going to speak briefly about formal verification at a high level and what it does and some of the criticisms in the past and where I think it's going in the future but largely the technical details of formal verification are not going to be discussed I'm happy to discuss those out of band so come and find me we've got a bunch of people here in Cur uh who will happily help you learn how to use this stuff um so my name is jonan I go by the jonan show on the internet all over the place this is a picture of me setting up our hacker house the other day here in um in Denver we have a hacker house going today where you can come by and U build a badge and uh we have an escape room we have a big party tonight there's all kinds of stuff going on if you scan this QR code it'll drop you into our little telegram group and then you can go in um learn more about it but among the things that we have at The Hacker House is a little PCB that you can assemble if building a multicast multimodal mesh device to achieve proximity based key exchange is a thing that sounds interesting to you or Hardware hacking generally or just uh that kind of a club that is into that sort of thing the order of the builders come and talk to me and I'll give you one of these afterwards um I'd love to hear from you we'll hang out so I work at this company called Sir Tor sir Tor had some big news this week we just open sourced our approver this is open source formal verification now we are I think uh before I worked there I also thought uh kind of at the Forefront of what's happening in for formal verification we've been around a long time we've been working on this for six years and in that time spent rather a lot of money building what I think and we think is the best prover out there uh and of course uh we would like you to try it so if you get a chance go by sor.com and check it out it's a pretty cool product it's very easy to use and that is a thing that we've been wanting in formal verification for a long time so let's talk about that um form of ucation just for those who are brand new here we're talking about mathematical proofs of program Behavior not necessarily that you are proving that your program is correct right because you're talking about the behaviors and the correct behavior of a program is always up to the interpretation of the author right but what formal verification can give you the the ability to do is to State an invariant about a system you could say something like hey we're building a bank the collective balance of all the people in the bank should never go below zero because then we're not a bank anymore right you could state that about your system and now what C toris prover can do and other existing Prov similar Technologies can do is they can go through those rules test your program with every possible input that could could come up every situation that could come up and they can say yes this rule holds or if it doesn't they will provide you with a counter example of how to do that this is what formal verification is you work through these and you use different types of logical reasoning to write these rules and write inv variance and modify your program in a way that makes it easy for us or another outfit who has written similar uh software to go in and break it down to a bite code level and analyze it there for these formal verification methods long term this means some pretty important things uh but we'll get to that in a minute when we get to talking about the future of this this technology so this is on Hacker News from a few years ago I talked to people a lot who are saying like yeah people used to be critical of formal verification in the 70s and 80s and nowadays mostly people have adopted this thing right um I think we live in a little bit of a microcosm that many of the people here in the audience probably work in the D5 space we certainly all work in web 3 or are familiar since we're in this building and that makes us a pretty uh small community actually uh I think in 2023 they said 28,000 web3 developers worldwide in the Electric Capital report something like this um as compared to about half a percent of the 9 million people on the planet we're only 28,000 of those so we have this perception maybe that formal verification is a thing but very largely outside of the web3 space people say well I think I did a a half of a a semester on formal verification when I was in college and then they told me that it couldn't be done that it couldn't be useful right um which is exactly what happened in this case why don't people use formal methods they're really sample to to this question is the really simple answer to this question is it isn't useful basically most applications are being specified by people who don't truly understand what they're trying to specify he goes on to say which is a really important distinction here that is important to understand about formal verification generally that we are not proving that the entire program can work for a very simple program obviously you can do that but the systems that we build are far too complex to prove every facet of them and it's not necessary that we do that to improve the quality of our software I think it's very important that we move generally in the practice of writing software towards declarative programming I'm going to come back to that a little bit and what that means to me so this is just a a quote from dyra who had a lot to say about formal verification he had some criticisms as many did but um I think largely in support overall of the idea of formal methods uh but one of my favorite quotes is that Simplicity is a great virtue but complexity sells better uh which I bring up only to say that this problem is not going away we can expect software complexity generally the complexity of the systems that we build to explode over the next decade I would say in the next two years right you may be May working on an application that's broken up into 300 microservices on your laptop by several different AIS who decided that was a great idea right these systems are going to escalate in complexity as we start to adopt artificial intelligence into our workflows already today they are so complex that we we could certainly measure them entirely for form verification but it may not in the end be worth the investment of effort because there are a certain number of states that we want to avoid in these systems in the defi space that one where they get to trade a token for all 9 billion tokens that's the one we want to avoid right so this brings back to that topic of declarative versus imperative programming and I have a quote on here from xcd pseudo make me a sandwich uh where guy's making a joke about getting his his friend to make him a sandwich in a comic but the idea is that um we very largely program imperatively these days um we have like a lot of computer science students I don't know some people come from different backgrounds we have a lot of Cs people out here you ever hear the um the Cs example where your professor's like hey teach me how to make a sandwich yeah you're familiar with this he's he's standing up there with a jar of peanut butter jar of jelly they do this often I'm I'm surprised if no one here has ever done this exercise but basically the class is test with coming up with a sequential set of tasks that will result in a sandwich right so it's like pick up the knife put it in the peanut butter right but we didn't remove the peanut butter lid so then he's stabbing the peanut butter right all these like comical errors that he makes as just this basic automaton which is exactly what we do in programming all day actually I I argue with a robot and get frustrated because it's too stupid to understand human reasoning because it is not a human and does not reason right what I'm doing is I'm telling it explicitly to pick up the knife to open the lid to put the knife in the peanut butter to pull some peanut butter out to put it over here it's a very involved process right what if instead I stated a certain number of things about the world that I wanted to be true and I let the software determine how to make that true so I declare about the world that a sandwich is peanut butter and jelly between two pieces of bread and it looks like most other sandwiches and I set in AI about the task of making that real right in the world of software now when we bridge this idea over we're talking about the idea that in the future AI is probably going to be riding most of the software I I know this isn't true for all of us yet but I think for many software engineers in the last year we've taken to using AI in our jobs full-time right and you think about what that's going to mean for us going forward from the perspective of formal verification and it's not great for the world generally this AI thing I think uh and we can talk about that another time but one of the things that it does a lot and is a real problem is that it hallucinates things right it will just make things up and it does this based on you know all of the all of the llm uh Magic but effectively it is intentionally randomizing itself at some level right that an llm is designed to intentionally randomize itself seeking better input it's part of this like self-training right and when we are building programs that's a real big problem because I'm not looking looking for your artistic interpretation of my popup right I'm not I'm not looking for what you think might be a good ux robot because it's going to be horrible I want a very specific thing and I want to Define it very specifically for it and I want you to give it to me and this is my biggest frustration with AI is that they will remember a thing and be convinced that you wanted the blue background and they just keep putting it back right but if you define instead about the state of the world look the page always has a red background now your robot can go back and make as many changes as it wants it can hallucinate and think that meant green it can modify your website in all sorts of other ways but at the end of the day if that test doesn't pass that the background is red then you're not done with your task you keep going AI right so this hallucination vaccination step I think is one of the primary values in the future of formal verification I don't want to Discount too much the value that it can add to your lives immediately today um the the AI component is certainly going to be relevant but right now there are people using formal verification to make sure that their smart contracts function the way that they they expect them to and there are a lot of Auditors out there who are using these tools there are a lot of Auditors who work at this company called Soro where I work who are using these tools this technology is available today many of the criticisms of it over time have been based on the fact that it was implausible to formally verify an entire program and we agree that may be actually true for most complex systems that's probably true it may not be worth your time to analyze every every dark corner and find every bug that could exist right but certainly the ones that are going to drain your entire pool and bankrupt your company instantly because you missed a thing with a human being looking at a contract and and I know a lot of these security research a lot of them they're brilliant they're really good but human beings are fundamentally flawed at this thing at just looking at a complex problem and saying yep we're good I don't think this is the future of auditing I don't think this is the future of writing software I spent a lot of my time arguing with the build process of JavaScript uh I don't hate JavaScript I don't hate any language whatever you use to build your dreams is fine by me but I want to point out that we write a lot of bad software over and over and over again we write the same bad software I have written implementations of lpad the thing that broke the whole JavaScript ecosystem that time these are the things that are going to slow us down as an industry in a time where we cannot slow down the people in this room are here because we believe in generally this decentralized dream that maybe we shouldn't turn our um our corporate world's leaders into gods and Kings right and then maybe we should we should hold the keys ourselves right we should we should seize the keys of production and I think that there is some urgency here in that the AI is coming and the AI is going to decide largely these algorithms that are being written now they're largely going to decide the future of humanity so we got one shot right now to put some rules in place think about Oso's rules of Robotics right these are the kinds of things that we need to put in place as invariants right now to protect our software and the stability of our software going forward not just so that we can move more quickly as an industry and be more productive in our work but so that we can event a future where we are being programmed by the programs that we write instead of programming them so uh with that I am going to wrap up and I thank you very much for your time I uh have a little bit of time for questions but I would much prefer to take them in the hallway so I'm just going to step down and invite you all to come forward and chat with me I'm going to hang out here as long as you like up on the stage and we can talk about all of that okay so thank you very much I appreciate you coming down take care I