Formal methods with Hillel Wayne

Speaker A: There's a popular theory going around that AI will finally make formal verification go mainstream, because when machines write the code, humans will need mathematical proof that it's correct. Today I'm talking with one of the best people to respond to this, Hillel Wayne, a former methods consultant. He's taught tla, a popular formal specifications language across the industry, wrote the book Logic for Programmers, and will soon be joining Antithesis. In today's conversation, we discuss the Crossover Project Halo's research, interviewing 15 traditional engineers to answer the question can software engineers also be considered real engineers? How AWS used tla an overview of how Amazon found a rare bug inside of DynamoDB using this formal specifications language, a deep dive into property based testing, and why this is the middle ground that most engineers should probably adopt, and many more. If you want to understand more about formal verification and get a sense of whether this approach could go mainstream with AI, this episode is for you. In today's episode we'll get to the does it make sense to use formal methods to verify AI written code? As a spoiler? The answer will be Proper formal methods are an overkill for this, but lightweight formal methods can actually be helpful. This is where I need to mention our presenting sponsor, Antithesis. Antistesis verifies your system's correctness by running your whole system in hostile simulation and finding bugs. It does this by using an approach called Deterministic Simulation testing, or dst, which AWS distinguished engineer Mark Brooker and Ankur Desai have described as lightweight formal methods. Setting aside Antithesis for a minute, if you as an engineer want to get more serious in verifying that your system works as intended, your best bet would be to use lightweight formal methods. Now back to intesysis. Antithesis turbocharges testing by running your whole system under aggressive fault injection. Imagine Antithesis has hundreds or thousands of versions of the Mario game, running each instance aggressively, trying to break the game with increasingly weird input combinations. With antistasys, you can specify properties at the whole system level and antistesis will actively try to disprove them. So you can be confident that if your system holds up in Antithesis, it will hold up in production. There's good reason teams like Jane Street, Fly IO and the ETCD community rely on antithesis. Head to antithesis.compragmatic to learn more. So hello, welcome to the podcast.

Speaker B: Thank you so much. I'm really excited to be here.

Speaker C: It's so nice to have you here. I was curious your very well known for formal methods, for programming, for logic, for all of these topics. But how did you get into tech?

Speaker B: So to start, I never really saw myself as a technical person. I like computers growing up, and I did a tiny bit of programming. My father was a programmer. He taught me Visual Basic, but I always wanted to do physics and math. That was like, my dream. I put in my college application. I want to listen to the heartbeat of the universe. Don't ever take advice from, like a, uh, high schooler for writing. Just, just saying. But after about three years of doing this in college, I realized that I kind of liked the idea of physics, but I didn't enjoy doing it, and I couldn't see myself doing it for 50 years. What part I did enjoy, though, was the programming in the labs. That was the most fun part to me. So I thought, well, if this is what I enjoy, why not try to do it full time? So after college, I left for San Francisco and became a, um, developer, a Ruby on Rails developer in education technology. After some time, moved back to Chicago. And then in the course of the next job I was working in, also in education technology, I fell into my current niche, which is formal verification and formal methods.

Speaker C: The first time I came across your writing, because you write a blog, a pretty regular one, and I really enjoy your writing. The first time was with the crossover project. This was a project where you attempted to answer, are we as, uh, software engineers, actually Engineers?

Speaker B: Yes.

Speaker C: Can we talk about this project?

Speaker B: Absolutely. So I guess I should probably start with the motivation, which was I've read a lot of books on software and I've read a lot of online articles about software. And one of the favorite things that software developers do is argue about whether it should be engineering or not. Right? And there's the camp of people that say, well, we don't deserve to call ourselves engineers. We should not. They are so far above us, we shouldn't even, like, consider ourselves in the same space. And then there are the people who are like, what we do is so special and so unique. Engineering doesn't have anything on us. They can't hold a candle to what we do. You see books like Software Craftsmanship, which talk about how like, oh, engineering is this really boring, slow field and software is this incredibly creative, special, wonderful thing. I was very firmly in Camp 1. I thought we were not engineers. We didn't deserve to call ourselves engineering, anything like that. What I do for work is really carefully analyzing software systems. And I thought, ah, uh, this is real engineering, and everything else is not engineering. Then I found this talk by Glenn Vanderburg where what he did was he read a bunch of engineering books and compare them, compare them to what we do in software. And he said, actually, this looks really similar to what we do in software. And I thought, that can't be right. I need something more rigorous. I'm going to have to talk to people who did both engineering and software development and see what they say. And they all agreed with him. So I was wrong. We're engineers.

Speaker C: Can we go a little bit into it?

Speaker B: So, uh, as I started talking to the first people, I realized that this was a much deeper project than I ever expected. And I, I decided I needed to have as comprehensive a look at traditional engineering as I could possibly get. There are many kinds of engineering. There's not just building bridges, but there's designing circuits, there's figuring out chemical processes, there's industrial engineering, which is figuring out the layouts of factories and how we organize kinds of labor. There's just so many different kinds. And I wanted to see every single kind's view into what engineering looked like to compare them all to software, which, when you think about it, when we say, like, oh, software isn't like building a bridge. Maybe it isn't. But is it like designing a circuit is like figuring out a chemical flow? Maybe those are much more closer to the kinds of engineering we do. I needed to know. I think in the end, I talked to about 15 or 20 people in total across about six or seven different fields.

Speaker C: And what were the similarities that you found that software engineering has with either specific types of engineering or across the board?

Speaker B: If I had to summarize what I found in general, I'd put it like this. Everybody hates waterfall.

Speaker C: No way.

Speaker B: Core tension of engineering is between how expensive it is to make a mistake and how quickly you can iterate. The faster you can iterate, the less planning you need to do before you iterate, and the more expensive it is, the more planning you need to do. That's why, for example, when you're building a building where you can't like, build it multiple times and see what happens, you have to do a lot of planning up front. But even then, you are looking for ways to iterate on the plan. You do things like build scale models, you use software to simulate the building you do, like CAD models, et cetera. And in other fields, like in, for example, electrical engineering, you have the ability to come up with a design, test it, and then throw it to the fab and get something back. So they will iterate a lot more than civil engineering does.

Speaker C: Ah, uh, Interesting enough, I, I heard the term smoke test originated from electrical engineering.

Speaker B: Actually I did not look into that, but I could believe it.

Speaker C: Yeah, fairly. It's when you have a test circuit and you just hook it up and if it does, if it smokes, it's already bad. That is very interesting. So even within engineering, when we say traditional engineering, there's just layers of engineering or differences. Right.

Speaker B: Layers of iteration, I'd say. One of the first people I talked to was actually a mining engineer. He designed mines deep underground to make sure that they were stable and didn't like leak task chemicals. And the first thing he pointed out to me was that they had their agile revolution in 1960. They called it, I believe, the Viennese tunneling method as a way of really quickly iterating through building a mine and tunneling through rock. Basically making the change as fast as they could, seeing how the rest of the system reacted to it, and then course correcting based on that.

Speaker C: Okay, so I guess we all hate waterfall. We all hate waterfall or the idea of waterfall.

Speaker B: Yeah.

Speaker C: What are some of the interesting differences that you came across? Either where engineering is ahead of us or traditional engineering has, you know, does have things on us which you were hoping to find, or places where actually software engineering is ahead.

Speaker B: In some ways there's both differences in how we practice it, but also differences in the shape of our material. Because every engineering concerns a different material, they have different constraints. While it's true that everybody tries to iterate as fast as they can, often turning to software to do that, software is the best at it. The best comparison is chemical engineering where I talk to people saying that they would set up their experiment, run it overnight and get the results the next day. And that was fast. With us, we can basically press F11 and get the result right. And that allows us to basically iterate much faster than uh, even those fields can. I think we all kind of know this. One thing that we might not realize as software engineers is that our work is a lot more consistent than other fields. The example I always do sometimes, because I've given a talk about this, is I would pull out like a CPU chip or like a stick of ram and I'd say like, hey, here's the spec sheet. And if you look at the spec sheet, it says this resistor has a resistance that is within 20% of a hundred ohms, as long as you keep it between 20 and 50 degrees centigrade. So they're basically saying that if they make a thousand of these, there's going to be a variance of 20% across all 1,000. And the only way to know is to test them. And then if you run it for too long or you heat it up too much, it's going to change. Again, with software, assuming no like CPU bugs or anything like that, the same program, if it runs on this computer, it'll run on your computer exact same. Store this list, the exact same if it's sorting algorithm.

Speaker C: Does this also mean that we might not account for, uh, variability as much as other engineering disciplines do?

Speaker B: I'd say so. The variation we have to deal with is kind of of our own making. Right. We are basically saying, okay, we've got all these different systems, all these different APIs versus other people was like we have all these different chipsets, We've got all these different like ports or sizes. But also if you happen to touch like an iron screw to a tungsten screw, they're going to cause corrosion between the two of them. And also some of your screws are a little bit too bigger than others and some are a little bit smaller than others, some are a bit longer, et cetera.

Speaker C: And how did you see the similarities or differences of software? Engineers, for example, often interact with customers with end users who use the software in other engineering fields. Is this also a thing where as an engineer you will talk or know your customer or just not knowing them at all?

Speaker B: I think it depends because different engineers I talked to had different experiences. Some said that they felt that with software they felt much closer to the customer. With other ones they said they felt much further. So I think it's hard to really tell there.

Speaker C: One thing I remember vividly is a difference that you pointed out, which was very different and almost makes software engineering a bit higher status or a better place. Is open source the concept of open source?

Speaker B: Yes. So that is one thing that seems very special about software versus any other field. Like, the reason I'm here in Hungary right now with you is because I'm going to be speaking at, um, craft conference. Right. Most other fields of engineering, or in fact any other field of like human labor, has two kinds of conferences, academic conferences where they talk about research and trade shows, where they try to sell, where vendors try to sell to like companies. Software is kind of unique in having the third kind of the practitioner conference, where we are just meeting to get better at what we do. We also are really the only kind to really focus heavily on like open source and making our knowledge freely available for any language. You can probably find out how to learn the language online Right. You don't have to buy a book, you don't have to like talk to the vendor to learn it. That's something really special about software.

Speaker C: I wonder why this might be both. The, the fact that we do share a lot of the information or the craft or how we build things. Even some of the largest companies, they I think are uh, like an Uber or Airbnb. These are a hundred billion dollar companies. They will not particularly hide how they built that piece of software. Uber publishes and does, talks about their app that is used by all these people, how exactly they built it, or approximately. I wonder why this became unique in software and in not the rest of engineering. What does the rest of engineering have to lose with it? Or uh, what did we do to get here?

Speaker B: I'm going to switch to speculation for a second. This isn't something that I could really speak on with full authority, but my guess is that part of it is cultural, but another part of it is that the material we work with is the same as our product. Right. We are using software to write software versus using tools and lathes to build things or using software to design circuits. And I personally think that that similarity basically that we are using the same materials on both ends is what makes it so much easier for us to talk about things like open source.

Speaker C: Interesting how I like this thinking of materials used in each engineering and how our material is software itself. Um, of course it's hardware engineering and we know that's a bit different of course, but already there's a divide between hardware engineering and software engineers on how they, how much they share, how much we know about them, M and so on.

Speaker B: I kind of wonder. I've got some friends who do like 3D printing and it seems like, and I haven't looked into this, but it seems like they also have like a very open space of like sharing things freely. And I wonder if that's the same because it is so easy to share and because like the unit of value is the schematic. There's if that kind of leads to the same thing.

Speaker C: I also wonder if hacker culture might play a thing in places where it's easy enough to afford to get started on a thing. For example ham radios, which is not engineering, but there's a thriving community where they share the setup, the uh, things they talk with each other. Small electronics might be and then, but ultimately software started in the 70s when it was affordable. Anyone could buy a computer, maybe the Internet. I'm also just speculating.

Speaker B: Yeah, definitely something worth doing a follow up Project on. Right.

Speaker C: Well you've already spent a bunch of time on it.

Speaker B: Don't give me so many rabbit holes. There's already too many rabbit holes in my life.

Speaker C: One more thing that you brought up is version control and the, and the, the, the fact that in software we just take it for granted we have version control everywhere. And you said that this is super unique across most of engineering.

Speaker B: Yeah, I interviewed like 20 people on this. I think all 20 mentioned version control as the thing they wish they had in their old field. Wow. Yeah. Now to be clear, they do have things like change management in like other fields, but I think version control as we have it is so much more sophisticated than anything they have. It's like comparing like a modern car to a model T. What do you think?

Speaker C: There are things that. Now having talked with so many people and learned about the different engineering cultures, like active traditional engineering cultures, what could we learn from them? Um, what are some kind of inspiration that might be useful here or there?

Speaker B: Yeah, this is a harder question because while everybody I talked to mentioned those two things of openness and version control, I got a much more scattering set of answers when talking to people about what we could learn from their old fields. The two things I kind of gleaned out is that one, while we are a lot better at iterating than other fields, we're worse at the planning part. Like we still need to do some kind of planning before we iterate and we just aren't as good as those other fields in part because we can get away with not doing it as much. But we could get some sort of fusion of the two and get even better than we currently are, which hey, plug for what I do. The other thing that I think is more interesting in terms of being a bit more shocking to me is that while we're better at being open about all of our materials, we seem to be worse at compiling information about the specifics of our job. And that's a bit loosey goosey. But the example I keep coming back to is that one of the engineers that I talked about two favorite books, the Design of Everyday Things, which he recommends every engineer read, and the Snap Fit Handbook. Are you familiar with Snapfits? No. Looking around here to see if there's like one, if I could just show it but like you know, like how remotes, they have that little clicky thing in the back that you use that hold the battery in. Yep, that's a Snap fit. Mhm. It is a physical device that basically clicks into another device to Keep them used. And this was a 500 page book all about snap bits, their engineering, appropriate shapes, materials, et cetera. And that kind of compiling of information about the materials is something other fields do that we don't do. An analogy that I would think of in software would be something like a 500 page book on how to version an API.

Speaker C: We could all use that.

Speaker B: Yes, we could.

Speaker C: And we don't have it.

Speaker B: We could learn it from engineering. We should have that.

Speaker C: You started this project asking, are we really engineers? And um, your personal inclination, which you didn't say at the time, was uh, that we're probably not. In the closing of this series, you said you're still a bit unsure of how to answer it. This was five years ago. This many years later, what is your inclination? Are we actually engineers?

Speaker B: I think so. I think this project and writing about and thinking about it has firmly moved me from the camp of we are definitely not to we probably are. I do want to caveat that I wrote this before LLMs were a thing. And this has probably changed our field as we know it. And it's probably also changed those other branches and I don't know how. So that could have changed the calculus between two spaces. But as of now, I think excluding LLMs and how they're changing things, what we do now is very similar to what those people in those other fields did. According to my interviews, it's, it's such

Speaker C: a cool project and it's still a very good read. Uh, I'll also link it in the show notes below. I do recommend going into it. So let's talk about formal methods. How did you get exposed to them? And for those of us who are not deep into it, what are they?

Speaker B: I'm going to give you a function, max, right. Which should, given a list, return the largest number. What would be a test you'd write for that?

Speaker C: I'd write a test that I do a list of like two items. It returns the largest one that I know. I give a very long list. I try to stress test it. I give a list where I give like similar numbers. I try to come up with some edge cases. I'll probably write like five tests. Try to think about integer overflows potentially try some tricky. Maybe I'll take it to maybe eight if I'm feeling super ambitious and then I'm done.

Speaker B: Okay, so when we take one of those tests, how do you know what the right answer is supposed to be?

Speaker C: I just know because I have a. I learned math. So, uh, in school I Know which number is bigger. Honestly, I look at it, I have this, I guess ingrained knowledge. It feels very basic knowledge that I don't even have to explain.

Speaker B: Right, you have some ingrained knowledge that you don't have to explain such that you can look at say the max of two and three and know it's three. Right. That's interesting. There's some sort of implicit mechanism in your brain that can see that and know what the function is supposed to do. Step one of what I do with formats is asking can we take that implicit knowledge and make it explicit? Can we figure out what a function is supposed to actually be doing and write that down in a way that can be shown to anybody. So I would basically in this process say like the max of a list is an element that is in the list such that every other element is smaller than that element. That is a way that we can formally say what the maximum of a list is. So that's part one. Just learning how to look at functions and say like, okay, I know what this is doing. How would I explain what this is doing in a way that is clear and unambiguous? Then step two is asking every single test you've written is basically some facet of it is an element of the list and it is the number in that list such that every other number in the list is smaller than it. Now that we have that, what's the best way to show that our function actually satisfies that? Specification tests are one way. Those are basically taking individual values and showing how those comport the specification types are another way. We could basically say like, okay, in every single case we are putting in a list of elements and we're getting out a single element. So we have to make sure that every time we call it, that's what's true. So basically the coming up with the properties of the thing, like what it actually is is the specification of it, and then showing the function matches that specification is the verification. And what foemath is asks is, can we use mathematics to show that it works not just for the cases that you asked for, but every single possible list you pass in. And that is done through proof. Coming up with some sort of mathematical argument that this code matches this spec.

Speaker C: And then in proof again from university, I still remember the maths proofs where we would proof, uh, an equation. You do rigid transformations, you know what you're allowed to do. Sometimes you can bring in tricks, but those tricks are also inside of your rigid list. And every time, you know, you typically Start from a complicated equation and you keep changing it and in the end you, you shape it in a way that it's now trivial or you transform. Those are one of the proofs we do. Is this what formal methods also does? To some extent, yes.

Speaker B: But you know how to basically add two tangent numbers by hand, right? Do you do that by hand or do you just use a calculator?

Speaker C: I now use a calculator. If it's easy enough, I use my brain as a calculator, otherwise I just punch it into the calculator.

Speaker B: Yeah. So similarly, a lot of formal methods that math and transformation, while you can do it by hand with like what's called a theorem prover, often in industry that is being done for the most part with tools that basically automate huge parts of this process. So you don't have to do every single transformation yourself. You can, for example, say, okay, we have, these things are true at the beginning. I want this to be true at the end. And can you figure this out? And it'll be like either yes, I can prove these things match, or no, I need a little bit more help. And then you say like, okay, at this point I'm going to also let you know that this is true. And like, okay, I can verify that's true and it helps me get to the end. And you just keep doing that until you actually have enough that the computer can do the proof for you. Yeah.

Speaker C: So with formal methods, this, I mean, this sounds all logical. I think it's easy, easy to follow in practice. What techniques, technologies, tools does the industry use, the tech industry use to actually prove that, you know, some stuff works.

Speaker B: To get to that, we need to ask another question. Why isn't this being done for everything?

Speaker C: Okay, let me ask that question. That's a good question. Yeah, this all sounds sound sensible. It will be nice to not have to write out those five or eight tests. And I know that those tests might not cover all edge cases. Been there, done that, where you miss. And I, I only I, I didn't think that. I didn't do a formal proof. I thought like, well, I missed a test case. That's on me. Sorry. Let me put in that, that test case. I now have nine tests. And now I go and think I did a great job. Why are we not doing formal testing for everything?

Speaker B: Instead of finding the largest number in a list, why don't we try to find the file in a directory that has the most lines in it?

Speaker C: Well, now I'm thinking of writing a program that in kind of an imperative style. It goes through a four list each. Each file I list how long the lines are. I, uh, count the lines. I cannot tell it easily.

Speaker B: Okay, are we talking about ASCII lines or UTF at newlines? What happens if one of the files, you don't have the file permissions to read it? Should you basically ignore it, or should you say, hey, my proof. My, My, um, function might be wrong?

Speaker C: You're now kind of trying to.

Speaker B: What if one of the, what if one of the files is a shortcut to another file? What if it's actually directory you're now simulating? What if it's a binary?

Speaker C: You're now simulating real world?

Speaker B: Yes, and that's the problem we have, is that when you start talking about, like, most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get correct 99% of the time is probably good enough to use in almost all cases. And if you want something that works in 100% of the cases, you've got to figure out, okay, which file system are we using? You have to figure out everything.

Speaker C: Yeah.

Speaker B: And that's why it's not done.

Speaker C: And, um, basically it would just not be practical. It will be for the, for 99% of the people. Why are you wasting your. It's like premature optimization, Right?

Speaker B: Yeah. Especially when, as you say, writing 10 tests might get you most of what you need.

Speaker C: What are practical technologies that you have seen use in some part of the industry that even though they will, I'm assuming, will be somewhat heavyweight? Because it sounds like pretty heavyweight. It might be the return, the return on investment of using this, uh, heavyweight stuff is worth it that teams in industry are using it today. Right.

Speaker B: And here we can basically start to break this down to different parts of the landscape. So one part is to look at the stuff that actually does need to be verified to that degree. And the usual term here is nukes and NASA, like nuclear power plants and like, um, NASA. But I can tell you with firsthand experience, nuclear power plants do not care about this stuff. They're actually just fine with thorough testing. Okay. Okay, so then category two is like really focused cores of programs where they need like one specific part of the program to be like, really verified. And the rest of it they can use informal methods. And this is usually things that are like, um, small parts of databases or like cryptographic primitives. I believe that the HTTPs stack in Firefox is verified as part of something called Project Everest. But I might be getting some details of those wrong.

Speaker C: Would an operating system kernel fall into this? Or maybe just a very key specific part of a kernel like memory allocation or something like that?

Speaker B: Yeah, parts of operating system kernel are good uses for this. Um, a couple examples I can think of is I believe Microsoft used some formal verification on parts of their Vista kernel for the driver loading. Famously, there is an operating system called SCL4 that has been end to end verified in a language called Isabel. It's a microkernel, it's very small, it's mostly used for, um, automotive and military applications. But it is a fully verified operating system with a caveat, meaning that it's matching the specification. So it might do the wrong thing. But of the things that you specify that it has to do right, it will do those specific things right in the right circumstances. The last category is the kind I work in, which is asking, okay, what if instead of verifying the entire real world system, which is a nightmare, as we just discussed, we create a simplified version of the system and verify that then the actual system might still have bugs, but we can iron out the issues, the abstraction such that we don't actually build them in the real system.

Speaker C: And so that's a topic where you are planning a system and you want to stress test it to iron out.

Speaker B: Yeah, stress test the plan.

Speaker C: What kinds of plans would these be? Roughly? Is it planning like again a database or some sort of distributed system?

Speaker B: In my work it's mostly been, um, databases and distributed systems for technology companies. But I've had some other like, interesting gigs. Like I've had one gig that was involving formally verifying um, firmware of a device kernel. And one, honestly, one of the coolest products I ever worked on was on, um, verifying the transponders of a train system to make sure that they wouldn't cause problems to trains going over those transponders. That was a lot of fun. We found a really old bug in that one too that was kind of exciting.

Speaker A: This whole episode is about a question that only gets more important as AI writes more of your code. How do you know if it's correct? And for some parts of a code base, you really don't want an AI model to be taking guesses at. AUTH is on top of that list. And this is where I need to mention our seasoned sponsor workos. If you're building any SaaS, especially an AI, uh, product, you'll need AUTH for apps and agents. This is the layer where close Enough is just not good enough, so don't let this layer get improvised by AI Workos Gives you the proven implementation sso, scim, and fine grid authorization built for how agents operate and in a way that's easy for them to integrate with an implementation that you can trust. Check it out@WorkerWise.com I also want to talk about our season sponsor TurboPuffer, but this time I don't want to talk about how they are a fast, cheap and extremely scalable search engine built on object storage. Instead, I'd like to talk about their team. I interviewed Simon, the co founder and CEO, on stage at AI NGOs World Fair and also hung out with their team for a few days in person. Here's a few interesting things I learned about them. The company is full remote, yet feels pretty connected. They have a Slack first culture, for example, all of their customers have a dedicated Slack channel, and engineers are in these channels, seeing feedback from these customers, often fixing their bugs. The team gets together for annual summits at least twice a year, and campfires form several times a month anytime several remote employees gather in the same city. Simon describes their engineering culture as hardcore and whimsical. They focus on solving difficult problems but but also try to have fun. A good example is the Pragmatic Engineer landing page that they built. We agreed to have a custom landing page and then their team decided to build a cool logo that animates on mouse movement. Another interesting thing is their team composition. Pretty much everyone currently working at the company has 1015 years of experience for a startup. They are an unusually seasoned team. Finally, I really appreciate how pragmatic their engineering philosophy is. Simon and the team strongly believe in how simplicity scales, and this is the reason that Object storage is TurboPuffer's only dependency. The team do seemingly silly things like build their job queue in a single file on object storage because they understand the core primitives and they know how they scale. To check out the whimsical animation or if you're building AI products, head to turbopuffer.com pragmatic and with this, let's get back to how TLA works with a demo from Hillel.

Speaker C: Can we see a demo?

Speaker B: Okay, sure. So I've got a couple languages with me, um, the kinds that I've worked in. So the most popular technology right now for that kind of planning is this language called tla. It was invented by Leslie Lamport, the same guy who made Latex, the, um, typesetting language, actually. Oh yeah.

Speaker C: All the PDFs behind the scenes are latex.

Speaker B: Yeah, PDF span of the scenes of latex. And he wanted a language that could be used to model distributed systems. So he basically created this thing called tla. Temporal Logic of Actions. Plus, everybody always asks about the name. You don't need to know the name, just know it's tla. And what it does is it basically represents the state machine of a system. Every possible state it can be in and every possible state it can transition to. Then we can use a brute force model, checking where we basically find every initial state and every state that can evolve from those and check if they have properties. TLA plus is unique in some ways because it has certain properties like checking liveness and refinement that we won't get into. But let's actually see a demo right now. So this is one of the demos I like to use to showcase this. And we, in this demo we have a simple model of a trading platform. Each person on the platform has a set of items and they want to trade these to other people. The way that we're going to show the simplified system is that each item is assigned to a person. There's also a set of outstanding offers. We're only going to model sending items to people, not swapping items. If you propose an item, you have to own that item and it's basically added to the set of offers. And then you can accept an offer. If that offer is available, you remove it from the set of offers and the owner transfers. If you reject the offer, it's just removed from the set. Then we define what can happen next. A next state. As in. One of the ways the system can evolve is we pick some two people that are different. That's what this from dash equals two means and some random item. And either you propose that item accept a proposal for that item, which must already exist, or reject an existing proposal. Below we have a property that a valid change is one where if the owner changes, it is because the new person accepted an offer from the old person. So if the item goes from you to me, it's because you offered it to me and I accepted that offer. And finally, we have a change invariant, some property of the system saying every change is a valid change. Now what's the bug in this?

Speaker C: Well, uh, first of all, this has a learning curve.

Speaker B: Yes, it has a learning curve. And that's why this is fairly niche. And I should probably point out right now that when Leslie Thumper made this in 1990, like 4, he was thinking of it mostly he was a mathematician, right? So he was Using his mathematical like background and like learning how a mathematician would write some symbols. In the 30 years since that point crisis, been 30 years since 1994 already a lot of languages have been developed in part from the lessons I've learned of TLA that uh, made things a little bit more appealing to programmers. So you have things like Quint and P, which are uh, languages that look more like programming languages and are easier for people to grok. The reason a lot of us use TLA was because like the first really high profile demonstration of this kind of work in practice was an Amazon paper, the use of formal methods in Amazon web services in 2014. And they used TLA for this. So that's what a lot of us just have originally started on.

Speaker C: So going back to this, there is a bug in this one with all the associations and how can we, how can we figure out what the bug is? Will, will the system help tell us or we now need to think through of what case we missed?

Speaker B: Well, if we had to think through it ourselves, we wouldn't be using snazzy syntax, would we?

Speaker C: Nope.

Speaker B: So what I've done is I've also written a quick um, configuration file saying take a specification, take these three people, Alice, Bob, Carl, and have them trade around a stick. And then I tell it, make sure this property that the change invariant always holds.

Speaker C: Always holds. Yep.

Speaker B: Now I just have to run this. I'm also having it output the state space for you so you can see what that looks like. And it just puts out the error for us. It says the property's been violated. It took 53 states to find it. And the way it works is it's on a small screen so it's being word wrapped. But if I see it kind of looks like this. Essentially the error is as follows. And let's actually see if the error. I can show it to you with the um, dot file. Um, graph is not vis. What am I saying? So this is just um, a preview of the state space it's generating. So you can see it's basically generating every possible state it can find. This isn't the whole state space usually because the state spaces end up being like um, 100 million states like in the state space. Usually these aren't that useful. It's mostly a thing that we have for, that we sometimes use for demos. So the error is as follows. Alice, Bob and Carol are on the system and Alice owns the stick.

Speaker C: Yep.

Speaker B: Alice makes an offer to Bob, Bob is away. Alice gets tired of waiting for Bob to come back to make the offer because she wants to get rid of her stick. She makes the offer to Carol. Carol immediately accepts. So the stick transfers from Alice to Carol. Now Bob comes back, sees the offer from Alice to Bob and goes, oh yeah, I want that stick. Clicks the button and now the stick becomes Bob's. But it did not transfer from Alice to Bob, it transferred from Carol to Bob. So the change invariant that if the stick went from Carol to Bob, it must be because Carol made an offer that Bob accepted was violated. And therefore the system raises an error.

Speaker C: And m Then how did the system simulate this? It had to simulate a state where Bob was uh, waiting or, or didn't respond for a while and responded later.

Speaker B: We basically, assuming we start in the state of basically Alice owns the stick. There's two possible things that can happen here, right. We have offer Bob.

Speaker C: Yep.

Speaker B: And we have offer Carol. Right. So those both happen and those are both distinct states. So the model checker says, okay, I'm going to create two new states. Then from this top one of Offer Bob, there's three things that can happen. We can have Bob accept. Mhm. Bob reject. Or and this is where the concurrency comes in, we can do offer Carol. Right, Yep,

Speaker C: I see, yeah, Mhm. I see where this is coming. And then when you continue, we will hit the bug.

Speaker B: Yeah.

Speaker C: The change invariant will be invalid at whatever step that is wrong at.

Speaker B: Right. And that's actually where a lot of this like, becomes useful for distributed systems. Because often it'll be like, okay, process one can do one of six things. Process two can do one of six things. Process three can do one of six things. And when you do this brute force, you get states like process 1 takes step 1, then process 1 takes step 2, then process 2 takes step 1, then process 1 Takes step 3, then process 3 takes step 1 and 2, then process 2 takes step 2 and 3, et cetera. And being able to sort of see every possible duration of that is very hard for human beings to do. But a computer with enough CPU can just crunch through it in a night or two.

Speaker C: Yeah. So this is what TLA is then.

Speaker B: Yeah, basically.

Speaker C: And one story I've heard, and I think you might have been involved is aws, uh, using tla. Can you talk about how they onboard it, how they're using it, what they're using it for, as far as you're aware?

Speaker B: Yeah. So the seminal paper on this was in 2014, the use of parallel methods at Amazon Web Services. And they talked about how a couple of people in the company were Interested and learned TLA plus in another language called PlusCal, which is something that compiles TLA and applied it to aspects of the DynamoDB and S3 storage systems. In doing so they were able to find fairly complicated bugs that could potentially lose data. And I think it was in the replication system.

Speaker C: In the paper it said that the shortest error trace exhibiting the bug contained 35 high level steps, which if I understand that correctly, it was at a depth that it would have been very hard for a human to persevere or you would have needs to be really determined.

Speaker B: Mhm.

Speaker C: And precise.

Speaker B: I did not work on that project, of course I don't know what the details are. I can speculate that the reason it found a 35 step bug was because the state space was probably a hundred million states wide. So there were like plenty of say like 70 or 80 step chains that were totally safe and just having this one 35 step chain was invalid.

Speaker C: Through working with a lot of customers and teams that have used formal verifications with distributed systems. What are some problems you've come across with distributed systems that might be a bit of a repeat pattern of how they break down or why they break down?

Speaker B: If I can think of one thing that besides just general race conditions and locks, this is the one that is always going to be pulling hardware. Yes. It's another time to allow time to check. The time to use bugs and time to check, time to abuse is a situation where you are checking to see if something is like valid, can be done validly and then you see that it's correct and then a little bit later you do it. Sometimes that little bit later is like a day later, sometimes it's a microsecond later. But is any case where it is possible for something to go from being valid to being invalid in between the time you check and the time you use it? A good, uh, example here is imagine you're withdrawing like money from uh, a bank account and putting to another bank account. And this is not how banks work. I know they use a different kind of ledger. But just as a demonstrative example, you check, oh, do they have $10 in their account? Yes, we deduct $10, we put $10 in this account. But what can actually happen is you check, do you have $10 in this account? Yes. And then while you're still getting ready to withdraw, somebody else quickly runs in and grabs those $10 away and now they're $0. Now you deduct those $10, you have negative $10. That's the time to check, the time to use kind of bug. They happen everywhere.

Speaker C: Yeah. And it's very interesting because I, when we were building Uber's payment system, I realized, or I learned, that the problem of having a message delivered in a distributed system exactly once is a very difficult one because typically that's what you need when you want to do one, one charge. You want to charge a customer's card exactly once, because if you send multiple messages just in case one of them gets lost, you now have double charges. And, and turns out it's a complicated, uh, problem. It's a lot easier to do at least once delivery than exactly one's delivery. But of course, you need exactly at least once delivery to build on, to create exactly once delivery.

Speaker B: Yeah. I wonder if this is why a lot of, um, businesses, they just charge you extra and then refund you some amount. That seems easier to do from an engineering perspective as well.

Speaker C: It's also from a risk perspective. You eliminate a lot of edge, uh, cases by authorizing upfront on the credit card. You have a credit limit, and if you would authorize exactly how much you think you need right now, but you need a bit more, you might get into that edge case where later you have trouble authorizing it. This is why often hotels don't want to deal with this. So they just authorize a larger chunk. And they know because it's a larger amount for hotels, otherwise they might have run into the thing where you run out of your credit and now they have to do a separate flow. But you're right. So some business, some engineering decisions might happen because it's easier to do some, some stuff.

Speaker B: Yeah, it makes sense. I honestly thought hotels did that because they were trying to convince you not to, like, break stuff because, like, hey, if you know that you're definitely gonna lose $800 if you break something, like, you're not gonna break stuff through.

Speaker C: Working with engineering teams who are building distributed systems, and you're coming in and helping them learn TLA plus, uh, learn how to revive things. What have you learned about how they usually think of verifying distributed systems before they learn about formal methods and what changes after.

Speaker B: So I think the most interesting thing about formal methods and how it affects how you build systems isn't the theory of the method or how it makes you think about systems. It's the practice. Why is concurrency hard? Why is it hard for us to reason about concurrent systems? Why do you think it's hard?

Speaker C: I think it's hard to keep several things in your mind of, like, where they could be. That's one. Or maybe we just don't really have a mental model of how to draw them out. Uh, I guess whiteboarding would be a way to do it. But I don't remember whiteboarding on concurrent system. I remember whiteboarding just boxes and imperative. This flowcharts are good for whiteboarding.

Speaker B: So this is something that I've wondered a lot, right? Like why it's hard for us to deal with these systems. And I'm not sure it's because it's hard for us to think about them. I mean, like, when you cross the street, aren't you working with concurrent system? You're just, there's cars everywhere, they're going to hit you, you're going to die if you don't model the concurrent system in your head. And there's actually this really cool paper I found called Common Sense Computing where some people were trying to figure out like, how people thought about concurrent systems. When talking with sort of like high school and college students, they changed the concurrency problem from like, hey, we've got these threads doing some operation to like, hey, we've got these clerks at a ticket office assigning seats at a concert. People saw the bug much faster. Uh, so I do think we can actually get quite good at seeing concurrency issues. I think a large part of the problem of why it's hard for us is because we don't get a lot of practice. Usually when you have a race condition in a system, you find out months later and then you try a fix and you find out weeks later after that if the fix actually worked. Whereas with the tla, I write my model of the system and then I click a button and immediately tells me, hey, race condition. And then you fix it and it says like, hey, timeout bug. And then you fix it again and says hey, T o C T O U bug. And that feedback loop ends up being so much faster than you get in practice. And I think that more than anything else, helps people find race conditions more easily and think about problems in super systems more easily. I've found personally that when I work with new clients and we're modeling their system, I usually have no idea how their system works, right? Because they're the domain experts. I just have notes of really weird funky language made 30 years ago. But once we actually have the model, I can see the bug in the model much faster than they can, even if it's their system, simply because through this work I've had so much more practice with it. And I think that's the Main change in how it affects people's ways of thinking about distributed systems. It gives them actual practice in seeing how those systems can go wrong so much faster.

Speaker C: I wonder if it's a little bit like refactoring and also migration. So refactoring a code base, when you are starting out as a developer and you need to do a refactoring by hand, you know, let's say just changing a function and then you need to go and change all the references that function and the first time you do that, you change it at a few places and then you forget about the rest and either it's a compilation issue or if it's a dynamic language, it's another problem. But then you get good at it once you practice with migrations. Most engineers that I've seen are terrible at migrations because you need to make a plan, you need to do check, you can shadowing, reverse shadowing, uh, ah, all that funk. And then there are a few engineers who have done three or four or five and then they close their eyes and they can just do it. I'm just thinking that when it comes to race conditions, most of us, I was exposed to race conditions by, oh, we did a double charge that one and then we found the race condition. But I never did a second one. So I will not be good at finding race conditions. I am not even good at thinking about them.

Speaker B: I think that's right on the money.

Speaker C: It sounds like you coming into teams or to these clients, you at least give them some practice, the very least of how to think about this category of errors, even assuming that the uh, to taking out even the tooling itself.

Speaker B: I think there's also like more subtle things that you start to pick up from these tools. But I think that's like the most visceral one, the visceral like hatred of a race condition that gets a like physical presence in the algorithm.

Speaker C: Um, you've been doing this for very long. For you writing TLA is like for most of us writing TypeScript or the language that we're familiar with. How has your thinking changed? And um, is there any similarities between when you program an imperative language and then you learn a different one, like a declarative language which requires a very different thinking.

Speaker B: And that also depends on declarative language. Like I've, I've, I've done a lot of stuff in like logic programming languages and like I've done some stuff in like array languages. But like you show me css, I'm just like, what is this dark Magic Declarative. What are you talking about? I think so. Um, it's gonna be hard to sort of pin down exactly what though. Like my usual hacking language is Python these days, just because that's like one of the first things I use and I just know very well and I think like, at the very least, like, the formal methods makes me much more willing to reach for mathematical solutions or like math heavy solutions than like simple, reliable solutions.

Speaker C: Math is also an interesting topic. Uh, you've recently had a bit of back and forth on whether developers, programmers, software engineers should learn math. There was a bit of a discussion back and forth. Could we talk about the core of the argument?

Speaker B: How math is useful in programming is a very interesting question. Right. So first of all, there's math that we all find so useful we forget that it's actually math. Like counting, counting is math. Knowing whether one thing is bigger than another number is math. Right. It's just math that we have been taught from a very young age because it is so important that no matter what you're doing in life, you need that math. Then there's a lot of math that is useful for very specific specialist jobs. Like, I've Talked to some SREs who need calculus, but I think most programmers do not need calculus. There are some branches of math that are useful in a wide range of programming. I think things like understanding graphs and directed graphs, knowing matrices, knowing formal logic can be very useful for a lot of different people. But I think it is more useful for most developers to have an exposure to like what math has in the various fields versus just going all on every single field when they see them. Right. You've got to know what's available to know what's most useful for you. And most math will not be useful for you.

Speaker C: It's also very interesting because for a long time I thought at university we had pretty heavy math education for computer science, from uh, algebra to computational theories, even formal methods. At university I learned a bunch of advanced math and at first when I came into the industry, it wasn't particularly useful or I didn't use it day to day. But then there are some times where it's kind of useful. For example, M matrix transformation, I learned 3D graphics and I how you compute all the points based on 3D, um, matrix transformations. And then it helped me understand when GPUs were becoming so popular with AI. Why this is because they're also very good at matrix transformations, which happens to be pretty similar. So every now and then I feel it, it helps with Your general understanding and it helps you be unafraid to go into deep. So if I see a paper with formal proof, I'm m not going to shy away from it. I can start reading it and I will know my, my limits. But I have that understanding. And I think going back to our discussion with the crossover project, I wonder if it helps you connect closer with other other engineering disciplines in terms of you can understand more things there. For example, for electrical engineering, you do have math involved that is there to describe and if you will want to have the vocabulary to understand that part.

Speaker B: One of the interesting things, at least about the mathematical differences is that in almost every traditional engineering field, the math they need is continuous math analysis, things like differential equations and calculus. And that in the United States is what's taught like at an advanced level in high school, if you get that far, is this kind of continuous math. In software engineering and computer science, the math that we most often use is discrete math. Things like combinatorics basically, which is the math of counting things, graph theory, formal logic, set theory, things that work with discrete entities, which isn't usually taught at least in the American high school very much or even early in university mathematics classes. And I wonder sometimes if that is the reason people don't recognize the use of math and software engineering is because the math they do need is not the math they've been exposed to.

Speaker C: Interesting. Yeah, because uh, the math that I did use more was common networks. Uh, and of course like maybe these days those interviews are going out of style, but there's the um, here's a problem. Build an algorithm that solves it and then you ask like okay, how efficient is this algorithm? And then there's the big old notation. We have the language to describe how efficient in space and time is. And you can do trade offs and you can. And once two people know the same thing, you can have discussions about these things. And on one end it's very abstract, but on the other end, if you're close to the machine, it can be very useful.

Speaker B: I've also found that my understanding of big O notation got a lot better once I understood the mathematics behind it because I think it's usually explained in terms of oh, this function scales at this certain rate, but it is more formally a way of describing a set of functions. And then there's the math of like how we do asymptotics and stuff, but like et cetera. I think even like the technical aspects, the math does help a lot in understanding those.

Speaker C: Yeah. And with the uh, tla specifically, what cases have you seen in the industry? TLA being a good fit for certain problems and in what cases would you never consider it?

Speaker B: I think the case is TLA plus and most, not all, but most role methods. They shine the most in highly computational domains where most of the problems are highly technical and not like business embedded. And what I mean by that is that like, how do you replicate nodes between these two data sets is like very technical, right? Something like I'm trying to think about like um, a good example here, like how do we make sure our sprints don't go over time is very business, right? It deals with like very human behaviors and I've had to help model client model that and we got some use out of it, but it was very hard. So that's why a lot of my clients end up being things like database vendors or like cloud computing, people who are, or like hardware people who are working in a space that's like very important for business, but several steps removed from like the front lines of that business. The other thing I would say is that different, uh, tools are good at different things. TLA in particular tends to be good at discrete distributed systems where the main challenges are messing with concurrency and possibilities of intellect being like behaviors. It doesn't do floating point, it doesn't do decimals, it doesn't do as well with when you're trying to figure out probabilistic things. Oh, that's another thing I guess I should be saying is that like where the kinds of errors you care about are, uh, ones where like, if it is possible this error to happen, that is a big deal. It's not good if like you're like, okay, this error is bad, but as long as it happens less than one out of a hundred times, it's okay. It can't do that kind of probabilistic reasoning for you. There are tools that can, but they lack things like functions or arrays or numbers. Also depends on how much time you need to spend planning. Like, if you don't need to spend that much time planning, this is going to waste your time. I do want to add that, that this, like, if you can iterate your way through a solution and the bugs aren't going to be that costly, then you might not need this tool. I think it's really important as like a person who talks about a really exotic tool to like constantly emphasize and like, no, I'm not trying to convince you to like use something that's not a good choice for you. I think a lot of the reason people are skeptical of these is because they've been burned by things like CASE and UML and all these other miracle solutions that were forced on them by people who wanted them to use it no matter what. And I think it's really important to always say like if this isn't the right tool for you, I am not going to recommend it.

Speaker C: And then m Can we talk about other tools or can you show us a few other ones?

Speaker B: Yeah. So the other tool I have installed on this computer is called Alloy and it was made by an MIT professor. Different from what is lineage? Just like there's m many different kinds of programming languages, there's many lineages of formal specification verification tools. So this example is a simple access control system. So we have a set of resources and users who can read those resources. So each resource has some people who it's reasonable by. And resources may or may not have a parent resource. L uh one mean L one meaning less than equal to one resource. There are no cycles. So no resource can have itself as a parent or its parent's parent. As a parent.

Speaker C: Yep.

Speaker B: You can read access a resource if the resource indicates you can read that resource or if its parent indicates you can read that resource. And we have a property that if you can read a resource you can read its children.

Speaker C: Yep.

Speaker B: This is, has a bug. What is it?

Speaker C: I mean I, I'm, I'm glancing at this and um, this all made sense to me. I thought this is it because we're saying all of the parents can access it. I'm assuming the bug, if, if there is one is it will. It might have to do with something that we talked earlier of like accessing in certain areas. No idea. Can we run it?

Speaker B: Yes we can. So this was actually made in an earlier version of Alloy just for the, just for context. Alloy did not have any sort of temporal reasoning over state up until about four years ago. So this is one of the examples I used from before then, uh, of basically how you can analyze and find bugs in static configurations. An alloy that often means finding bugs in data structures or in data models and domain models actually. So there's actually some interesting, there's some interest in this in the domain driven design community. I found I'm going to copy this over to Alloy their ide, which is a bit more rudimentary and that's why everybody uses the VS code. Now if I execute this, Here's the counter example and this is one of the things about Ally specifically is that it can generate like um, visualizations so basically, here's the problem. We have a user who can read a parent resource. The parent has a child because of how we defined, um, can access, we can read as parents. So we can read the child.

Speaker C: Yes.

Speaker B: The child has a grandchild, we cannot read the grandchild. So because we are not in, we are not assigned to the readableby for the child, only the parent. In other words, readableby is not transitive. So we can read the child, but not the child's children. And that is the bug.

Speaker C: Mhm. And to visualize this for us.

Speaker B: Yes. Which is quite nice and one of the reasons why people really like Alloy.

Speaker C: Nice.

Speaker B: It's a bit worse for modeling like distributed systems though, which is why most of my work is in tla.

Speaker C: And then, um, to do the fix, what would it involve? We would need to give access to the children's children.

Speaker B: Yeah, there's a few different ways that we could fix it. And often like PRO methods, they don't really tell you. Here's how you fix it. It lets you choose how you want to fix it. Like one thing I could do is I could say, okay, I'm going to say that this is a transitive lookup too, that we transitively close over all parents and if I execute that, no more counterexample. That said, that might not be something physically implementable. I might try to tell like hey people like hey, in our SQL database you have to have a transitive query. And our database administrators like no, that's going to crash the database. You can't do that. Then we have to find a different fix.

Speaker C: So this is the beauty of formal methods. Yes. It gives gives you opportunities of how you will implement fixes, changes and then you can rerun it again and see what difference it made.

Speaker B: Exactly. Now one quick fun fact I love just fun facts about stuff. You see how this says solver sat 4j? So have you heard of SAT SAT problems?

Speaker C: No.

Speaker B: Okay. Is there some variable that makes the statement P true? If I can make P true or false, is there a way I can make that true? Let's say P is a boolean and I have a statement P. Can you assign some value of true or false to P to make that true?

Speaker C: Typically you can assign true and it will correct, well, true. Yeah.

Speaker B: So that statement is satisfiable by setting P to true. What about P and not Q?

Speaker C: Also satisfiable by giving, giving true to P and false to Q.

Speaker B: Right. Now what about P and Q and not psy?

Speaker C: That's unsuccessful because no Matter what Boolean you do, uh, true and false will always, will never be true.

Speaker B: Lovely. What you've just done is a Boolean satisfiability problem. Taken some sort of statement of a ton of Boolean variables, in this case two and found some, either found some assignment that makes it true or said that it cannot be made true. Now Boolean satisfiability is what we call NP complete. And what that means in theory is that there's no such thing as a perfectly efficient algorithm, uh, that solves all problems. In ah, practice that means that we can solve them really fast. So often what makes Allo interesting is that unlike tla which must be brute forced alloy can be converted into a satisfiability problem. I'll open this up and it is able to turn that model into a Boolean probability saying not x 21 and x 96 and x 15 or not x 72 etc. And because of that most alloy models can be checked in like a few milliseconds or a second at most, whereas often for like a large TLA model you have to basically churn it overnight to go through all hundred million states.

Speaker C: Can we talk about some other tools uh, on the like as a table of someone looking into formal verification?

Speaker B: Happily. So I don't have any more demos on my PC right now, but I can talk about a few of them. So a couple of the ones that have been successful. TLA plus is um, the P language, um, which was invented by I think a person at Microsoft Research who was then poached by Amazon as a way of making a language that was more accessible than tla, among other things. So it basically looks like a set of um, state machines, interacting state machines that send messages to each other. Almost like the actor model in like Erlang or something like that.

Speaker C: Yep.

Speaker B: So there's that. There's also another one in the same space as Quint, which was basically people who were making a different kind of model check for TLA and then realized they can make an entire language that was easier for people to pick up. They've gotten a lot of interest in the banking and um, I believe cryptocurrency space smart contracts. So another one that I've used which is a, which is a lot more niche but quite interesting is called prism. And PRISM is a probabilistic model tracker. So like TLA can tell you like this bug will never happen or it could happen. PRISM can tell you this bug can happen 10% of the time or it has a 25% chance of happening if you shut down, it's really cool. But it's also much more academic in that there's a lot more work required to actually translate languages into Prism if you're interested in it. I've basically been doing this like, um. Have you heard of the Jewish game Dreidel?

Speaker C: No.

Speaker B: Okay. It's a game that you play on Kronika where you spin a little top and you get money. And I do not like the game. And I have written a two part series using PRISM to show how this game is not fun by analyzing as a mathematical thing. Love it. Those are, I think some of the ones that are like really popular. But there's also um, I mean I could just keep listening. There's like, there's like event B which has like been used, I believe famously in part of the Paris Metro system. Um, there's like MCRL 2, which I think comes from a Dutch university, Humira X, which is mostly used for like um, robotic control systems. But I think that's mostly academic. There's like new SMB which I think NASA's used for a bunch of stuff. I can keep going. Then of course there's all the. Of course this is only for specifying like abstract models of systems. If you want to talk about verifying code, then you've got things like Daphne, which is basically something that compiles to like. Net and lets you basically write provable code. You've got JML for like model checking Java code. You've got like um, Primacy for like checking C. You've got ADA Spark, you've got like. And you've got Ethereum provers like um, Rock and Lean and Isabelle and I can keep going.

Speaker C: I wanted to ask, how does property based testing relate to formal verification? And before let's just like lay out what property based testing is.

Speaker B: So let's go back to that entire thing with max, right? Maximo list. We can define like the specification of max as it is in the list. And for all, all elements of the list, it is the largest element of that list. Right. I actually have a demo on my computer of doing that. So let's actually go into this. So over here in this file that I wrote for my book plug, I have a, I have basically three variants of max. A good version which just returns the max of the list, one that returns the max of the first three and then one that returns the max the absolute value. Uh, this below here is a property test. What it does is it says given a list of integers, where each list has at least one integer in it, the maximum value of that function should be in the list and all other values should be less than or equal to it.

Speaker C: Yep, clear.

Speaker B: So this basically looks a lot like our formal verification spec, our formal specification spec. The difference between the formal methods that we do and um, property testing is that the formal methods are asked are saying like, okay, can we prove this for every possible list? And property testing says well, that's very, very hard and as we talked about, very difficult to do in practice. Can we instead generate a thousand random lists and try all those? I have it set. So that way it basically has the invalid max Max.

Speaker C: The first three we should be getting errors or it should cast some errors.

Speaker B: Mhm. Let's run it. Let me just run it from the command line. That's faster. Uh, um, Pytest, uh, max py. This is an old machine I built you bring around for conferences because it's like easy to just throw on something on here. So we see over here that it says that this test failed on this line, that for the list 0001 it is not true that all the values are greater than zero. This is because as I said, our BadMax only looks at the first three values. So it found the max was zero, but here the actual max of the list was one. I broke this down to two subspecs for part of the book where we have testing that max is the largest element and also that it's in the list. So that's why one of the test passes. Um, um. I should note though that um, if I believe I run this with a verbose, what I'm trying to do for this demo is um, show that it actually does not start with the um, largest list, it actually starts with a much smaller with. Here we go. If I print max, if I print, then I do it like this. I think. It tries a lot of edge cases first. So it's basically trying huge list, is trying like tiny list, is trying like empty list, et cetera. And once it has one that fails, for example this value, it starts to shrink it finding the minimally interesting example. And that's why this lets us like find a bug. Not just find a bug, but also find a bug and present it in a way that is like comprehensive for the average human. Because I think that it found the original bug with this list and I do not think that looking at this I'm going to know what the problem is. That's basically property based testing in a nutshell. And as you can see it is less Thorough than formal verification, but it's a lot easier to apply.

Speaker C: So it sounds like it can be a nice middle ground in terms of

Speaker B: getting started with it and probably just stopping with it. Because I think that I love, uh, formal methods, but I think it's a fairly niche tool for most people. And I think like party based testing is in general going to be useful for more people.

Speaker C: So speaking of verification in general, today we have AI generating way more code. We have data to prove this as well. But also day to day, uh, I see it on myself. I have AI generate a lot more of my code, we're getting more code, code reviews are, uh, people are, it's hard to pay more attention to this. So there's a growing number of people saying, well, maybe we should somehow validate things more. And there's an idea that keeps coming up on maybe formal verification or property based testing or some of these things could be more useful. Do you think this will happen or. Because I see a lot of people talking about this, I don't really see anyone doing much about it.

Speaker B: I'm definitely seeing more business from people in my client as I Prometheus people trying to generate specs with AI and then getting me to help work with the spec or find issues with that. And I'm definitely seeing more people using property based testing. I know, for example, I think Kiro, like the Amazon Spectrum and development platform, specifically advertises generating property tests as one of the key values of it. And I've been seeing a lot of papers about generating specs using AI. I uh, will say this is kind of really exciting because as you saw like a lot of the challenge of writing a spec, not all of it, but like a lot of it is like rocking your head around like very, very technical syntax and like semantics. That said, I've been doing a lot of experience with this myself and I think the one thing AI is extremely bad at as of March, I know that Claude just released a new like Claude 4.8. So maybe this is all out the window. It's changes every month. It is very bad at coming up with properties. It is very bad at that.

Speaker C: What does coming up with properties mean? Is it writing the actual form of verification part?

Speaker B: Yeah. So like if you give it properties and like a spec, it can tell you like, hey, we're going to fix the spec to make these properties pass, that's fine. But if you basically tell it here's the spec, also come up with the properties of the spec, it'll be like, okay, so one of the properties I'm going to specify is that either P is true or not P is true. And then you're like, that's just always true. And it's like, wow, I verified it. Amazing. I'm so good at this. Especially when you deal with what's called liveness Properties. Properties about how like a system can evolve over a long period of time. It just, it's hard to put down. It's just not good at that yet. And often I find with my clients I have to tell them like, it's doing a good job at generating the actual design, but in actually expressing what the design is supposed to do, it cannot do that yet. You have to do that part yourself.

Speaker C: It's interesting because there's a, uh, there's a blog post that I'll also link in the show notes, uh, from a year ago in March 2025, uh, titled the Coming Revolution in Distributed Systems. And this was an engineer working on GitHub's copilot team. And this person wrote how AI autonomously produced precise TLA plus specifications from Azure Storage's production source code. And it uncovered a subtle race condition that had debated traditional code reviews. And then this person was very enthusiastic and saying, well, this could be a revolution. AI could just generate TLA from specification like it did with Azure. This was a year ago and I haven't heard much on any of this, even though the models were not as great. What have you seen in this area?

Speaker B: So actually the same person, Chang Huang, um, did come up with a, um, tool called Lamport Agent where they demonstrated using this to um, specify parts of um, crack. I think it's called part of deepsea's crack. I'm um, going to link both those in the thing. Here's my response because I was writing about this and then the thing that they did, he seemed to be a lot more successful than um, I was at generating properties. But um, one, at least the example that he showcased in his later piece, one, he's an expert specifier who already knows how to do this stuff on his own without the LLM. So that makes it easier. Yeah, he knows how to get good results out of it as uh, that's a general thing we've seen. To get good results you have to already know how to get good results without it. It just helps you get good results faster. And also one of the systems that he was able to create complicated properties for Intella plus already had a sophisticated spec written in P. So I don't know how much that's Relevant here. Maybe it read that and it cheated. Maybe that was like fine, I don't know.

Speaker C: But we do see this a lot where when you're an expert in a domain it may that be software engineering or like backend or mobile. AI works better for you.

Speaker B: Then there's also this one interesting person. Um, um, Claudia Colley did write a write up because she just did about a multi year project in using formal methods that the big Chinese cloud provider where she talks about how in between her like working on this paper and the time she got published, she got really sophisticated data on how long it took people to write formal methods at this one company and then LLMs basically just compressed the scale by the time she actually had the paper out. So I think people are seeing more use from formal methods. But it seems that people with the most success right now are specifiers who are using it to amplify their ability to specify. And we haven't yet really seen. I mean people post hacker news all the time. Like people who they had a AI write the whole spec for them but those tend to not be very good specs.

Speaker C: And uh, what's your take on again? I've heard some voices say that AI might make formal verification go mainstream off bait based on this. But, but outside of the. Do you see any movement outside of the this niche of people who already know how to do formal verification?

Speaker B: I think it is making it more popular. I don't know if it'll make it go mainstream but it's definitely making it a lot more popular. It's bringing it from maybe like 0.1% to 0.3% which is huge.

Speaker C: There's also this uh, this thinking that I've read actually in uh, June 2025 in your newsletter you said that AI is a specification force multiplier. And now of course we see that LLMs are bad at vibing specifications. What changed between that time where you saw that they were like a year ago they were pretty decent at doing it or they had science and now we have bit more proof they're not as good.

Speaker B: So what I wrote that it was really good at was fixing syntax errors which is really big because um, that's often trips people up. It's good at understanding error traces which is huge because being able to take like a 35 step error trace and turn that into like two paragraphs of English text. Major improvement. Good at boilerplate like mass changes to like a bunch of small things like updating like boilerplate. And it's okay at writing properties from A very precise description. It's bad at fixing specs and it's real bad at providing properties for a spec.

Speaker A: Ha.

Speaker C: Huh.

Speaker B: I'm still consistent. Yeah, so I think I called that early back then that it like is really bad. It's good at translating properties from like English, precise English into a spec, but it's bad at coming up with properties on its own. Everything got back was trivial. Understanding you're too, coupled with the implementation details. So I think ultimately what I'm going to say is that like, I think it has a lot of potential to improve things. But even back then in 2025 I was noticing that I was really bad at this one thing, that it continues to. It continued to be bad as of March of this year.

Speaker C: So then how much do you think you really need to know formal methods to be able to use LLMs to help you at all? You need to get the basics in place, likely.

Speaker B: I, uh, think getting the basics in place is really valuable here. Right? Because for one, I mean even discounting like being able to like write the properties and all that, you need to be able to tell when the AI is doing something wrong. Right. And if you don't know the basics, you can't really do that very well.

Speaker C: In your book Logic for Programmers, you argue that formal logic is probably one of the most useful parts for day to day engineering. Why is this?

Speaker B: First of all, I'm honored that you read my book, or at least the early drafts. I mean the official answer is because logic teaches us to work with like booleans and statements. What we learn in elementary, um, school. How to work with numbers. Right. Essentially there's not a whole lot of difference between knowing that one plus one is two and true. And true is true. It's still the manipulation of values. And it happens that Booleans are so important to software engineering that having some formal grounding in that is very handy, especially when we are not taught that in school for the most part. The other answer is that I've just on um, learning logic and getting better at logic and teaching logic a lot as part of teaching tla. I just finding more and more applications where I'm like, oh, because of logic, I can do this one thing. And I find that people who don't have that background struggle through that one thing. I guess I'm saying that empirically logic keeps coming up as a useful form of math.

Speaker C: And um, if I'm a software engineer and I work on complicated systems, distributed systems, what techniques would you recommend that I look into to Harden these systems. We can assume that I'm already doing basic unit testing, potential integration testing, but I'm now interested in like, well, should I look into formal methods, property based testing? If it's formal methods, there's all these different technologies. It's almost overwhelming. What is a good place to start to just do some experiments that are cheap to do.

Speaker B: I'm going to just completely go 90 degrees here and recommend this book by um, Nancy Levison called Engineering a Safer World. Um, she was an aeronautics engineer who investigated things like etheric 25 radiation case and like the Columbia disaster. And she was really fascinated in how like systems happen accidents and systems happen like why accidents could happen in complicated systems. And I found her writing on this to be incredibly insightful and incredibly valuable in understanding how these systems can break. So that's the thing at first I'd recommend is checking out that book looking

Speaker C: ahead for the industry. A year ago you wrote a post where you shared some of the uncertainties and anxieties. It was a longer post. Uh, it started with how vibe coding will be never going to solve. Software engineering. Experienced software engineers. And you wrote six different things. Can we read through them and just reflect on how you feel about them, what you think might have changed and maybe talk about what potential new anxieties we have because there's so much change going on. That's for sure.

Speaker B: The way I sort of think about it is that the next five years keep being rewritten every few months. Right? Yeah. So I wrote the following can all be true one by coders will never be good at software engineering. As an experienced software engineer, probably true. I mean if you don't have the basics, you can't really.

Speaker C: It feels true. I even see it on myself when I try to build a software in a domain I'm not an expert in, like a game. And it's an absolute just five coded mess.

Speaker B: Yeah. LLMs can significantly augment a significant a professional software engineer's ability to quickly write high quality software. I think also true. I mean even if you don't have it writing a single line of code, just being able to be like, okay, what's this bug? Where's the bug? Or like, hey, what library should I look into to solve this problem?

Speaker C: And I think we're starting to see or starting to recognize that engineers who have really deep knowledge are so much more efficient and the ones who embrace these tools and figure out how to control them and not them to control, you know, like their anxiety or whatnot, they get a lot done absolutely.

Speaker B: LLMs will cause many software developers to lose their jobs. I don't know. That's a hard one to pin down because like, I mean one, the software engineering at least in the US is starting to recover. Like we're starting to see more jobs open up for software development. So it's hard to tell how much of like the loss of the past few years was AI versus the end of like zero interest rate policy and like the post Covid crash and I think it's more the latter. But like again elements are still getting better. Maybe they're going to cause job losses in the future.

Speaker C: Yeah, this is an open question. The data that we had in the Pragmatic Engineer, it did show that we are seeing overall more software engine openings in the us In Germany and France they're declining a little bit at the same time and there seems to be um, um, a big shift on who is being hired and the skill set. So now AI engineering is increasingly spreading to more software engineering fields, not all of them. And we're seeing a decrease in for example front end engineering hiring, mobile engineering hiring. So I think the shape is changing but it's always changed in the past. If you think about 20 years ago the most in demand engineer, uh, was a Java engineer, like Java specifically like don't care, 10 years of Java experience required and that's changed.

Speaker B: Okay then we'll open up new jobs for many, possibly far more money software engine developers. I think that's also true. I think when you basically need one developer to make your product as opposed to five, you're more likely to hire one developer.

Speaker C: Right, that's been true.

Speaker B: Yep. The software jobs that LLMs open up will be lower paid and lower procedures than the heights of the 2008-22 tech era. And that's the thing that scares me the most is that as mentioned I uh, decided to leave a field and just become a techie and I was able to do that and I was able to get a well paying job that led to me to now full time mathematically prove systems Correct. That's crazy. What other field can somebody just go like? What other engineering go like? I want to be an engineer and just walk straight into it. What other field is going to send people to budapest from the US to give a talk for 45 minutes? Like it is really precious and magical what we have here and I'm afraid of losing that. I'm afraid of a uh, place where it just becomes like any other like white collar job where you get two weeks paid Vacation every year and like two days off sick and I don't want to lose that.

Speaker C: Are we saying we're afraid that software engineering might become just like every other engineering job?

Speaker A: Yes, because that is the reality of

Speaker C: a lot of engineering jobs. We do have a privilege. I don't think we talked about it when we compared with the rest of engineering. We have massive privilege.

Speaker B: Yes, we have a huge amount of privilege and I don't want to lose that. And I, I mean it'd be nice if everybody else got the same things we are, but I don't want to like equalize us by losing what makes software engineering so magical and precious.

Speaker C: Yeah, so this is a worry.

Speaker B: Yeah, that's my, that's my fear.

Speaker C: And then number six, there'll be still

Speaker B: be high paid professional software engineering jobs, but they will be rarer, more competitive and more, and less developer friendly.

Speaker C: I'm afraid we're seeing some of this already. I wonder if this is inevitable. Um, I also see it in some other industries. For example with investment banking, uh, the traders used to be many of them very highly paid, highly respected. There are now fewer of them still highly paid, highly respected. It's harder to get into them.

Speaker B: Yeah, I mean I think, I think like most jobs do ossify over time. Like as like the standards are set and more people enter them. Um, software engineering, I think for a longer period of time was able to like get away from that.

Speaker C: Yeah. And then, and then you close your prediction, uh, with these lines a year

Speaker B: ago, I predict that in the next 10 years software development will survive, but it will become like any other white collar professional work. No more $200,000 salaries, a notification or incredible employee bargaining power. I feel sad that we'll lose something so magical. But I guess it couldn't have lasted forever. Automation comes for all of us, even us automators. Here's a, here's a good way of ending. This actually fits in the backlink. If we start with. Automation comes for all of us, even automators. And like on one hand I feel like I'm losing something really special. On the other hand, a doctor friend of mine came to me like a few months back and was like, hey, we managed to like create a new shift scheduling platform for like our hospital, like to trade shifts. That really saved us all a lot of time and like made all of us nurses and doctors so much happier. And I was able to just vibe it out. I don't know any kind of code but like AI let me do this and I'm like, wow, it really is helping you, like, and your hospital make your life better. And it's like, it feels so weird to balance my needs as a professional software developer with like, his needs as a doctor, like, who matters more, like my cushy job or his job, Like, I don't know. And it's gonna, we're gonna all find this out in the next 10 years, I guess.

Speaker C: Grady Bush told me that this time reminds him of the time in the 19, late 1960s and early 1970s where people could purchase computers and start to hack with them. And he said it was a magical time because teachers and people who had nothing to do with software saved up and started to just hack around and it democratized it. And I feel, uh, this is the first time I'm also feeling like this other person at the gym told me that they're vibing something together. It feels it's opening up the field and if anything, a lot more people are realizing, oh, software is cool, I can do it. And now they're starting to learn the hard parts of software engineering eventually.

Speaker B: Did you ever read up Clay Shirky's essay Situated Software? No. Basically what it is is that this person was talking about, um, how they think, like the most important. The vast majority of software should be made for like three people or like a, uh, family or community or like one school. And up until now that like, could only really happen if one of those people in that family, that community or that school was like really, really into computers. But now it's possible for everybody to have situated software. And that again is going to change the world in some strange and some terrifying and some exciting ways.

Speaker C: It's exciting as closing. What are books? Uh, a few books that you could recommend that you have enjoyed or made an impact on you.

Speaker B: Hoo, boy. Let's just leave this just for this into just software books, okay? Because otherwise we're going to be here for like a month. So there's three books that I really love in software that I think of as like the books that have influenced me so much. The first one I think I mentioned in the interview was Nancy, um, Levison's Engineering a Safer World. I believe that's actually free online. The second book is called Data and Reality by, um, Bill Kent. And this was actually hard to find because it was republished in 20, I think 11, but the republisher changed the book. So the last good edition is the second, uh, edition, which can be found like in dark corners of the Internet online, is actually kind of hard, but like it is basically by this, like, famous database designer who, like, worked on IBM databases, who was just asking, like, what is data? What does it mean for something to have an identity? What does it mean for something to have oneness? If you talk about a book, is that the book, the physical copy, is that the series, is that an addition? And it's just an entire book about these questions about what data is and how we need to represent it. He ends it by saying that data isn't reality, it is our view of reality for our useful purpose. This incredible book, it totally changed how I think about things. The last book is, um, called Debugging the Nine Simple Rules by David Agans. And it's literally just like a book of war stories about debugging and, like, basic principles. But this is the book that I give to every junior engineer because I think, like, nobody ever really talks about debugging as, like, a discipline outside of, like, basic heuristics. And this is like, just at least something that's trying to do that. And having something is better than nothing in this category. So really good book. And I think it's like $10 for a used copy, so, like, anybody can just get one. It's great. Those, I think, are the three most useful books for software engineers. If you want to talk about other books, I can keep going, but this is great.

Speaker C: Well, Hillel, this was very educational, uh, and, um, I found it fascinating. Thank you.

Speaker B: Thank you.

Speaker A: I really enjoyed this conversation, especially the demos where Hillel showed tools like tla, Alloy, or Hypothesis and how they can catch bugs. By the end of the conversation, I'm starting to understand, um, more why it's not likely that formal verification will go mainstream, even with AI. I mean, these tools feel very rigid for the real world, for specific parts of a system that you can model mathematically, like state spaces, sure, they can

Speaker C: work, but for everyday programs, it just feels like it would be a bit

Speaker A: pointless to create TLA specifications. One thing that I was always also thinking about is how Hill talked about why he thinks we're not good at catching concurrency bugs, and it's because we don't have much practice with them. As a developer, you're lucky to debug a concurrency bug once every few years. So of course you won't be able to build expertise this way. This is also similar to how most engineers are bad at migrations, because most devs, uh, only ever do one or two migrations over several years. But if you're an engineer who does a bunch of migrations, you're going to be really good at them. Same thing if you're working on systems with concurrency issues and you become an expert in this. I also find it fascinating how other engineering fields have similarities with software engineering, like how mining engineers had their own Agile revolution in the 1960s and how all engineers hate the concept of waterfall. Plus, it was amusing to hear how source control is kind of an envy from other engineering fields that we software engineers have, but not many others do. Check out the show notes for related deep dives on distributed system at Tech Depth that go into more detail into the topics that we talked about today. And if you've enjoyed this podcast, please do subscribe on your favorite podcast platform and on YouTube. A special thank you. If you also leave a rating on the show. Thanks and see you in the next one.