Formal methods with Hillel Wayne

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 is correct. Today, I'm talking with one of the best people to respond to this, Hillel Wayne, a formal 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, Hillel's research interviewing 15-plus 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 question, 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. Antithesis 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's 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 Antithesis. Antithesis turbocharges testing by running your whole system under aggressive fault injection. Imagine Antithesis as hundreds or thousands of versions of the Mario game running, each instance aggressively trying to break the game with increasingly weird input combinations. With Antithesis, you can specify properties at the whole system level, and Antithesis 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.com slash pragmatic to learn more. So hello, welcome to the podcast. Thank you so much. I'm really excited to be here. It's so nice to have you here. I was curious, you're very well known for formal methods, for programming, for logic, for all of these topics, but how did you get into tech? So to start, I never really saw myself as a technical person. I liked 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 high schooler for writing, 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 developer, a Ruby on Rails developer in education technology. After some time, I 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. 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 software engineers actually engineers? Yes. Can we talk about this project? 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 consider ourselves in the same space. And then other 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 one. 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, 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 compared 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. Can we go a little bit into it? So as I started talking to the first people, I realized that this was a much deeper project than I ever expected. And 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 it 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. And what were the similarities that you found that software engineering has with either specific types of engineering or across the board? If I had to summarize what I found in general, I'd put it like this. Everybody hates waterfall. No way. The 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're 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, etc. 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. Interesting enough. I heard the term smoke test originated from This many years later, what is your inclination? Are we actually engineers? I think so. I think this project and writing about it 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 such a cool project and still a very good read. 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? 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? 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 ones. Maybe I'll take it to maybe eight if I'm feeling super ambitious, and then I'm done. Okay, so when we take one of those tests, how do you know what the right answer is supposed to be? I just know because I have a, I learned math, so 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. 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 formal methods 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, 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, okay, in every single case, we are putting in a list of elements and we're getting out a single element. So you 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 formal methods ask 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. And then in proof, again, from university, I still remember the maths proofs where we would prove 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 typically start from a complicated equation and you keep changing it. And in the end, you shape it in a way that it's now trivial or you transform those. Those are the ones we do. Is this what formal methods also does to some extent? Yes, but do 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? 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. 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, okay, at this point, I'm going to also let you know that this is true. And it'll be like, okay, I can verify that's true, and it'll help 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, so with formal methods, I mean, this sounds all logical. I think it's easy to follow in practice. What techniques, technologies, tools does the industry, use the tech industry, use to actually prove that, you know, some software works? To get to that, we need to ask another question. Why isn't this being done for everything? Okay, let me ask that question. That's a good question. Yeah, this all sounds sensible. It would 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 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 test case. I know I'll have nine tests, and now I go and think I did a great job. Why are we not doing formal testing for everything? 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? Well, now I'm thinking of writing a program that, in kind of an imperative style, it goes through four lists. Each file, I list how long the lines are. I count the lines. I cannot tell this easily. Okay, are we talking about ASCII lines or UTF-8 new lines? What happens when 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 function might be wrong? You're now trying to confuse me here. What if one of the files is a shortcut to another file? What if it's actually a directory? You're now simulating real world. 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 it correct 99% of the time is probably good enough to use in almost all cases. And if you want something that works 100% of the cases, you've got to figure out, okay, what file system are we using? You have to figure out everything. Yeah, and that's why it's not done. And it would just not be practical. It would be for 99% of the people, why are you wasting your time? It's like premature optimization, right? Yeah, especially when, as you say, writing 10 tests might get you most of what you need. What are practical technologies that you have seen used in some part? The way it works is, it's on a small screen, so it's being word-wrapped, but if I can 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 .file. dotvis, graphvis, not dotvis, what am I saying? So this is just 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 a hundred million states for 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. 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. And then how did the system simulate this? It had to simulate a state where Bob was waiting, or didn't respond for a while and responded later. We basically, assuming we started the state of basically Alice owns the stick, there's two possible things that can happen here, right? We have offer Bob, 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, Bob reject, or, and this is where the concurrency comes in, we can do offer Carol, right? Yep. I see. Yeah. I see where this is coming. And then when you continue, we will hit the bug. Yeah. The change invariant will be invalid at whatever step that is run at. 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 one takes step one, then process one takes step two, then process two takes step one, then process one takes step three, then process three takes step one and two, then process two takes step two and three, et cetera. And being able to sort of see every possible iteration 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. Yeah. So, so this is what TLA plus is then. Yeah, basically. And one story I've heard, and I think you might have been involved, is AWS using TLA plus. 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? Yeah, so the seminal paper on this was in 2014, the use of formal methods at Amazon Web Services. And they talked about how a couple of people in the company were interested in it, and learned TLA plus and another language called PlusCal, which is something that compiles TLA plus, 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. 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 needed to be really determined and precise. 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 happened this one 35-step chain was invalid. Through working with a lot of customers and teams that have used formal verification with distributed systems, what are some problems you've come across with distributed systems that might be a bit of a repeat pattern of you know how they break down or why they break down? If I can think of like one thing that like, besides like just general race conditions and locks, this is the one that like, is always in the corner. I was like, yes, it's another time to allow a time to check a time to use bug. And time to check a time to use 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 it's 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 example here is, imagine you're withdrawing like money from a bank account and putting it into 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 and grabs those $10 away. And now there's $0 and now you deduct those $10, you have negative $10. That's a time to check a time to use kind of bug. They happen everywhere. 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 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 it turns out it's a complicated problem. It's a lot easier to do at least once delivery than exactly once delivery. But of course, you need exactly at least once delivery to build on to create exactly once delivery. Yeah. I wonder if this is why a lot of like businesses, they just charge you extra and then refund you some amount. That seems like easy to do from engineering perspective. As well, it's also from a risk perspective. You eliminate a lot of edge 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 run into the thing where you would run out of your credit and now they have to do a separate flow. So math does help a lot in understanding those. Yeah. And with the TLA plus specifically, what cases have you seen in the industry TLA plus being a good fit for certain problems? And in what cases would you never consider it? I think the case of TLA plus and most, not all, but most formal 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, and I'm trying to think about like a good example here, like how do we make sure our sprints don't go over time? It's very business, right? It deals with like very human behaviors. So I've had to help a 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 harder 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 tools are good at different things. TLA plus in particular tends to be good at discrete distributed systems where the main challenges are messing with concurrency and possibilities of interleaving like behaviors. It doesn't do floating point, it doesn't do decimals. It doesn't do as well 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 ones where like if it is possible for it 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 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, 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 emphasizing 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 that 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. And then can we talk about other, other tools or can you show us a few other ones? 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 this lineage, just like there's 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 readable by and resources may or may not have a parent resource. L1 means L1 being less than or equal to the one resource. There are no cycles, so no resource can have itself as a parent or its parent's parent as a parent. Yep. 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. Yep. This system has a bug. What is it? I mean, I'm glancing at this and this all makes 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 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? Yes, we can. So this was actually made in an earlier version of Alloy, just for just for context. Um, 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 of basically how you can analyze and find bugs in static configurations. And 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 interestingness 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. If I execute this. Here's the counterexample. Right. And this is one of those things about Alloy specifically is that it can generate like 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 can access, we can read his parent, so we can read the child. Yes. The child has a grandchild. We cannot read the grandchild. So because we are not in, we are not assigned to the readable byte for the child, only the parent. In other words, readable byte is not transitive. So we can read the child, but not the child's children. And that is the bug. Mm-hmm. And it visualizes for us. Yes, which is quite nice. And one of the reasons why people really like Alloy. Nice. It's a bit worse for modeling like distributed systems though, which is why most of my work is in TLA plus. And then to do the fix, what would it involve? We would need to give access to the children's children. Yeah, there's a few different ways that we could fix it, and often like formal 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 look up 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 different things. So this is the beauty of formal methods. Yes, it gives you the gives you opportunity of how you will implement fixes, changes, and then you can rerun it again and see what difference it made. Exactly. Now, one quick fun fact. I love just fun facts about stuff. You see how this says solver SAT4J. So have you heard of SAT, SAT problems? No. 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 see if 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? I 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 wrapping 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 changes every month. It is very bad at coming up with properties. It is very bad at that. What does coming up with properties mean? Is it writing the actual form of verification part? 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 a spec, also come up with the properties of this 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. It's interesting because there's a blog post that I'll also link in the show notes from a year ago, in March 2025, titled The Coming Revolution in Distributed Systems. And this was an engineer working on GitHub's co-pilot team. And this person wrote how AI autonomously produced precise TLA plus specifications from Azure storage production source code, and it uncovered a subtle race condition that had evaded traditional code reviews. And then this person was very enthusiastic and saying, well, this could be a revolution. AI could just generate TLA plus 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? So actually, the same person, Chen Huang, did come up with a tool called Lamport Agent where they demonstrated using this to specify parts of crack, I think it's called, part of DC's crack. I'm 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 have be a lot more successful than I was at generating properties. But one, at least the example that he showcased in his, like, later piece, one, he's an expert specifier who like already knows how to do this stuff on his own without the LLM, so that makes it easier. Yeah, he knows how to like get good results out of it. And that's the general thing we've seen, like, to get good results, you have to already know how to get your results without it. It just helps you get good results faster. And also, one of the systems that he was able to create the complicated properties for on TLA 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. 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. Then there's also this one interesting person. Claudia Colley did write a write-up because she just did about a multi-year project and using formal methods at the big Chinese cloud provider, where she talks about how in between her like working on this paper and like the time she got published, she got really sophisticated in 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 like more use from like formal methods, but it seems 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. And what's your take on, again, I've heard some voices say that AI might make formal verification go mainstream based on this, but outside of the, do you see any movement outside of this niche of people who already know how to do formal verification? 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. There's also this uh this thinking that I've read, actually in in June 2025, in your newsletter you said that AI is a specification force multiplier. And now, of course, we see that LLMs are are bad at vibing specifications. What changed between that time where where you saw that they were, like, a year ago they were pretty decent at doing it or they had signs, and now we have a bit more proof that they're not as good. So what I wrote that it was really good at was fixing syntax errors, which is really big because 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 it 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. Ha, I'm still consistent. Yep. So I think I called out earlier back then that it like is really bad. It's good at translating properties from like English-processed English into a spec, but it's bad at coming up with properties on its own. Everything that back was trivial, understanding are too covered with 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 it was really bad at this one thing that it continues to be, it continued to be bad at as of March of this year. 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. I 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. 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? First of all, I'm honored that you've 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 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 learning logic and getting better at logic and teaching logic a lot as part of teaching TLA plus, 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. 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. So if you want to talk about other books, I can keep going. But this is great. Well, Hillel, this was very educational, and I found it fascinating. Thank you. Thank you. I really enjoyed this conversation, especially the demos where Hillel showed tools like TLA plus, Alloy, or Hypothesis, and how they can catch bugs. By the end of the conversation, I'm starting to understand 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 work. But for everyday programs, it just feels like it will be a bit pointless to create TLA plus specifications. One thing that I was also thinking about is how Hillel 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 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 systems and tech debt 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.