Empowering Everyone: Taking Specialization Out Of Formal Methods | Daniel Cumming | ETHTaipei 2025

[Music] Hello. All right. Thank you everyone uh who's come to listen to this talk. I appreciate you coming here today. Oh, well my name is Daniel and I'm from runtime verification and today I'm going to talk to you about formal methods which is something that has largely been the domain of research over the years but is uh coming into industry and is being able to be deploy deployed at scale to projects and I want to talk about bringing that uh to developers in an accessible way.

So there's a couple of things I'm going to cover in this talk. I'm going to talk broadly about what formal methods is, what its goals are, and how we might be able to incorporate that into the developers timeline and or how to do it uh best into the developer timeline and then what the responsibilities are for tool developers in order to to make this ultimately accessible. So to define formal methods, formal methods is uh using mathematically rigorous techniques to specify and verify the correctness of software or hardware systems. I think that uh for the context of this talk, I'll be talking about smart contract development, but this is broadly applicable to software. I mentioned specification and verification there.

Specification is defining what the system ought to do. So when you write a smart contract, you might have some idea about what the behavior should be, but aside from writing maybe some design documents and documentation, there isn't a a mathematically rigorous description of what this system ought to do. However, if you want to prove that the code is doing something that you think it do uh you think it does, then you're going to need to mathematically specify what this what the behaviors of the code ought to be. And and once you have that a a proof verifying the program is is proving that the systems implementation that the code that you wrote is is adhering to that specification. So there's a bunch of different approaches to doing this.

uh four that I have listed here are model checking, interactive theorem proving, symbolic execution and abstract interpretation. So there's a pros and cons to each of these. Some of them differ in complexity, some of them differ in how much automation you can apply to them, and some of them have a tolerance for false positives. Abstract interpretation might tell you that there's a problem with the code even when there isn't. Uh if you've used static analysis tools, you might be familiar with this kind of thing.

It's an over approximation for correctness. But I don't expect that anyone here would be familiar with these kinds of approaches. But something that I expect you are familiar with is testing. So it might be good to ask how does this relate to testing? So testing checks concrete inputs one at a time through the system and it has the same goal as formal methods.

Both are trying to determine that the system is correct, that it's doing what you think it ought to do, but the scale is different. Testing is checking one input at a time. And so if you want to know that it works for all inputs, you're at a position where it's unless your code is on an extremely small scale of the range of inputs that can be provided. We don't have the computing power to test all of them. So you'll never be able to know anything about the inputs that you didn't test.

Formal methods is attempting to check ranges of inputs at one time. And so it tells us about well the aim is to tell us about the entire state space. And so I'll show a a visual description of what I mean by that. But a some preamble to that is we can think of the the EVM as a state machine. So there's some state that is getting manipulated.

It's undergoing state transitions. And so this state is like the ledger that's storing all of the the data and storage and transactions are sent to it and that creates some sort of state manipulation. And so if we think about these state manipulations that have happened in history, they're they're kind of like a straight line of what actually got written in. And it is true that some of these states that were achieved are are bad states that we don't like there. there was some amount of um there was some transaction that was provided which which moved the state into a position which was not the author's intention of the person that wrote the smart contract.

And so these these are bugs and and the goal for testing in formal methods is to try and imagine for all of the different states that are possible to branch out at this point, how can we identify the ones that have bugs and make sure that we we cut them off so that they can't actually be reached. And so testing goes through one at a time and checks them. But doing that doesn't tell you anything about the states you don't get to. And so you're really hoping that you end up selecting the path with the bug. And even if you're using fuzzing or randomizing things, you aren't guaranteed that if there's a really hard to spot bug that you're going to hit that path.

formal methods is trying to use uh a r a range of inputs like I said so you can reason over the state space is large and hopefully you're able to you you won't be able to rec reconcile these branches that have the bugs and so that will give you an indication of where some problems are. So if you agree with me that this is valuable then suppose the next point would be how can we introduce it into the developers timeline. So I think the developers timeline generally right now doesn't include formal methods and it looks something like this. Developers write some code they write some tests which find bugs and then they correct these uh bugs. the tests are passing and they might iterate on this a few times, add more features, make make things better, but eventually they're going to get to the point where their entire test suite is passing, they're satisfied and they're ready to go to something like an audit.

And so at that point control of finding the bugs shifts into the hands of uh some experts and those audits will probably find some bugs and then the developer goes back they write tests they improve their test suite the bugs get fixed and then even again another audit occurs but the what I'm trying to demonstrate with this graph here is at a certain point we tend to have this situation where the the autonomy of finding the bugs is handed off to experts and it's not in the hands of the developer to completely or to to attempt to completely find all the bugs in their code. If we introduce formal methods and and some projects are introducing formal methods because they're they want higher assurance than what the audit model is giving. Then at the point that they're satisfied that their test suite is passing, they can hand that over to uh an expert to specify and verify that the code works. And so hopefully they're going to iron out all the bugs or for the components that they're looking at and and these can be added to CI as the developer then continues that you know these proofs might fail. Hopefully generally testing is going to catch the bugs but but it might not and then if the proof fails it will be the job of the developer to try and understand why the proof is failing and correct it.

And while this is a massive improvement over the for the amount of assurance you get from uh audits which are like snapshots in time, it is a bit of an ask for the person to interpret why the proof is failing if they weren't the person who wrote the specification and verified it in the first place. And so I think we can do better than this. Although this is already an improvement, but really what we want is some sort of future where developers are specifying and verifying their own contracts or at least to some degree. And this is a bit of an undertaking. But on the positive end, if we are able to do this, we're enabling developers to find and catch their own bugs uh a lot more completely.

And if they're able to do well or include specification and ver verification in mind from the start, the process of of doing this should get a a lot smoother. They're already in a pretty good position in that in order to specify a program, you need to understand it well enough that you can write a rigorous specification. And the developers already know the code well enough that they're able to to write the code for it. like they they understand the business logic, they understand what the goals of the code are. That's their attempt to implement it.

So they're already predisposed to to be successful at this at least at the start. So then I guess the problem comes to is it possible for a standard developer with no training in formal methods to reason over this state space? And the answer to the question is yes, but I don't think it's an obvious yes because it depends how exactly are we going to present that information. And as I said, there's a range of different options available to us. And on the left hand side here, we have some code that's from the Isabel Solidity uh project.

And so Isabelle is a traditional formal methods tool which is really powerful for doing interactive theorem proving. And this is a really valuable project which is going to do great things for the ecosystem. But I think that everyone would agree that it's a bit of an ask that is really unachievable for a regular Solidity developer to interpret what's on the left hand side here in a meaningful way. So this tool is probably only going to be used by people who already know how to use this stuff. And so that's that's verification engineers.

So it doesn't really solve the problem of bringing finding bugs uh and and empowering users to find their own bugs uh using formal methods. So the thrust of that point was complicated tooling makes formal methods inaccessible for developers. But as I said, there's a range of different options available. And so uh I bring up this this is a paper at the top or it's the title of a paper with the authors that was done by Amazon. So they had a a team of engineers at some department writing software and with minimal oversight they were able to get all of these engineers to who had no background in formal methods to specify the software and uh verify the proofs and add these proofs onto CI there.

There was oversight I think of two verification engineers maybe one I can't remember if it was two or one and the whole department managed to successfully do this and the takeaways that they have in this paper are well there's there's a few points they make but some I think the important ones I want to bring up now is the specification needed to be in familiar styles and idioms to what the developer was used to. So if you were expecting developers to use some sort of specification language that was new, they were unfamiliar with it. It's it's too much friction. They're not going to be able to do it. They need they want to work in language they already know.

So if you're used to working with Rust, you want to specify using Rust or something like Rust. If you're used to using Solidity, you want to specify in something that looks like Solidity. And then verification. What they needed was the proof harnesses that they were using needed to be similar to unit tests because this is what they're familiar with. They know what a unit test is.

They know they're familiar with the concept enough that it's just an extension that that unit test is in in some way doing a proof instead of a you know as I said a symbolic range of values maybe instead of one input at a time. So the thrust of that point is research tells us that if we meet developers where they are at, they can pick up formal methods fast. So I showed the interactive theorem proving with Isabelle is is probably on the the more complicated end of how you could approach this. But I think on the less the or less complicated end to do this would be symbolic execution. Symbolic execution requires running a program on abstract inputs uh following each branch of control flow and collecting and reasoning the path conditions.

So said like that it probably sounds not intuitive what this is but I argue that everyone who writes software already does this. And why I bring that up is because if you've ever written an if else uh you know control flow branching statements then when you write this you're going to be thinking about this symbolically when you when you write this code you don't think about each uh like a concrete value you don't choose one value in a UN 256 you think of uh the relationship between what's happening at the guard of the if statement symbolically like if the balance is lower than the value you know that you're going into the branch And if it's not then you know in the else branch it's true that the value must be less than or equal to sorry the value must be less than or equal to the balance. And so then with that knowledge of the path condition you know that you're fine to minus the the value of the balance. So that's everything that's happening on the left hand side and developers are already doing this uh just not on the scale of what we see with formal methods tooling but it's a good sign that they're predisposed to do it. So we've taken this on board with our design philosophy for tools and uh I've got two examples of tools that we use.

So this is the solidity debugger that we make a runtime verification called symbolic. And so with the knowledge that people are probably able to handle symbolic execution and reason about things symbolically, we wanted to make a debugger that instead of just stepping through things concretely when you got to branching conditions, it was able to show you symbolically what would happen if you went down different avenues of that branching. And then in order to help you navigate the code having some sort of graphical representation that you could go around click to the nodes and ultimately get more feedback about the entire state space of what you're looking at. So this is us trying to meet developers where they are at. And another example of that is we have our tool control.

And so some design philosophy that we had with control is we want to do symbolic property tests. And how we what we wanted to do for that was make it so that we were asking developers to work with something they were already familiar with. This is a foundry fuzzing test which shows uh that some assembly in solidity that's doing m wad is equivalent to the solid a m wad. It's just an equivalence check. And the foundry fuzzing test will fuzz this uh you know the number of times that you ask.

But this is more than a foundry fuzzing test. It's also a control symbolic property test because the very same test that you would run with foundry is the input to control. This is us with the design philosophy of what are the devs already familiar with? We need to make the input to our tools the same as that. So if you run the same test with either foundry or control, it's valid input.

And running it with control or running it with foundry, you do forge test, it runs a number of times, it gives you the output. The only difference is really that you do control prove. And so this is proving it over the entire state space. If you remember that graph with all the branches, this is uh this is trying to be complete across that graph. So we have a lot of benefit uh for doing this in that we're trying to make developers have some access to these tools.

We can think of our tech stack works like this. we have an inner core of the the mathematics uh that that we use to encode our formal methods which we call matching logic and there's a wrapper around that called K which is the the interface that a language would be able to work with the mathematical core and as you can see this this is the ring so there's many tools around that that work at this at this level or or that that are building on this core and so KVM is the input to symbolic and control. And if you ever are attempting to work directly with KVM, you'll notice that it's it's if you haven't looked at anything like that before, it's probably pretty intimidating. It's probably pretty difficult. So our goal then with symbolic and control is that's the edge of the ring that needs to be accessible.

So there's a complicated core underneath that is mathematically rigorous and that's okay to be really really complicated as long as the way that you interface with it is in an intuitive and coherent way. Uh oh yeah that's that's everything that I got to talk about today. So thank you great talk. Any questions? Okay, this gentleman has a question.

Uh, thank you for the great talk. I'm a little bit confused about the comparison between foundry and control or symbolic. Are you trying to saying that what we're doing with foundry fuzzing test is kind of a form of what you're trying to do with symbolic or control? I don't remember which one. So uh symbolic and uh control are distinct.

So one is trying to do uh symbolic debugger and one is trying to do uh symbolic execution and and uh end to end automate end to end automated symbolic execution. So you have some idea of uh a property test that you oops that you encode with foundry. You know, there's going to be some assert statement down the bottom which is representing some sort of property and we want there to be you push a button and instead of it running that concretely, it does a proof and it shows for the entire state space that property holds. symbolic is different in the sense that on the path of doing that there's going to that I talked with control there's going to be many states and many branches and avenues that you go down and the representation that you get with that in control it you can look at the intermediate states in some fashion but it's not really accessible to developers it's going to be this this state representation of KEVM like I mentioned but that's really useful for developers is to be able to inspect what's going on in these branches. And so this is a much better representation for that is being able to see where the branching occurs symbolically through the source code uh at that level.

And so this is still formally tied back. It's just a it's it's a different way of representing it and it's got some different goals. Does that make sense? Yeah, it does. Thank you.

Cool. Cool. I think we can accommodate one last question. Anyone has questions? Okay, that gentlemen, great presentation.

Excuse me. Great presentation. Thank you. Um, how how would like a working solidity developer use these tools symbolic and control kind of in their development cycle? Like what would that look like?

Yeah, TR that's a that's a great question. I like that one. Uh I think that symbolic is something that can be introduced really early into the picture and why I say that is because it's interactive across the the states and as you're developing the code and increasing the complexity you can look at how much these graphs and complexity and the factor is changing and you can look at the leaf nodes and the interate intermediate states along the way. Control on the other hand is going to run uh a proof and it's going to be quite a large proof obligation that you give it with complicated code and the state space explosion that we get with formal methods means that this could be this could actually take quite a bit of time to try and do the proof. So generally if you're going to try and prove something with formal methods you want to be pretty confident that any easy to find bugs are already gone.

So this working with Foundry means that it would be far better to use Foundry to blast away statistically most of the bugs. You're going to hit most of the bugs, clean things up. If you're quite confident then that this this is indeed correct code, you can run a proof and then it comes to the point that you have to be able to wrangle the output that comes back from that proof and get that working. But uh so control late in the development cycle, symbolic early and through. Got it.

That's that's really helpful. Thank you. Cool. Cool. I think we still got time.

So maybe one last question before we wraps it up. Okay. More. Okay. If not then.

Yeah. I really really like this talk. Thanks for all the details about how to use these tools. I think it's really helpful. No worries.

Thank you everyone. Yeah. Thanks to Daniel. [Music]