Transcript
Hillel Wayne: I have a bit of a weird job. Companies pay me to find bugs in systems that don't exist, or more specifically, don't yet exist. They come to me with some idea for a system they want, but they're also afraid the system might lose them customers if it goes wrong, and they ask me to look at their description and tell them if there's a really bad bug somewhere. Growing up in extreme programming and agile shops, this felt verboten to me when I first started doing it. After all, we all know that we can only find bugs at the very end when we have the whole coding system that we can test, possibly in production. It's actually a relatively simple process that all of us can do. To show you that this is just even possible in the first place, let's walk through the thing doer.
The thing doer does a thing. It first checks to see if the thing has been marked done. Then it marks the thing as done. Then it actually does the thing. Would anybody like to shout out the problem with this thing doer? Yes, there, you found a bug in something that didn't exist. The problem with this is that we all know this is not how an actual system works. The actual system is going to look like this. Doing the thing might fail. If it fails, we have to retry. If we retry, we get to this point where we check the thing is marked done, and see, it's been marked done. Then we just never do the thing. That's a bug. The client might try to fix this by saying, what if we instead do the thing and then mark it as done? Now if we fail and we retry, we have it marked as done, so maybe we can actually get it finished.
This, though, has a new bug. It even has this bug if we even remove the possibility of it ever failing, this bug is the two-thing doer bug. If we have two thing doers, the first might do the thing, but before it marks it as done, the second one might start up and do the same thing, leading the thing to being done twice. This also has a bug, a different kind of bug. Who here has built anything that looks like a thing doer? Because this is an abstract version of a very real system, one that I see very often in our designs. I've also seen it fail many times in the real world. I have seen package senders that end up sending people two packages for the price of one, which is very good for the consumer but makes the company a little bit sad. I have seen scheduling systems that can end up accidentally scheduling two people to the same slot, and I really don't want to be shouting over somebody to try to get my point across.
Although I might want to listen to their talk, which would make it hard to give mine. I've even, and this was the worst I saw, something that allowed you to install an app on a device twice, which doesn't seem as bad as the first two. I'm thinking a very particular system where if it was trying to install something and you told it to install the same thing, it would first stop running and start randomly deleting files on the device.
Scope - Formal Methods
Hopefully I've established that this is something we all can do implicitly and intuitively, finding bugs in descriptions of systems. My work is an explicit version of this, it's called Formal methods. The way of taking systems, encoding them in mathematical notation, and then using tools to find errors in those systems by exploring the entire state space. I've been doing this for about 8, 10 years now, and I've talked about it a lot. I found out two things about this. One, any talk about formal methods can only have one possible conclusion, which is you should try formal methods. This is a really terrible conference talk, though, because most engineers do not need formal methods in the same way that most engineers do not need to learn graphics programming or geographic information services. It's useful to a lot of people, but not useful to far more people. Two, using formal methods has changed how I think about regular software in ways that I think are actually quite useful for people to understand.
Instead of just talking about formal methods, I want to talk about the ideas I've learned from this that I use in everyday coding. We're going to be looking at three different aspects, the ideas of properties, verification, and environments. Or, to be a bit less technical, what it means for systems to be correct, how we can verify this correctness, and what is needed to make correctness possible in even the first place.
Properties
Let's start with what it means for a system to be correct. To formalize this notion, we have the idea of a property. A property is something that should be true of a working system. If it is false, then the system is wrong in some way and needs to be fixed. Properties, notably, are Booleans. They are either true or false. They are not partially true. An example of a property is that we have 99.999%, five nines of uptime. This is something that is verifiably true or false. If we are down for more than five-and-a-half minutes a year, our system does not have this property and we need to make a more sophisticated system or migrate cloud providers, depending. This is a property. It is also a relatively complex property that is hard to verify. We are often interested in automatically verifiable properties that we can easily check.
An example of this might be that all the messages we send in our system follow the appropriate schema. I would recommend checking out Ian Cooper's talk. That is some of the things he was talking about, the ways of enforcing this property in his systems. Properties get much more detailed than that or much more low level. Even something like a unit test is a property. Testing that max of 1, 2, 3 as 3 is the property that a given input always gives a certain output. If your system does not give that output for that input, something is wrong and must be fixed. Our thing doer had two properties that we talked about at failing. We don't do the thing more than once. Or a safety property, something bad that we want to prevent. We do the thing at least once. Or liveness, something good that we want to make sure happens.
I said that properties are Booleans. This leads to a very interesting consequence. Take the property that a system can handle 10,000 queries per second. Think of the set of every possible system you could build that to some degree of abstraction satisfies this property. Now take the property of can satisfy two queries per second, every possible system that can satisfy two queries a second. The set of properties that can satisfy 10,000 queries is a strict subset of those that can satisfy 2 queries. If a system can satisfy 10,000, it can satisfy 2. We would say that being able to satisfy 10,000, having this property, implies you have this property too or implication. This is an extremely useful thing that comes out of mathematics.
Some other examples of properties that satisfy this is that if you have no memory errors, this implies you have no use-after-free errors. If you have exactly once delivery somehow, you have at least once delivery and also at most once delivery. Something like GDPR compliance implies that you have cookie banners on every page of your site. Notice that these properties on the left-hand side are harder to satisfy than the properties on the right-hand side. Also, if you know you have the property on the left-hand side, you automatically have the one on the right-hand side. This gives us a notion of property strength. The properties on the left-hand side are stronger than the ones on the right-hand side. Some properties are stronger than others, and this is really important for verification. Because if we have a property that is strong and we know it's satisfied, like a test that a user can buy something with a coupon, if this passes, we automatically know the system has all the weaker properties too.
You can apply coupons and you can complete orders. If you run this test and it passes, you don't even need to run these tests hypothetically. The other consequence is actually more important, the consequence of the contrapositive. Notice in this space that there are three distinct regions. The region that satisfies both 10,000 and 2 QPS, the region that satisfies 2 but not 10,000, and the region that satisfies neither. There is no region that satisfies 10,000 QPS but not 2 QPS. If 10,000 implies 2, 2 not holding implies 10,000 doesn't hold either. If a system breaks at 3 queries a second, it's clearly not going to handle 10,000. This is called the contrapositive and leads to something quite interesting. If we have a set of weaker properties and we know one isn't satisfied, like you can't actually add shipping, we don't even need to look at the stronger property, we know it doesn't hold either.
If you're trying to figure out what's wrong with your system, which is more helpful, knowing that this test fails or knowing that 70 of these tests pass and this one fails? Which will isolate the error more? The second one. It is pretty much universal that strong properties passing show that a system is correct, while weak properties failing show why a system is incorrect. This actually explains a lot of practice in how we verify systems. Think about the testing pyramid. You have end-to-end tests, just a few of them, and then some more integration tests, and then a whole lot of unit tests. The reason we do things this way, there's many reasons, but one of the big ones is that often we are trying to debug broken systems versus verifying correct ones. This means that the unit tests provide us way more information about what could be going wrong than a single end-to-end test. That's why we often want many more of these.
In our thing doer, we had two versions of the thing doer, two different systems, and two properties. We don't do the thing more than once, and we do the thing at least once. The next step, now that we have those properties, is to figure out how we can represent a system in a way that can verify them or show them wrong. As before, we can do this intuitively, but the goal here is to find some sort of rigorous process. Then we can apply it to way more complicated systems where this might not be as evident. The way we do this in formal methods is to first encode the system as a set of logical formula, and then encode the properties as a set of logical formula, probably linear or temporally logically formula. Then we try to run some sort of model checker, SMT solver, or proof assistant to do this.
We're not covering any of that, because again, this is not about using these tools. This is about thinking like these tools. How do we actually represent a system in a way that can be verified? The goal here is abstraction. We want to find the simplest possible system that covers the expected behavior. The simplest system will have fewer error modes than the more complex real-world system. At the same time, if there's an issue in the small system, there is definitely going to be an issue in the larger system. If thing doer is going to fail, the package sender is also going to fail and probably much worse. This isn't perfect, but it is a very cheap way to find very dangerous bugs quickly.
At the highest level, what is the actual state of the thing doer? I'm going to propose three kinds of state. The first is, since we're running an algorithm, the step of the algorithm we're on. This will be an enumeration, check, mark, do, and done. If we're on the check step, that means we're about to do check. If we're on do, we are about to do either do or fail. We also have whether or not we have marked the thing as done. This will be a Boolean. In the real system, it will probably be like a database record or a file somewhere or a date timestamp. A Boolean is all we really need to do this kind of analysis. Then, finally, we have how many times a thing has been done. It's not enough to make this a Boolean, whether it's been done or not, because we want to make sure it's not done twice, so it has to be an integer.
This is all the state we really need to represent the system. In looking at this, there's actually a really useful insight I already see here, which is that step and marked are machine variables. They are internal to the system that we design ourselves. Done, the number of times something is done, is a world variable. It represents some exterior part of reality. The difference matters a lot to us, because machine variables are entirely in our control, because we can design the system however we want, we can do whatever we want to these values. Whereas the world variables, we have very limited control over. We can do some things, but not anything we want. If I really want to, I can design a system where marked goes from true to false again. If number of times done is 2, I can't make it 1 again. I can never unsend the package.
We have our states, and now it's time to figure out what our system can actually do. The first thing to do is figure out what are the initial possible configurations that the system can be in. There is only one, that we're on the check step, we have not marked it as done, and we have not done it any number of times. From here we ask, what possible evolutions can happen in the check step? This is deterministic, meaning there is only one possible thing that can happen in this step. We go to the mark step. We have seen that marked is false, so we go from check to marked as opposed to from check to done. From here again there is only one possible step, we go from mark to do. Here though, we have two possible things that can happen, we can do the thing, or we can fail.
This is called non-determinism, when more than one thing can happen from a given point in time, a given state of the system. We can go to either the done step, where we also set the number of times things has been done to 1, or we can fail and go down here, back to the check step in a retry, where marked is true and it's not been done zero times. Once we've done this, we have to explore both possible states, figure out what can happen from those situations. Both of these are once again deterministic. From the right-hand state, we can try to retry, we go back to check, but we see it's already been done, so we go back to done. Similarly, over here, if we retry over here, we see it's already been done, so we go to the done step. If we try to retry over here, we go back here.
This is every possible configuration of the system. We call this the state space. Each of these individual things is a state, and each state has state. The word's overloaded. Every possible path through the system is called a behavior. I will try to use the word path because it's more colloquial, although I think behavior is the more technical term.
Verification
Now that we have our state space, we have to verify our properties. Starting with we don't do things more than once, that's a much simpler property to verify, because that is what we call an invariant, something that must be true in every given state. I would write it mathematically as it is always the case that the number of times it has been done is less than 2. If you look at actual notations, they use a weird squared thingy, but I'm going to use always to be explicit. To verify this property, we just have to go through every possible state and see whether it holds this property. For example, this state over here, we're done at 0. That holds it. Same with this state, same with that state, same with that state, same with that state. Every single state satisfies this, so this holds. Now as to the bottom property, what we call liveness.
This is not a property on states. If it was, we would immediately fail in the initial state, because in the initial state, we have not done it. It is actually a property on paths. In this top path, we enter a state where it has been done. Therefore, this path satisfies that property. This path on the other hand does not. If we go down to this state over here, this check true 0 state, there is nothing we can possibly do that would get done to be 1. Because at least one path does not satisfy this property, it does not satisfy to the system. There is the potential for a bug in the real world. V1 satisfies one property but not the other. That's bad. What about V2? In V2, instead of check, mark, do, we check, do, mark. The new state space looks like this. It seems from the state space that we now satisfy the below property. Even if we fail, on the do step, we go back to a step where it is possible to still reach the done step. It seems like this property is satisfied. If you leave now, you're going to be horribly misled.
Before we explain why you'll be horribly misled, we have to talk about the other property, the safety property up above. I said this fails when we have two thing doers. The question is, how do we use this process of exploring the state space on two thing doers? There's two aspects to this. The first is to decide what is a local variable to each process and what is global to the whole system. World variables, like the number of times something's been done, are almost universally global variables. They are shared between all processes and the external world. On the other hand, machine variables can depend. I will argue that these are probably sharing a database somewhere, so the mark is going to be a global variable. The step each process is on is local. Each one has its own step, and we start in check, check. Marked is a global variable that's false, and the number of times it's been done is 0.
The next question is, how do we represent concurrency? How do we decide which process happens first? That's just non-determinism. I can say either the blue process happens or the red process takes a step. From here, I can say red happens or red happens. I can just keep doing this. Eventually, I'll reach a point where the number of times this has been done is 2, following blue, blue, red, red, or red, blue, blue, red, or blue. We can say that this property up above is not satisfied by the thing doer mark 2. That is property checking.
In practice, though, we don't usually do things this way in our heads. The reason why is because usually we're not dealing with 12 states, but 800 or more likely 10 million or 100 million states. This is how the tools often work. This is something that can be done by tools. It works the same way. We take an initial state, then we find every possible succeeding state from that initial state, and then we repeat the process in every state we found. Sometimes this will bring us back to a state which we've seen already, which is fine. It just means that we have found a different path to the same state. Then we just keep doing this, hoping that our state space is finite. Eventually we have seen the whole state space, and we can check it for properties. I covered this brute force analysis because that's how tools work.
I think it's the best demonstration that this is something that is totally possible, not magic. Again, this is not how we do things in our heads. When you do enough formal methods, you start to develop an intuition for how things can go wrong. The way this intuition works is by taking advantage of something called adversarial non-determinism, or the gremlin. You take every source of non-determinism in your system, things like randomness, user inputs, concurrency, whether or not us-east-1 decided it should be better or not that morning, and at the abstract level replace them all with the gremlin. Whenever you have a non-deterministic choice, you ask the gremlin what should happen, and the gremlin always gives you the worst possible answer. You can get pretty good at doing this in your head once you've done enough of this, just always figuring out what's the worst possible thing that can happen.
This gremlin is why this system does not actually satisfy the below property. Because think about this, we start in the check step, we go to the do step. Then here comes the gremlin. We ask the gremlin, what should happen? Should we do the thing or should we fail? The gremlin goes, fail. Ok, we're back here. Then we try again and we go to the do step. We ask the gremlin, what should happen? Should we do the thing or fail? The gremlin goes, fail. Then we get back to the check step, and we go to the do step. We look at the gremlin, and we decide, no, this is just not satisfied. Simply put, if we have any kind of loop like this, it is possible for us to enter the loop an infinite number of times and never actually get to a valid state. That's the easy case.
The much worse case is this. This does not satisfy liveness either, even if we remove the fail state. How does that work? We get to the check state. We go to the do state. Then the gremlin pops up. We're like, gremlin, what are you even doing here? There's determinism here. There's not even anything that can happen. The gremlin goes, like, and you go, ok, gremlin, what's going to happen? The gremlin goes, meteor. Or more realistically, a server outage, or a timeout, or latency just being high enough that you don't get a response in the window you want, or any number of things that can cause a system to just not do what you think it needs to do.
Environment
This brings me to the last aspect of this talk, environment. Environment is all the assumptions that need to be true for our system to work. In the first version of the thing doer, we need the assumption that the system never crashes to guarantee liveness. This may or may not be a good assumption, but it probably is one we have to have. Even think of something like trying to click a clicker. You have to assume it always works because it is totally valid for it to have the error that you try to press a button, but before you do, it catches fire. Without the ability to say that things always make progress, you simply cannot have any properties at all. This still reiterates that properties are things outside of our control. Often, these assumptions come from other people's systems we don't have control over. If a vendor decides to switch from always consistent delivery of messages to eventual consistency, what can you do about that?
You can change vendors maybe, but you can't tell them to go back to the old behavior. This is a really defensible assumption. If we add in the fail state, we now need a much stricter assumption that do thing never fails. This is a lot less defensible. If I see a client say, "We're just going to make this assumption that this never ever fails". I'm going to be like, "Your system has a bug", just saying. This is something that might push us to using V2. In this case, in V2, we no longer need the assumption that do thing never fails. We could have a much weaker assumption, that do thing fails only a finite number of times. Even if we fail at this step a million times, we still, on the million and first, go past this. We're done. We have satisfied liveness. This kind of really fine-grained assumption is what formal methods is really good at. It really forces you to think about all the kinds of assumptions of so many different types that go into a system. I would also like to point out that do thing never fails and do thing fails only a finite number of times are very qualitatively similar properties, if not quantitatively.
This brings us back to strength and weakness. Some assumptions are stronger than others, just like some properties are stronger than others. No failures is a stronger property than finite failures. Strong consistency is a stronger assumption than eventual consistency. When we have stronger assumptions, we can have stronger properties for the same level of sophistication of our system. Correspondingly, weaker assumptions can be compensated by system design. One good example of this I think about is I used to work for a company where we knew for a fact that every single one of our users would stop using our software at 4:00 New York time. This made deployments extraordinarily easy. We could just turn off everything around 6 p.m., update it, and turn it back on. We had a very strong assumption that made it easy for us to guarantee deployment properties. Imagine Google doing the same thing.
Just imagine it. It would be very funny to imagine. Another thing, though, is that different systems require different levels of assumption for different properties. It's not monotonic. A system design doesn't make all properties necessarily easier to guarantee for the same assumptions. We see this in version 2 again. In version 2, we needed a weaker assumption to guarantee liveness but we need a stronger assumption to guarantee safety. We need to assume there is only one thing doer acting at a time. It might be possible for there to exist in V3 of the thing doer, where V3 does not require either of these strong properties. It might be able to work even with only finite failures, but also guarantee safety even if there's more than one thing doer. That system, if it exists, is probably going to be a lot more sophisticated than either V1 or V2.
I've found empirically that there's this relationship between sophistication of the system, the properties you want to guarantee, and the strength of the assumptions you have, where either one of these can be fixed and the other two change based on that. For example, if you wanted to guarantee liveness for the same level of assumption, of say a message being passed, like are all messages processed? You can actually do that, even with weak assumptions, by weakening the property. From all messages are processed to all messages are either processed or go into a dead letter queue. Similarly, if you look at something like a spaceship, just off the top of my head, a spaceship cannot even assume that the RAM is going to be consistent. It's constantly being flipped by cosmic rays and radiation effects. They have to have a much more sophisticated system for the same level of property.
One of the other consequences of this is that weakening assumption often weakens the properties you have. If you take a fixed system that works and guarantees all your properties and then weaken one of the assumptions that are currently in this operating environment, it may not satisfy the properties it started out satisfying. I find this often leads to an enormous amount of bugs in practice, where people build a system for an operating environment, and it works, and then the operating environment changes. I keep going back to this example because it's the one that I have the most vitriol over. When a client changes a database from saying, ok, we're always going to give you updated information, to, we're going to give it to you five minutes from now maybe, we'll be consistent at some point. We built that depending on it being always consistent, strongly consistent. When it switches to a weaker assumption, our properties start failing. Theirs might be satisfied, ours are not. Those are three of the perspectives I use very often coming from formal methods.
Summary
In a summary of what I've talked about, systems have assumptions and properties. These can be related in terms of strength. Some properties are stronger than others, and some assumptions are stronger than others. For a given property and assumption, the system sophistication depends on both these things. A system needs to be more sophisticated to handle a stronger property, and needs to be less sophisticated given a stronger assumption. Strong properties show correctness. When they pass, we know our system is correct. Weak properties show incorrectness. They're used to debug why things are going wrong. We can look at a simplified model to find a real-world bug in the system. Then, finally, beware of the gremlin. I hate the gremlin. Ultimately, a lot of this comes out of mathematical analysis of software. We don't necessarily have to do this mathematical analysis ourselves, but we can still gain the benefits of the things it gave us. We see this in a lot of fields, in formal methods, in functional programming, in type systems. I find the mathematics behind this all really cool, and I'm glad that it actually gives us so many benefits.
Resources
I want to talk about a couple of resources. If you've decided after this whole talk that's not about formal methods that you just really want to learn formal methods, I'm sorry, I failed. I do have this resource that I've been working on called learntla.com, which is designed to teach one such method called TLA+, which is relatively popular in the industry. It's pretty good for this kind of concurrent system and finding bugs in that. It's not the only formal method out there, though. There's not really like zealot wars about this. This isn't like Emacs versus Vim. If you come to me afterwards and you just talk about the system you have, I can tell you whether this is the most appropriate thing or recommend resources for another one, like Alloy or P or Quint or PRISM. Or you can just hire me to work with you.
I do that too. The other thing is, though, as mentioned, I've really been fascinated by how we can derive useful insights into everyday software engineering from mathematical perspectives. For that reason, I've spent the past three, four years working on this book called "Logic for Programmers". It covers formal methods, but also things like property and stateful testing, design by contract, SMT solving, logic programming. If this is something that might interest you, I've actually done the first printing proof to actually make it into a physical real book you can buy. If you're interested, you can buy the PDF of the current version, which will automatically update to the final version when it's done at this link for $10 off.
Questions and Answers
Participant 1: Do you find a difference applying the technique of formal methods in legacy messy systems versus brand new starting from scratch Greenfield projects?
Hillel Wayne: Yes, actually. It's a lot easier to apply it in Greenfield. There's this interesting thing that happens in legacy systems where it's easier to demonstrate the value of it. The reason why is because in a Greenfield system, you can't really argue that like any given bug it finds is actually a realistic like, we would have found that later. In a legacy system, you can be like, I modeled our old system that had this critical bug, found it in two seconds, and then show that, ok, now that we can establish it can find the real bugs that we have faced, let's use it to model past changes to that. That's actually how I got started doing this. There was like systems that were going horribly wrong, and we'd basically make a patch, and they'd go horribly wrong, and they'd make a patch and go horribly wrong. Then, when we were thinking of another patch, I was just investigating these methods. I was like, ok, I have managed to reproduce the past five things that went horribly wrong in 50 lines of spec. This new patch has something else that went horribly wrong. Let's not do it just yet.
Weakly: One thing that I'm curious about is, when we talk about these properties, when we talk about proving things, it's often easy to show it or to demonstrate it or to curate in a small isolated component. If you have multiple different components, and you want to reason about them as a whole, groups don't compose, properties don't necessarily compose. In the real world, what strategies have you found pragmatically for addressing that in a way that works?
Hillel Wayne: Generally, this is like a big question in the space. This is a big problem in any kind of space. Things can be independently correct, but interact in ways that make them all break. This is known as feature interaction or boundary error. There's a really great book by Nancy Leveson called "Engineering a Safer World" about trying to find these issues after the fact. That's really the best that we can do for the most part. In formal methods, the way that we can do this is by basically titrating the amount of abstraction we do. We can make a really abstract system of all of the components working together, and then we can do what's called a refinement to take one chunk of that global system and make a detailed version of that. Then plug that back into the abstraction to see if it behaves correctly with everything else still being abstract. You can do this progressively. It's just really annoying and really hard to do because it's really complicated, and you're dealing with multiple layers of abstraction. It's not fun, but it's possible. If this was fun, a lot more people would be doing it.
Participant 2: You were talking about correlation between assumptions, properties, and sophistication of the system. I wonder, sometimes it's just impossible to meet the properties if assumptions go weaker. Sometimes it's possible by making systems more complex. Do you have any tools in formal systems that helps to answer that question? Is it possible or not to change the system that way so it can meet properties with weaker assumption?
Hillel Wayne: Is it possible for methods to tell you whether if an assumption is weakened, it's possible to fix it with a more complicated system or if it's impossible?
Participant 2: Is it possible to fix it with a change to the system without lowering the properties?
Hillel Wayne: There's two answers to that. There's the theoretical answer and the practical answer. The theoretical answer is, no, that it's not possible because that basically gets into like, how do you prove anything? It is possible to weaken assumption in a way that makes the property always impossible to verify, but it's not easy to necessarily show that's the case. That's gets into like, what is a proof? How do we prove anything? In practice, I found it's very easy to run, for a given system, multiple layers of assumptions and changes to it. You can say, ok, these properties always hold in our system design, these properties hold if we have this assumption. If we have this assumption, which is weaker than this assumption, this weaker version of these properties hold, too, but not these stronger versions. If this property is weakened, this refinement of the system satisfies the stronger property. It is possible to do that through engineering effort, but you can't automatically deduce that something would be impossible.
Participant 3: Unfortunately, I mostly work in non-deterministic systems, like agents or machine learning models. How much of this can be applicable? Can you measure the potential state space of the solution space or something like that? Are there methods available that help find these failure states before the agent inevitably trips up into it?
Hillel Wayne: I think the challenge with agents is that it's kind of a non-determinism that we really haven't seen before. We think of non-determinism as being like A or B can happen due to like the confluence of real-world factors. I feel with AI, it's to some extent like, it could do A or B. Why? Temperature. There hasn't yet been a lot of work in applying formal methods to make the agents themselves work correctly. Most of the work has been in either making sure the code that agents generate is valid or making sure the pipelines that the agents work in are valid. Actually verifying the agents themselves, it's not yet been established how to do that.
Participant 3: I was thinking maybe something like if you've got the trifecta of you can have stuff that can be exported and you could find those links and the potential combinatorial, like if you combine three APIs and you give an agent that, you may not immediately get an error, but you've created the potential.
Hillel Wayne: I think that that can be thought of as like an error in the three APIs. Like if a human uses three APIs, could an error happen? If a poorly written program uses those three APIs, could the error happen? In that case, I think that is verifiable. The agent itself is something that I cannot like give you a professional answer on without misleading you and myself. I do not have the expertise to really speak about that. Agents and APIs, that's the newest dumb version of Dungeons & Dragons.
Participant 4: Moving back to the world of systems that are supposed to be deterministic, is there any work on deriving properties or assumptions from the source code or the comments, or anything like that?
Hillel Wayne: Yes. A couple of ways we can take this question. The first is, can we generate a specification from the source code? There's actually been some really good work of using LLMs to do that. The other thing is, if we have a deterministic system, it is possible to just prove it directly correct with the code itself. That gets into a space called the formal verification of code, which is its own entire can of worms. Like, you'd be using tools like Dafny or Frama-C or SPARK to do that. Either a dedicated language that can be directly proved to be correct, or an augmented harness that goes on an existing language, like Frama-C on C code, to prove existing C code correct.
Participant 5: I've seen in my workplace folks using skills to try and automate some of these initial bug searches and security reviews and stuff like that. Have you seen in your experience people successfully try to adopt formal methods through skills using AI? If you have, have you seen it go successfully or poorly?
Hillel Wayne: One of the things that's been really interesting about the new LLM age is that it's revealed a lot of revealed preferences to us. One thing it's revealed is that a lot of people really want to ruin other people's day by putting slop on the internet. It also has shown me that a lot of people really want to use these formal methods, and they're just intimidated by the skill threshold required to get into it. There's been a lot more specifications, both of code and of systems being written with LLMs, which is a problem because they're really bad at it. The biggest problem with LLMs and doing this stuff right now is that LLMs are just really bad at figuring out properties. They cannot do liveness at all, and often their safety properties, their invariants are things like, if X and Y is true, and I know X is true, Y must also be true.
That, again, might change. These things get way too good, way too fast, and my answer could be wrong. Right now, it requires somebody who's already experienced in doing this stuff to get an AI to do it well. If you are experienced, it does save a lot of boilerplate and a lot of pain, and I love using them. I feel bad about loving using them.
Participant 6: You mentioned how your formal methods background helps you to identify weaknesses in the systems. Did you build an intuition how to build correct systems from it as well, I wonder?
Hillel Wayne: I think so. For example, one thing, I now hate any kind of graph data with a burning passion. The cycles, they're everywhere. I've definitely also noticed that there's more of like an intuitive sense of like, ok, this is going to fail because this has a race condition, so how can we design the systems that way? This race condition doesn't matter. I feel like I built that intuition, but it could also be the case that I've built that intuition, but it's totally wrong and I'm just overconfident. I don't want to say like you too will become perfect at distributed systems if you do this.
Participant 7: Is this a time-consuming effort?
Hillel Wayne: Yes. It is time-consuming, but with the goal of being money-saving and either a few days of specifying, saving you a couple weeks of development or saving you a couple weeks of trying to tell an angry customer, "No, please do not cancel. I'm sorry we lost your data, but we won't do it again". It is a time investment.
Participant 7: Do it early then you can save money.
Hillel Wayne: It will be time-consuming.
See more presentations with transcripts