The Pragmatic Engineer - Formal methods with Hillel Wayne

Episode Date: July 29, 2026

Brought to You By:• Antithesis – verify your system’s correctness without human review or traditional integration tests – and avoid bugs or outages.• turbopuffer – a vector and full-text search engine built on object storage. It’s fast, cheap, and extremely scalable.• WorkOS – everything you need to make your app enterprise ready.—There’s a popular theory that AI will finally make formal verification mainstream because mathematical proof of correctness will be needed when machines write most or all of the code. But will this happen? Today, I’m talking with one of the best people to tackle the prediction. Hillel Wayne is a formal methods consultant, educator, and author, who’s deeply interested in software history. In this episode of Pragmatic Engineer podcast, I sit down with Hillel to compare software engineering with traditional engineering, discuss where formal methods fit into modern software development, and we explore why they are essential for some of the world's most complex systems. We cover the formal specification language, TLA+, walk through several formal verification tools, examine why distributed systems are so difficult to reason about, and look into whether AI will make formal methods accessible to more engineering teams.—Timestamps00:00 Intro03:21 The Crossover Project10:26 What software engineering does better14:19 What traditional engineering does better17:06 Formal methods28:21 TLA+: what it is and demo35:47 TLA+ at Amazon36:59 Ways distributed systems break39:52 Formal methods and systems thinking45:09 The value of learning math49:12 What TLA+ is good for and isn’t51:39 Alloy: a declarative language for software modeling57:42 Other formal methods tools1:00:13 Property-based testing1:04:20 AI and the need for formal verification1:11:18 Logic for programmers1:13:24 Hillel’s 2025 prediction on AI’s impact1:20:19 Book recommendation—The Pragmatic Engineer deepdives relevant for this episode:• How to debug large, distributed systems: Antithesis• How AWS S3 is built• Paying down tech debt• How Big Tech does quality assurance (QA)• Bug management that works• Resiliency in distributed systems—Production and marketing by ⁠⁠⁠⁠⁠⁠⁠⁠https://penname.co/⁠⁠⁠⁠⁠⁠⁠⁠. For inquiries about sponsoring the podcast, email [e-mail]. Get full access to The Pragmatic Engineer at newsletter.pragmaticengineer.com/subscribe

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, Hilo-Wain, a formal method consultant. He's taught TLA Plus, a popular formal specifications language across the industry, wrote the book Logic for Programmers and will soon be joining anticesis. In today's conversation we discuss the crossover project, Hello's research interviewing 15 plus traditional engineers to answer the question, can software engineers also be considered real engineers?

How AWS used TLA Plus. 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, Anticisys. Anticisys verifies your system of 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 ADW is distinguished engineer, Mark Berker, and Anchorage, aside have described as lightweight formal methods. Setting aside Enstis 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 Intestis. Anticis. Tuprocharges testing by running your whole system under aggressive fault injection. Imagine Antisces 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 Intestisysic, 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.I.O, and the etcd community rely on

antitisesis. Head to antitcum.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 tactical 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 high schooler for writing, just saying. But after about three years of doing this in college,

I realized that I kind of like 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, want to 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 went 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 as engineers. We should not. They are so far above us, we shouldn't even like consider ourselves in the same space. And another of 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, this is real engineering and everything else is not engineering. Then I found this talk by Glenn Vanderberg, 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 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 kinds of 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 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, have the ability to come up with the design, tested, 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 electrical engineering, actually. I did not look into that, but I could believe it. Yeah, apparently, it's when you have a test circuit and you just hook it up, and 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? 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 toxic 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, of course correcting based on that. Okay, so I guess we all hate waterfall. We all hate waterfall. Or the idea of waterfall. Yeah. 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 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 talked 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 even those fields can. I think we all kind of know this. One thing that we might not realize the software engineer is that our work is a lot more consistent in 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 like a spec sheet, it says, this resistor has a resistance that is within 20% of 100 oms, 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 or run on your computer, exact same. Sort this list of the exact same if it's sorting algorithm. Does this also mean that we might not account for variability as much as other engineering disciplines do? I'd say so. The variation of you have to deal with is kind of our own making, right? We're basically saying, okay, we've got all these different systems, all these different APIs versus

other people are like, we have all these different chips, 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 bigger than others and some are a little bit smaller than others, if are a bit longer, et cetera. And how did you see the similarities or differences of software engineers,

for example, often interact with customers with end users who use a 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. I think it depends because different engineers that talk 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.

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 better place, is open source. the concept of open source. 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 crap 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 what we do. We also are really the only kind to really focus heavily on open source and making our knowledge really 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. I wonder why this might be both 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 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 thus 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 what did we do to get here. 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 lades

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. Interesting how I like this thinking of materials used in each engineering and how our material is software itself. 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 and how they, how much they share, how much we know about them and so on. I kind of wonder, I've got some friends to do like 3D printing, and it seems like, and I haven't looked into this, but it seems like they also have a very open

space of like sharing things freely. 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, if that kind of leads to the same thing. 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, hammer radios, which is not enduring, but there's a thriving community where they share the setup, the things, they talk with each other. Small electronics might be. And then, but ultimately software

started in the, what, 70s when it was affordable, anyone could buy a computer, maybe the internet, I'm also just speculating. Yeah. Definitely something worth doing a follow-up project on, right? Well, you've already spent a bunch of time on it. Don't give me so many rabbit holes. There's already too many rabbit holes in my life.

One more thing that you brought up is version control. And the fact that in software, we just take it for granted. We have virgin control everywhere. And you said that this is super unique across most of engineering. 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 there are things that now having talked with so many people

and learned about the different engineering cultures, like actual traditional engineering cultures, what could we learn from? them? What are some kind of inspiration that might be useful here or there? Yeah, this is a harder question because while everybody 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 slowly 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 every day things, which he recommends every engineer read, and the SNAT Fit handbook. Are you familiar with SNAP fits? No. Looking around here to see if there's like one, if I could just show it,

but like, you know how remote they have that little clicky thing in the back that you use that hold the battery in? Yeah. That's a snap fit. 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 fits. They're engineering, appropriate shapes, materials, etc. 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. We could all use that.

Yes, we could. And we don't have it. We could learn it from engineering. We should have that. You started this project asking, are we really engineers? And your personal inclination, which you didn't say at the time, was 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? I think so. I think this project and writing about and thinking about it has firmly moving from the camp of we are definitely not to we probably are. I do want a 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 it's still a very good read. I'll also link it in shown

those 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 in 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 tests. 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. Okay. So 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 no, 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 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 to the list, and it is the number in that list such that every other number of 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 come forward to 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 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 phone method is 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 proof 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 shape it in a way that it's now. trivial or you transform though those are one of the proofs we do is is this what formal methods also does to some extent yes 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 i now use a calculator if it's easy enough it might i use my brain as a calculator otherwise i just punch it into the calculator yeah so similarly a lot of problem methods that math and transformation while you can do it by hand with like what's called a theorem prover often in industry that it's 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 know 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's 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. So with Foreman Method is this, 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 softs 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 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 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 how of 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 to a four list each file. I list how long the lines are, I count the lines. I cannot tell it easily. Okay, are we talking about ASCII lines or UTF and new lines?

What happens with 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 not 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. What is a binary? You're now simulating in 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, 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're right 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 100% of the cases, you've got to figure out, okay, which 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 will be, for 99% of people, why are you wasting your... 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 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 of investment of using this heavyweight stuff is worth it that teams in the industry are using it today. Right. 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 NASA, but I can tell you for the first-hand 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 small parts

of databases or like cryptographic and primitives. I believe that the HTTP stack in Firefox is verified as part of something called Project Everest, but I might be getting some details of those wrong. 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?

Yeah, parts of them as operating system kernel are good uses for this. A couple of examples I can think of is, I believe Microsoft used some formal verification on parts of their Bista 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 microcernel. It's very small. It's mostly used for 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 system and verify that. then the actual system might still have bugs, but we can iron out the issues in the abstraction such that we don't actually build them in the real system. And so that's the topic where you are planning a system

and you want to stress test it to iron out. Yeah, stress test the plan. What kinds of plans would these be roughly? Is it planning like a database or some sort of distributed system? In my work, it's mostly been 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,

firmware of a device kernel. And one, honestly, one of the coolest products I ever worked on was 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. 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 season sponsor, WorkOS. If you're building any SaaS, especially an AI 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, skim, and fine-grade 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 at Workwise.com. I also want to talk about our season sponsor TurboPuffer. But this time, I don't want to talk about how they are 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 onstage at AI Ingeers 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 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 10-15 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 a reason that object storage is turbo puffers-only dependency. The team do seemingly silly things like build their job queue in a single file on object storage, 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 slash pragmatic. And with this, let's get back to how TLA Plus works with a demo from Hillel. Can we see a demo? Okay, sure. So I've got a couple languages with me, the kinds that I've worked in. So the most popular technology right now for that kind of planning is this language called TLA Plus. It was invented by Leslie Lamport, the same guy who made Laotech, the typesetting language, actually.

Oh, yeah. All the PDFs behind his scenes are Lata. Yeah, PDFs behind the scenes are Lotech. And he wanted a language that could be used to model distributed systems. So he basically created this thing called TLA Plus, temporal logic of actions plus. Everybody always asks about the name. You don't need to know the name. You just don't as TLA Plus. 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, 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 remove from the set. Then we define what can happen next. A next state, as in one of the ways this isn't 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 that finally we have a change in variance, some property of the system, saying every change is a valid change. Now, what's the bug in this? Well, first of all, this has a learning curve. Yes, it has a learning curve. and that's why this is fairly niche.

And I should probably point out right now that when Lesothan Amper made this in 1990, like four, he was thinking of it mostly, he was a mathematician, right? So he was using his mathematical, like, background and, like, reading how a mathematician would write some symbols. In the 30 years since that point, price, it's been 30 years since 1994 already, a lot of languages have been developed in part from the lessons of LerTLA Plus that made things are a little bit more appealing to programmers. So you have things like Quint and P.

which are languages that look more like programming languages and are easier for people to grog. The reason a lot of us use TLA Plus was because the first really high profile demonstration of this kind of work in practice was an Amazon paper. The use of formal methods at Amazon Web Services in 2014 and they used TLA Plus for this.

So that's what a lot of us just have originally started on. So going back to this, there is a bug in this one with all the associations. And how can we figure out what the bug is? Will the system help tell us or we now need to think through of what case we miss? Well, if we had to think through it ourselves,

we wouldn't be using this nasty syntax, would we? Nope. So what I've done is I've also written a quick configuration file saying, take this 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 in variant always holds.

Now I just have to run this. I'm also having it output a 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 dot file. dot biz, graphiz, not dot biz, 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 states traces end up being like 100 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 errors 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 out 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 in a variant 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 awaiting or didn't respond for a while and responded later.

We basically, assuming we started to say, basically, Alice owns the stick. There's two possible things that can happen here, right? We have offer Bob. Yep. 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 Carroll, right? Yep. I see. Yeah. I see where this is coming. And then when you continue, we will hit the bug.

Yeah. The change of variant 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 will be like, okay, process one can do one of six things, process two can do one of six things, process two can do one of six things. And when you do this report, 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, and two, 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. Yeah. 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 prolethe's at Amazon Web Services. And they talked about how a couple of people in the company were interested in it and learned TLA Plus in 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're 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 needs to be really determined and precise. I did not work on that project, of course, so I don't know what the details are. I can speculate that the reason it found a 35-step bug was because the state's base was probably 100 million stateswide. So there were like plenty of say like 70 or 80 step chains that were totally safe.

And just having this 135 step chain was invalid. Through working with a lot of customers and teams that have used form of a 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 how they break down

or why they break down? And I can think of like one thing that like besides like just general erase conditions and locks, this is the one that like is always a new point in my hair and it's like, yes, it's another time to allow it, time to check and time to use bug.

And time to check time to be use is a situation where you are checking to see if something is like valid and 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 example here is imagine you're withdrawing like money from a bank account and putting 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 they're $0. And 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. Yeah. And it's very interesting because when you're 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 turns out it's a complicated problem it's a lot easier to do at least once delivery yeah than exactly one's delivery but of course you need exactly

at least one's delivery to build on to create exactly one's delivery. Yeah. I wonder if this is like a lot of like on 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 off front 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. 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 engineering decisions might happen because it's easier to do some stuff. Yeah, it makes sense. I honestly thought hotels did that because they're trying to convince you not to break stuff. Because like, hey, if you know that you're definitely going to lose $800 if you break something, like you're not going to break stuff. Through working with engineering teams who are building distributed systems

and you're coming in and helping them learn TLA plus 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? 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? 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. 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 flow charts are good for whiteboarding. 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 a concurrent system? You're just, there's cars everywhere. They're going to hate 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 commonsense computing, where some people were trying to figure out like how people thought about concurrent systems.

When talking with like sort of like high school and college students, they changed a concurrency problem from like, hey, we've got the concurrency problem from like, hey, we've got these threads doing some operation to, like, hey, we've got these, like, clerks at a ticket office assigning seats at a concert. People saw the bug much faster. 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 Plus, like, I write my model of the system and then I click a button and it tells me, hey, race condition. And then you fix it and says, like, hey, timeout bug. And then you fix it again and says, hey, TOC, TOU 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 distributed systems more easily. I've found personally that when I work with new clients and remodeling their system, I usually have no idea how their system works, right? Because they're the domain experts. I just have

to know this 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 and seeing how those systems can go wrong so much faster. I wonder if it's a little bit like refactoring and also migrations. 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 name and then you need to go

and change all the reference to that function. And the first time you do it, 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 keep in shadowing, reverse shadowing, all that bunk. And then there are a few engineers who have done three or four or five and then you, 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 the second one. So I will not be good at finding race conditions. I am not even good at thinking about them. I think that's right on the money. It sounds like you coming into team. or to these clients, you have these give them some practice, the very least,

of how to think about this category of errors, even assuming that the, taking out even the tooling itself. 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.

You've been doing this for very long. For you writing TLA Plus is, like, for most of us writing TypeScript or the language that we're familiar with, how has your thinking changed? And 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? And that also depends on a declarative language. Like, 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, show me to see this time.

I'm just like, what is this dark magic? Declarative, what are you talking about? I think so. It's going to be hard to sort of pin down exactly what though. My usual haggling 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. Math is also an interesting topic. 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? How math is useful? 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 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.

It's also very interesting because for a long time I thought at university we have pretty heavy math education and for computer science from algebra to computational theories, even formal methods. At university, I learned the budget of advanced math. 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, matrix transformation. I learned 3D graphics and how you compute all the points based on 3D 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 in that, I feel 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 not going to shy away from it. I can start reading it and I will know 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 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. 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 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. Interesting, yeah, because the math that I did use more was common atyroics. And of course, like, maybe these days those interviews are going out of style, but there's the,

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 a big old notation. We have the language to describe how efficient in space and time is. And you can do tradeoffs and you can. And once two people know the same thing, you can have. have discussions about these things. And it's on one end, it's very abstract, but on the other end, if you're close to the

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

And with the TLA Plus, space. specifically, what cases have you seen in the industry, TLA plus being a good bit 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 moral 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 to replicate nodes between these two data sets is like very technical, right? Something like, I'm trying to think about like 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. 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 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 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 ones where like, if it is possible with 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 100 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 it 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 is 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 constantly be 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 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. And then we talk about 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 formathous 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 reasonable by and resources may or may not have a parent resource. L1 meaning less than equal one resource. There are no cycles.

So no resource can have itself as a parent or its parent's parent's parent as a parent. Yep. You can read access to resource if the resource indicates you can read that resource or if his parent indicates you can read that resource. And we have a property that if you can read a resource, you can read as children.

Yep. This isn't as a bug. What is it? I mean, I'm glancing at this, and 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 there is one as 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, earlier version of Alloy, 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 examples I used from before then 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 those things about Alli specifically is that I 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 as parent so we can read the child. Yes. The child is. has a grandchild, we cannot read the grandchild. So, because we are not in, we are not assigned to the readable by for the child, only the parent.

In other words, readable by is not transitive. So we can read the child, but not the child's children. And that is the bug. And to visualize this 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, full 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 counter example. 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 administrator is like, no, that's going to crash the database. You can't do that. Then we have to find a different fix.

So this is the beauty of formal methods. Yes. It gives you opportunities 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 SAT 4J. So haven't heard of SATSAT 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 say P is a bullion. And I have a statement P. Can you assign some value of true or false to P to make that true? Typically, you can assign true and it will be true.

Correct. Well, true. So that's even a satisfiable by citing P to true. What about P and not P? also satisfiable by giving true to P and false to Q. Right. Now what about P and Q and not P? That's unsatisfying.

That unsatisfiable because no matter what bullying you do, true and false will always will never be true. Lovely. What you've just done is a bullying satisfiability problem. Taking some sort of statement of a ton of bullying variables in this case too and found some, either found some assignment that makes it true or said that it cannot be made true.

Now, bullying satisfyability is what we call MP complete. And what that means in theory is that there's no such thing as a perfectly efficient algorithm that solves all problems. In practice, that means that we can solve them really fast. So often what makes Alloy interesting is that only TLA Plus, 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 bullion probability, saying not X-21 and X-96 and X-15 or not X-72, et cetera. 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 plus model, you have to basically churn it overnight to go through all 100 million states. Can we talk about some other tools on the, like as a table of someone looking into form of verification? 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 successes to TLA Plus is the P language, 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 Plus. other things. So it basically looks like a set of state machines, interacting the same machines that send messages to each other almost like the actor model in like Erlang or something like that. So there's that. There's also another one in the same space as I'm Quint, which was

basically people who were making a different kind of model check for TLA Plus 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 I believe cryptocurrency space, smart contracts. So another one that I've

views, which is a lot more niche, but quite interesting, is called Prism. And Prism is a probabilistic mile tracker. So, like, TLA Plus 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 is a 25% chance of happening if you shut down. It's really cool, but it's also much more, like, academic in that there's a lot more required to actually translate languages into Prism. If you're interested in it, I've basically been doing this, like, have you heard of the

Jewish game Dradle? No. Okay, it's a game that you play on Kronica 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 it as a mathematical thing. Love it. Those are, I think, some of the ones that are like really popular. There's also, I mean, I could just keep listening. There's like, there's like Event B, which is like been used, I believe famously in part of the Paris metro system.

there's like MCRL2 which I think is comes from a Dutch university HemeraX which is mostly used for like robotic control systems but I think that's mostly academic there's like new SMV which I think NASA is used for a bunch of stuff

I can keep going then of course there's all the 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 dot net

and lets you basically write provable code you've got JML for Java check for like model checking Java code. You've got like Brima C for like checking C. You've got Ada Spark. You've got like, and they've got the theorem proofers like I'm rock and lean and Isabel and I can keep going. I wanted to ask how this property based testing relate to formal verification. And before let's just like lay out what property based testing is. So let's go back to that entire thing with Max, right?

Maxible List. we can define like the specification of max as it is in the list and for all elements of the list, it is the largest element to 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 the one that returns the max the absolute value.

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 equal to it. Yeah, clear. 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 property testing is that the formal methods are saying like, okay, can we

prove this for every possible list? And probably 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 of those? I have it sets that way it basically

has the invalid max. Max the first three. We should be getting errors or it should cast some errors. Let's run it. Let me just run up the command line. That's faster. pie test test max. pi.

This is an old machine ability to bring out 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 0-0-0-1,

it is not true that all the values are greater than zero. This is because I said our bad max 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 subspecks for a 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.

I should note, though, that if I believe I run this with a verbose, what I'm trying to do for this demo is show that it actually does not start with the 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 lists, trying, like, tiny list is trying, like, empty lists, 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 a percentage 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 what can't decide and 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. So it sounds like it can be a nice middle ground

in terms of getting started with it. And probably just stopping with it because I think that I love formal methods, but I think it's a fairly niche tool for most people, and I think like property-based testing is in general going to be useful for more people.

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. I see it on myself. I have AI generate a lot more of my code. We're getting more code. Code reviews are

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 or maybe formal verification or property based testing or some of these things could be more useful. Do you think this will happen? Because I see a lot of people talking about this. I don't really see anyone doing much about it. I'm definitely seeing more business from people. In my client, as I'm with people trying to

generate specs with AI and then getting me to help work with the spec or like find issues with that. and I'm definitely seeing more people like using property-based testing. I know, for example, I think Kiro, like the Amazon Spect-driven development platform, specifically advertises generating property tests as like one of the key values of it. And I've been seeing a lot of like

papers about generating specs using AI. 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 rocking your head around like very, very technical syntax and like semantic.

that said, I've been doing a lot of experience to 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, Cloud 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 on with properties mean? Is it writing the actual form of verification part? Yes, 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, I'll 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 live in this 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 out 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 will also link in the show notes from a year ago in March 2025 titled The Coming Revolution and 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's production source code and it uncovered a subtle race condition that had debated traditional code reviews. And then this person very enthusiastic and saying, well, this could be 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, Chang 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 DFC'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 do have to be a lot more successful than I was generating properties. But 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 easier. Yeah, he knows how to get good results out of it. As this is a general thing we've seen, like to get good results, you have to already know how to get good results without it. It just helps to get good results faster. And also, one of the systems

that he was able to create the complicated property for NTLA 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 Collie 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, 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 LMs 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 well 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 tachron news all the time like people who like they had a AI right, 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 form of 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 thinking that I, I've read. Actually, in June 2025, in your news article, you said that AI is a specification

force multiplier. And now, of course, we see that ELMs 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 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 boilplate. And it's okay at writing properties from a very

precise description. It's bad at fixing specs and it's a real bad at for fighting properties for respect. Ha, I'm still consistent. So I think I call that early back then that it like is really bad. it's good at translating properties from like English Prethice English into a spec, but it's bad at coming up with properties on its own. Everything got back was trivial, uninteresting or two 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 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, bullions 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 bullions 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'm just on learning logic and getting better logic and teaching logic a lot as part of teaching TLA Plus, I just finding more and more applications around like, oh, because of logic, I can do this one thing. And I find 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. And 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? I'm going to just completely go 90 degrees here and recommend this book by Nancy Levison called Engineering a Safer World. She was an aeronautics engineer who, inventing.

investigated things like Etherick 25 radiation case and like the Columbia disaster. And she was really fascinated in how like

systems have been 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 ahead for the industry year ago, you wrote a post where you shared some of the uncertainties and

anxieties. It was a longer post. It started with how Vype coding will be never good as software experience 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. The way I sort of thinking 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, vibe 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. 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 vibe-coded mess. Yeah. LMs can significantly augment 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? 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. Ellen's 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 U.S. 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, Ellen's are still getting better. Maybe they're going to cause job losses in the future. Yeah. This is a novel 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. there seems to be 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 was a Java engineer, like Java specifically.

Like, don't care. 10 years of job experience required. And that's changed. Okay, then we'll open up new jobs for many, possibly far more money, software, inch 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, right? That's been true, yeah. The software jobs that LLMs open up will be lower paid and lower procedures in the heights of the 2008-22 tech era. And that's the thing that scares me the most, is that, as mentioned, I 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 proved systems correct. That's crazy. What other field can somebody just go like, what other engineering feel can something like, I want to be an engineer and just walks straight into it? What other field is going to send people to Budapest from the U.S. 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 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. Are we saying we're afraid that software and Drew might, become just like every other engineering job. Yes. Because that is the reality of 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. Yes, we have a huge amount of privilege and I don't want to lose that. And I mean, it would be nice if everybody else got the same things we are, but I don't want to equalize us by losing what makes software engineering so magical and precious. Yeah. So this is a worry.

Yeah, that's my fear. And number six? There will be still be high paid professional software engineering jobs, but they will be rare, more competitive. and less developer friendly. I'm afraid we're seeing some of this already. I wonder if this is inevitable. I also see it in some other industries, for example,

with investment banking, 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 hard to get into them. Yeah. I mean, I think most jobs do ossify over time. As like the standards are said and more people enter them,

sovereign engineer, I think for a longer period of time was able to, like get away from that. And then you close your prediction with these lines a year 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 limitification 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 curious way of ending this, to actually fit in the back wing.

If we start with automation comes for all of us, even as automators, and like, on one hand, I feel like I'm losing something really, 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 this nurse 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 in 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 going to, we're going to all find this out in the next 10 years, I guess. 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 had nothing to do with software saved up and started to just hack around.

And it democratized it. And I feel, this is the first time I'm also feeling. Like this other person in 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 trying to learn the hard parts of software engineering eventually. Did you read up Clay Shirky's essay situated software?

No. Basically what it is is that this person was talking about how they think like the most important, the vast majority of software should be made for like three people or like a 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. It's exciting. As closing, what are books, a few books that you could recommend that you have enjoyed or made an impact on you?

Who 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. 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 Levison's Engineering and Safer World. I believe that's actually free online. The second book is called Data and Reality by Bill Kent.

And this one is actually hard to find because it was republished in 2011, I think, 11, but the republisher changed the book. So the last good edition is the second edition, which can be found like in dark quarters the internet online is actually kind of hard, but it is basically by this famous database designer who worked on IBM databases, who was just asking like, what is data?

What does it mean for something to have identity? What does it mean for something to have oneness? If we 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. incredible book. It totally changed how I think about things. The last book is called Debugging, The Nine Simple Rules, by David Agens. 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 it 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 we want to talk about other books, I can keep going. This is great. Well, Hillo, this was very educational. And I found it fascinating. Thank you. Thank you. I really enjoyed this conversation, especially the demos where Hilo showed tools like TLA plus alloy or hypothesis and how they can catch blogs. 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 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 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 a 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 the waterfall. Plus, it was amusing to hear how source control is kind of an envy from other engineering feels that we, software engineers, have, but not many others do. Check out the show notes for related deep dives on distributed systems at TechDept 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.