Formal methods with Hillel Wayne

There's a popular theory going around that AI will finally make formal verification go mainstream because when machines write the code humans will need mathematical proof that is correct. Today I'm talking with one of the best people to respond to this. Hillelouin, a formal methods consultant. He saw TLA+, a popular formal specification language across the industry, wrote the book logic for programmers and will soon be joining antithesis. In today's conversation we discuss the crossover project.

Hillelou's research interviewing 15 plus traditional engineers to answer the question can software engineers also be considered real engineers? How AWS used TLA+, an overview of how Amazon found a rare bug inside of DynamoDB using this formal specification language. A deep dive into property-based testing and why this is a 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 what 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 a lightweight formal method can actually be helpful. This is where I need to mention our presenting sponsor, Intissisys.

Intissis verifies your system's correctness by running your whole system in hostess simulation and finding bugs. It does this by using an approach called deterministic simulation testing or DST, which ADW is a distinguished engineer, Mark Broker and Anchorage Desai have described as a lightweight formal methods. Setting aside Intissis 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 Intissis.

Intissisys is turbochargers testing by running your whole system under a aggressive fault injection. Imagine Intissis 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 Intissis, you can specify properties at the whole system level, and Intissis will actively try to disprove them. So you can be confident that if your system holds up in Intissisysys, it will hold up in production. There's good reason teams like Jane Street, Fly.io and the et cd community rely on Intissisys.

Hetsu, Intissis.com slash pragmatic to learn more. So, hello, welcome to the podcast. Thank you so much. I'm really excited to be here. It's so nice to have you here.

I was curious. You're very well known for formal methods for programming for logic for all of these topics, but how did you get into tech? So to start, I never really saw myself as a technical person. I 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 school or 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 the labs. That was the most one part to me. So I thought, well, if this is what I enjoy, I 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. I just went back to Chicago and then in the course of the next job I was working in, also in education technology, I found my current niche, which is formal verification, 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 read a lot of books on software and I read a lot of online articles about software. And one of the favorite things that software developers do is argue about whether to be engineering or not, right?

And there's the kind of people that say, well, we don't deserve as course engineers, we should not. They are so far above us, we shouldn't even like consider ourselves in the same space. And other people who are like, what we do is so special and so unique, engineering doesn't have anything on us. They can't hold a candle to what we do. You see books like software craftsmanship, which talk about how like, oh, engineering is really boring, slow, field and software is this incredibly creative, special, wonderful thing.

I was very early in camp one. I thought we were not engineers. We didn't deserve to call ourselves engineering anything like that. What I do for work is really carefully analyzing software systems and I thought, ah, this is real engineering. Everything else is not engineering.

Then I found this talk by Glen 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 to have to talk to people who did both engineering and software development and see what they say and they all agreed with him.

So I was wrong. We're engineers. Can we go a little bit? 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 the software, which when you think about it, when we say like, oh, software is like building a bridge, maybe isn't, but is it like designing a circuit is like figuring out a chemical flow.

Maybe those are much more closer to the kinds of engineering we do. I needed to know. I think in the end, I talked about 15 or 20 people in total across about six or seven different fields. 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 put it like this.

Everybody hates waterfall. No, but 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 to do before you iterate and the more expensive it is the more planning you to do. That's why, for example, when you're building a building where you can't like build it multiple times and see what happens, you have to do a lot of planning upfront. But even then you are looking for ways to iterate on the plan. You do things like build scale models, you software to simulate the building, you do like CAD models, et cetera.

And in other fields, like in, for example, electrical engineering, you have the ability to come up with the design and test it and then throw it to the fabric and get something back. So they'll 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 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 changes as they could, seeing how the rest of the system reacted to it, and of course, correcting based on that. Okay. So I guess we all hate water. All hate water.

Or the idea of waterfall. Yeah. What are some of the interesting differences that you came across? Either we're engineering as a head 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 different material, they have different constraints. Whilst true that everybody tries to iterate as fast as they can, often trying 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 overnight and get the results the next day. And that was fast. With us, we can basically press F11 and get the results, 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 as software engineers is that our work is a lot more consistent than other fields. The example I always do sometimes, because I'm going to 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 I said, it says, this resistor has a resistance that is within 20% of 100 ohms as long as you keep it between 20 and 50 degrees centigrade.

So they're basically saying that if they make a thousand of these, there's going to be a variance of 20% across all 1000 and the only way to know is to test that. And then if you run it for too long or you hit it up too much, it's going to change again. So if you're not consuming a CPU bug or anything like that, the same program, if it runs on your computer, or on your computer, exact same, sort of the same exact same, that's sorting algorithm. Does this also mean that we might not account for a lot of variability as much as other engineering disciplines do? I'd say so. The very short of view of this is kind of our own making, right?

We're basically saying, okay, we've got all these different system, all these different APIs versus other people. We have all these different chips, we've got all these different like, ports or sizes. But also, if you haven't touched like an iron spool, they're going to cause corrosion between the two of them. And also some of your spool are a little bit bigger than others and some are a little bit smaller than others, a little 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 the software in other engineering fields, is this also a thing where as an engineer, you will talk or know your customer or just not knowing them at all?

I think it depends, because different interests talk to different experiences. Some said that they felt that was 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, which makes software engineering a bit higher, better places 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 a craft conference, right? Most other fields of engineering or in fact any other field of human labor has two kinds of conferences. Academic conferences we talk about research and trade shows where vendors try to sell to companies. Software is kind of unique in having the third kind of the practitioner conference, where we are just meeting to get better at what we do.

We also are really the only kind to really focus heavily on open source and making our knowledge really available. For any language, you can probably find out how to 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 Uber or Airbnb. These are $100 billion companies. They will not particularly hide how they built that piece of software Uber publishes and that talks about their app that is used by all these people. How exactly they built it or approximately.

I wonder why this became unique and software and 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 both already. 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 leads to build things or using software to design circuits. I personally think that that similarity, basically that we are using the same materials and build ends, that makes it so much easier for us to talk about things like open source. Interesting. I like this thinking of materials used in each engineering and how our material is software itself. Of course, it's hard rendering and we know that it's a bit different.

Already there's a divide between hard rendering and software engineers and how much they share, how much we know about them and so on. I kind of wonder, I've got some friends that do 3D printing and it seems like, and I'm not looking at this, but it seems like they also have a very open space of sharing things freely. I wonder if that's the same because it's so easy to share and because the unit of value is the schematic there, if that 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, hand radios, which is not engineering, but there's a driving community where they share the setup, the things, they talk with each other, small electronics might be.

But ultimately software started in the 70s when it was affordable, anyone could buy a computer, maybe the internet. I'm also just speculating. Definitely something worth doing a follow-up project on, right? You've already spent a bunch of time on it. There's already too many radicals in my life.

One more thing that you brought up is version control. The fact that in software we just take it for granted, we have version control everywhere, and you said that it's super unique across most of engineering. I interviewed 20 people on this. I think I'll totally mention version control as I think they wish they had in their old field. Wow.

Now, because they do have things like change management in other fields, but I think version control as we have it is so much more sophisticated than anything they have. It's comparing 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 charging and engineering cultures? What could we learn from them? What are some kind of inspiration that might be useful here there?

This is a harder question because while everybody talks to mention 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 that kind of cleaned out is that one while we are a lot better at iterating than other fields, we're worse at the planning part. We still need to do some kind of planning before we iterate, and we just aren't as good as those other fields, in part because we can get away with not doing it as much, but we could get some sort of fusion with it 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.

That's a bit loosey-goosey, but the example I keep coming back to is that one of the engineers that talked about two-fear books, the design of every-the-fear books, which he recommends every engineer read, and the snap-it handbook. Are you looking around here to see if there's one? I can just show it. You know how remote they have the little clicky thing in the back that you used to hold the battery in? No.

That's a snap-it. The physical device that clicks into another device to keep them confused. This was a 500-page book all about snap-its. They're engineering, appropriate shapes, materials, etc. That kind of compiling of information about materials is something other fields do that we don't do.

An analogy that I would think of as software would be something like a 500-page book on how to version an API. We could all use that. Yes, we could. We could go to 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 this project and writing about anything about it has been really weird from the camp, but we are definitely not too. We probably are. I do want to caveat that I wrote this for LM's Worthy thing.

This has probably changed our field as we know it. It's probably also changed with other branches. I don't know how. That could have changed the calculation to do spaces. As of now, I think excluding LM's and how they're changing things, what we do now is very similar to what those people in other fields did.

According to my interviews. It's such a good project. It's still a very good read. I'll also link it as shown below. I do recommend going into it.

Let's talk about formal methods. How did you get exposed to them? For those of us who are not deep into it, what are they? I'm going to give you a function in Macs, which is given a list, return the largest number. What will be a test you write for that?

I write a test that. I do a list of two items. It returns the largest one that I know. I give a very long list. I try to stress test it.

I give a list where I give similar numbers. I try to come up with some edge cases. I'll probably write five tests. Try to think about integer overflows potentially. Try some tricky.

Maybe I'll take it. Maybe eight if I'm feeling super ambitious. Then I'm done. Okay. We take one of those tests.

How do you know the right answer is supposed to be? I know which number is bigger. I have this ingrained knowledge. It feels very basic knowledge. I don't even have to explain.

You have some ingrained knowledge. You can look at the max of two and three. That's interesting. There's some implicit mechanism in your brain that can see that. I know what the function is supposed to do.

Step one of what you're asking is can we take that implicit knowledge and make it explicit? Can we figure out what a function is supposed to be doing and write that down in a way that can be shown to anybody? I would say 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 we can formally say what the maximum list is. That's part one.

I know what this is doing and how I explain what this is doing in a way that is clear and unambiguous. Step two is asking every single test you've written is basically some facet of it is an element of the list and it is the number that lists such that ever other than a list is smart in it. Now that we have that, what's the best way to show that our function satisfies that specification? Pest there one way. Those are basically taking individual values and showing how those are important 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. Every time we call it that's true. So basically the coming up with the properties of the thing, what it actually is a specification of it. And then showing the function matches that specification is the verification.

What I'm asking 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 improve again from university. I still remember that the math 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 typically start from a complicated equation and you keep changing it. And in the end you shape it in a way that it's now trivial or you transform those rules. Is this what format is also just 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 use a calculator? I now use a calculator. If it's easy enough, I use my bring as a calculator otherwise I just punch it into a calculator. Yeah.

So I'm going to do a lot of methods that map transformation. While you can do it by hand with like what's called a theorem prover, often in industry that is being done for the most part with tools that basically automate huge parts of this process. So you don't have to do every single transformation yourself. You can for example say, okay, we have these things are at the beginning. I want this to be true at the end.

And can you figure this out? And I'll be like, either yes, I can prove these things match or knowing a little bit more help. And you say, okay, at this point, I mean, also, you know, this is true. I go, okay, I can verify that's true. And it helps me get to the end.

I just keep doing that until you actually have enough that computer can do the proof for you. Yeah. So I mean, this, I mean, this sounds logical. I think it's easy to follow in practice. What techniques, technologies, tools, does the industry use a tech industry use to actually prove that, you know, some, some stuff 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, 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 control edge cases been there done that where you miss and I don't, I didn't think that I didn't do a formal proof. I thought, like, well, I miss a test case.

That's on me. Sorry. Let me put on that test case. I go and take 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, each file I list how long the lines are. Count the lines. I cannot tell.

Okay. Are we talking about ASCII lines or UTF at new lines? What happens when the files, you know, the file permissions to read it? Should you basically ignore it or should you say, Hey, my proof, my, um, function like you're wrong? You're not trying to find it.

What are the files is a shortcut to another file? What if it's actually directory? You're now simulating binary. You're now simulating real world. It's a very interesting domain problems.

You have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get pregnant in a percent of the time is probably good enough to use in almost all cases. And if you want something that works a hundred percent of the cases, you've got to figure out, Okay. What else is more of using everything? Yeah.

And it's not done. And basically it would just not be practical. It would be for the 99% of people will be wasting your time. It's like premature optimization, right? Yeah.

Especially when, as you say, writing 10 tests might get you most of what you need. What are practical technologies that you have seen using some part of the industry that, even though they will, I'm assuming, will be somewhat heavyweight because it sounds like a pretty heavy weight, it might be the return, the return of investment of using this heavyweight stuff is worth it. That seems in history, 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 what the first time experience nuclear power plants do not care about this stuff. They're actually just fine with, with, with their own 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 it for methods. And this is usually things that are like small parts of databases or like cryptographic primitives. I believe that the HTTPS that can firebox is verified as far as I call product 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 the kernel like memory allocation or something like that? Yeah.

Parts of our, as operation kernel reduces for this. A couple of things I believe Microsoft used some pro application of parts of their piece of kernel for the driver loading. Famously there is an operating system called SCL4 that has been n to n verified in a language called Isabel. It's a microkernel. It's very small.

It's mostly used for automotive and military applications, but it is a fully verified operating system. That means that it's matching specification. So it might do the wrong thing, but other things that you specified that 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 system, which is a nightmare as we discussed, we create a simplified version system and verify that.

Then the actual system might still have bugs, but we can iron out the issues in the abstraction 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 a database or a distributed system?

In my work, it's mostly been databases and distributed systems for technology companies, but it has some other interesting gigs. I've had one gig that was involving firmware of a device kernel. And honestly, one of the coolest projects I've worked on was verifying the transponders of a train system to make sure they wouldn't cause problems to transglue up 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 warm-borne 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. So, the fourth 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 on 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 FIND-RATE authorization, builds 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 Turbo Puffer. But this time, I don't want to talk about how they are fast, cheap, and extremely scalable search engine built on their storage. Instead, I'd like to talk about their team. I'm the co-founder and CEO on stage at AI and Jears 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 facing their bugs. The team gets together for annual summits at least twice a year, and campfires, formed several times a month, anytime several of our employees gather in the same city.

Simon describes your engine culture as hardcore and whimsical. They focus on solving difficult problems, but also try to have fun. A good example is the pragmatic engine 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 on the company has 10-15 years of experience. For startup, they are an unusually seasoned team. Finally, I really appreciate how pragmatic their engine philosophy is. Simon and his team strongly believe in how simplicity scales, and this is a reason that object storage just turbopuffers only depend on the same. The team do seemingly silly things like build their job queue in a single file on object storage because they understand the core primitives and 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 Hello. Can we see a demo? I've got a couple of languages with me. The kinds that I've worked in.

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 LaTeX, the typesetting language. That's all the PDFs behind the scenes. Yeah, PDFs behind the scenes. 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 asks about the name. We don't need to know the name. Just know what is TLA plus.

What it does is it basically represents the state machine of the system. Every possible state it can be in, and every possible state it can transition to. Then we can use a brute force model checking where we basically find every initial state and every state that can evolve from those and check out their properties. TLA plus is unique in some ways because it has certain properties like checking, lightness 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 the training platform. Each person on the platform has a set of items. And they want to train 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're moving from the set of offers and the owner transfers. If you reject the offer, it's just removed from the set. Then we define what can happen next. A next state, as in one of the ways this isn't going to 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 an 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 then 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?

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 Leslie Napper made this in 1990, like four, he was thinking of it mostly, he was a mathematician, right? So he was using his mathematical background and running how mathematician would write some symbols in the 30 years since that point. Price has been 30 years since 1994 already.

A lot of languages have been developed in part from the lessons of learn of TLA+, and that making a little bit more uplink 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 rock. The reason a lot of us use TLA+, was because the first really high profile demonstration of this kind of work and practice was Amazon paper, the use of problem as Amazon Web Services in 2014, and they use TLA+, so that's what a lot of us 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 missed? Well, if we had to think through ourselves, we wouldn't be using Snassy Syntax, would we? Nope. So what I've done is I've also written a quick configuration file saying, take a specification, take these three people, Alice Bob, Carol, and have them trade around a stick. And then I tell it, make sure this property that the change in variant always holds.

When we sold it now, I just have to run this. I'm also having it out with the state space for you so you can see what that looks like. And it just puts out the error for us. It says the property's been violated. It took 53 states to find it.

And the way it works is, it's not 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 is, graph is not dot is when we're saying. So this is just a preview of the state space is generating.

So you can see it's basically generating every possible state you can find. This isn't the whole state space, usually because the state is in the state space, it's in the state space, like 100 million states, like in the state space. Usually these aren't that useful. It's mostly a thing that we have that we use for demos. So the error is as follows.

Alice, Bob and Carol are on the system, and Alice owns the stick. Alice makes an offer to Bob. Bob is away. Alice gets tired of waiting for Bob to come back to make the offer because she wants to order for 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. Click the button. And now the stick becomes Bob's.

But it's not transferred from Alice to Bob, it's transferred from Carol to Bob. So the change in 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 would 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, somebody's trying to say, oh, 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, OK, I'm going to create two new states. Then from this top one of offer Bob, there's three things that can happen. We can have Bob accept, Bob reject.

Or, and this is where the concurrency comes in, we can do offer Carol, right? Yep. I see. Yeah. Mm-hmm.

I see where this is coming. And then when you continue, we will hit the bug. Yeah. The change in variant will be invalid. That's whatever step that is run out.

Right. And that's actually where a lot of this, like, becomes useful for distributed systems, because often it'll be like, OK, process one can do one of six things, process two can do one of six things, process three can do one of six things, and when you do this 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, then process two takes step two and three, etc. And being able to 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 CLA plus is.

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 onboarded, 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 problem at Amazon Web Services, and they talked about how a couple of people in the company were interested in it and learned TLA plus another language called plus gal, 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 buck contained 35 high level steps, which if I understand that correctly, it would have been very hard for a human to persevere, or it would have been to be really determined and precise. I did not work on that project.

Of course, I don't know what the details are. I can speculate that the reason it found a 35 step bug was because it's based on 100 million states wide. So there were like plenty of say like 70 or 80 stepchains that were totally safe, and it just happened this 135 stepchain was invalid. Through working with a lot of customers and teams that have used formal verifications with distributed steps, 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 think of one thing that besides just general race conditions and locks, this is the one that is always in your point, how much like, yes, it's another time to a lot of time to check the time to use bug.

And time to check time to use is a situation where you are checking to see if something is like valid to be done validly, and then you see that it's correct, and then a little bit later, you do it. Sometimes a little bit later is like a day later, sometimes it's a microsecond later, but it's any case where it is possible 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 money from a bank account, meaning another bank account. And this is not how banks work, I know, they use a different kind of ledger, but just as a demonstrated example, you check, oh, do they have $10 in their account? Yes, we did talk $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, some of these ones have been grabbed $10 away, and now there's $0 in, deduct those $10 in $10, that's the time to check the time to use kind of bug. They have been everywhere. Yeah, and it's very interesting because I, when you're building New Jersey, New Jersey, I realized or I learned that the problem of having a message delivered in the distributed system exactly once is a very difficult one, because typically that's what you need when you want to do one charge, you want to charge a customer's card exactly once, because if you send multiple messages just in case one of them gets lost, you now have double charges.

And turns out it's a complicated problem. It's a lot easier to do at least once delivery than exactly once delivery, but of course you need exactly at least once delivery to build on to create exactly once delivery. Yeah, I wonder if this is like a lot of like on businesses, they just charge you extra than refund you some amount. That seems like easy to do from engineering perspective. As well, it's also from a risk perspective, you eliminate a lot of edge cases by authorizing upfront on the credit card, you have a credit limit, and if you would authorize exactly how much you think you need right now, but you need a bit more, you might get into that edge case where later you have trouble authorizing it. This is why often hotels don't want to deal with this.

So they just authorize a larger chunk and they know because it's a larger amount for hotels, otherwise they might 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. Some of this might happen because it's easier to do some stuff. Yeah, makes sense. I honestly thought hotels are that because they're kind of convincing off to like break stuff, because like, hey, if you know that you're definitely losing $100 to 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 cycle 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 read about concurrency 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 concurrency system. I remember whiteboarding just boxes and imperative this flow chart sort of whiteboarding. So this is something that I've wondered a lot, 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 that.

I mean, when you cross the street, aren't you working with a concurrency system? You're just, there's cars everywhere. They're going to die if you don't model concurrency system in your head. And there's actually this really cool paper I found called the Common System Computing, where some people were trying to figure out how people have a current system. When talking with high school and college students, they changed the concurrency problem from like, hey, we've got these threads doing some operation to like, hey, we've got these clerks in 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 synchroncy issues. I think a large part of the problem with why it's hard for us is because we don't get a lot of practice. Usually when you have a race condition system, you find out months later, and then you try effects and you find out weeks later after that, if the fix actually worked. Whereas with the TLA plus, like I write my model system and then I click a button and it tells me, hey, race condition. And then you fix it and says like, hey, time out bug. And then you fix it again,

it says, hey, TOCTOU 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. I think about crossing the street system 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 no 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 different systems. It gives them actual practice and seeing how the systems can go wrong so much faster.

I wonder if it's a little bit like refactoring and also migrations. So refactoring the code base when you are starting out as a developer and you need to do a refactoring by hand, let's just change a function name and then you need to go and change all the references of a function. And the first time you do it, you change it out a few places and then you forget about the rest. And either it's a compilation issue or dynamic language. It's a problem. But then you get good at

it once you practice with migrations. Most engineers that I've seen are terrible migrations because you need to make a plan, you need to check, you can do shadowing, reverse shadowing, all that funk. And then there are a few engineers who have done three or four or five and then you can just do it. I'm just thinking that when it comes to race conditions, most of us, I was exposed to race conditions by, oh, we did a double charge. That one, and then we found the race condition.

But I never did a second one. So I will not be good at finding race conditions. I'm not even going to think about them. I think that's right on the money. It sounds like you coming into teams or to these clients, you at least give them some practice, the very least of how to think about this category of errors, even assuming that the taking out even the tooling itself. I think it was also like more subtle things that you

started to pick up from these tools, but I think that's the most visceral one. The visceral hatred of a race condition that gets a physical presence in the algorithm. You've been doing this for very long. For you writing TLA plus is 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 has a declarative language. I've done a lot of stuff in logic programming languages and I've done some stuff in a way like a language but some of you see this as 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

hackling which is Python these days, just because that's one of the first things I use and I just know very well. I think at very least the format makes you much more willing to reach for mathematical solutions or heavy solutions than 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 discussion back and forth. Can we talk about the

core of the argument? How might these programs are a very interesting question? First of all, there's math that we all find useful. We forget that it's actually math. Counting is math. Knowing

whether one thing is bigger than another number is math. 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 and like you need that math. Then there's a lot of math that is useful for very specific specialist jobs. I've talked about some SREs who need calculus but I think most programmers don't make 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 what math has in their fields versus just going on every single field when they see them. You've got to know what's available to know what's 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 computer science from Algebra to computational theories, even formal methods. At university I learned a bunch 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 useful. For example, matrix transformation, I learned 3D graphics and how you compute all the points based on 3D matrix transformations and then helping understand when GPUs were becoming so popular with AI, why? This is because they're also very good at matrix transformations which happens to be pretty similar. So every now and then I feel that 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. 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 a 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 and you discontinuous 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 we most often use is discrete math. Things like combinatorics, basically which is the math accounting 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 in software engineering is because the math they do need is not the math they've been exposed to. Interesting because the math that I did use more was combinatorics and of course like maybe these days those entries are going out of style but here's the problem building 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 and space and time is and you can do trade-offs and you can once two people know the same thing you can have discussions about these things. And it's one that is 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 understanding a big old notation got a lot better one-centers with the math in the next thing is usually explained in terms of like oh this function scales at a 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 that's taught and stuff but like etc I think even like the technical aspects math does help a lot in understanding those. And with the CLA plus specifically what cases have you seen in the industry, CLA plus being a good bit for certain problems and in what cases would you never consider it? I think it becomes a CLA plus and most not all but most role methods they shine the most in highly computational domains where most of the problems are highly technical and not like business embedded.

And what I mean by that is that like how you 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 springs don't go over time is very business right? It deals with like very human behaviors. I've had to have a pipeline model that and we got some use of it but it was very hard. So that's why a lot of my clients end up being things like database vendors or like cloud computing people who are or like harder people who are working in a space that's like very quantum 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. CLA plus in particular tends to be good at discrete distributed systems where the main challenges are mess with concurrency and possibilities of interleaving like behaviors. It doesn't do floating point it doesn't do decimals it doesn't do as well when you're trying to figure out probabilistic things. Oh that's another thing I guess I should be saying is that like where the kinds of errors you care about are ones where like if it is possible 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. It also depends on how much time you spend planning. Like if you don't need to spend that much time planning this is gonna waste your time. I do want to add that this like if you can iterate your way through a solution and the bugs aren't gonna be that costly then you might not need this tool.

I think it's really important as like a person who talks about a really exotic tool to like constantly emphasize like no I'm not trying to convince you to like use something that's not a good choice for you. I think a lot of the reason people are skeptical of these is because they've been burned by things like case and UML and all these other miracle solutions that were forced on them by people who wanted them to use it no matter what and I think it's really important to always say like if this is the right tool for you I'm 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 form of this lineage just like there's many different kinds of programming languages there's many languages of our 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 a people who it's reasonable by and resources may or may not have a parent resource. L1 means L1 means less than equal to one resource. There are no cycles so no resource can have itself as a parent or its parent as a parent. You can read access to a resource if the resource indicates you can read that resource or if it's parent indicates you can read that resource.

And we have a property that if you can read a resource you can read its children. This isn't has 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 is it will it might have to do with something that we talked earlier about 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 the just for context. Alloy did not have any temporal reasoning

overstate up until about four years ago. So this is one example I used from before that of basically how you can analyze and find bugs and static configurations and Alloy that often means finding bugs and data structures or data models and domain models actually. So there's actually some interesting there's some interesting 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 a counter example. And this one is specifically that I can

generate like on visualizations. So basically here's the problem. We have a user who can read a parent resource. The parent has a child because of how we defined can access we can read his parents so we can read the child. The child has a grandchild. We cannot read the grandchild. So because we are not

we are not assigned to the readable by for the child only 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 one. Individualizes for us. Yes which is quite nice. 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 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 from what they don't really tell you how you choose how you want to fix it. Like one thing I could do is I could say okay I'm going to say that this is a transitive look up too that we transitively close over all parents and 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 a transitive

query and our database and it's like no that's going to crash the database you can't do that. They're going to find different things. So this is a beautiful method I said it gives you the opportunity of how you will implement fixes changes and then you're going to be running again and see what difference it made. Exactly. Now one quick fun fact I love just fun facts about stuff.

You see how this has solver sat for J so have you heard of sat SAT problems? No. Okay is there some variable that makes a statement p true? If I can make p true or false is a way I can make that true but let's see p is a boolean and I have a statement p can you assign some value of true or false to p to make that true? Typically you can assign true and it will be true. That's even

satisfiable by setting p to true. What about p and not q? Also satisfiable by giving true to p and false to q. Right now what about p and q and not p? That's not that's not that's not unsyssifiable because no matter what boolean you do true and false will always be true. Lovely.

What you've just done is a boolean satisfiable problem taking some sort of statement of a ton of boolean variables in this case to and found some either found some assignment that makes it true or said that it can't be made true. Now boolean satisfiability is what we call empty complete and what that means in theory is that there's no such thing as a perfectly vision algorithm that solves all problems in practice that means that we can solve them really fast. So often what makes all interesting is that only kla plus which once we've reversed alloy can be converted into a satisfiability problem. I'll open this up and it is able to turn that model into a boolean probability saying not x21 and x96 and x15 or not x72 etc and because of that most alloy models can be checked in like a few milliseconds or a second. Whereas often for like a large tla plus model you have to basically turn it overnight to go through all hundred million states. Can we talk about smarter tools

on the like as a table of someone looking into form of verification? Happily. So I don't have my PC right now but I can talk about a few of them. So a couple of the ones that have been success with tla plus is on the p language which was invented by I think a person at Microsoft Research was then coached by Amazon as a way of making a language that was more accessible than tla plus among other things. So it basically looks like a set of state machines interacting machines that send message 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 were making different kind of object with tla plus and then realize they can make an entire language that was easier for people to pick up. They've got a lot of interest in the banking and I believe cryptocurrency space smart contracts. So another one that I've used which is a lot more niche but quite interesting is called prism and prism is a probabilistic model checker. 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 work for actually translate languages into prism if you're interested in it I've basically been doing this like I'm having a Jewish game in the game. Okay it's a game that you play on conica where you spin a little top and you get money

and I do not like the game and I have written a two-part series using prism to show how this game is not fun by analyzing as a mathematical thing. Those are things from the ones that are like very popular but there's also um I mean I can just keep listening there's like event B which is like venues I believe famously in part of the paris metro system. There's like MCRL2 which I think is comes from a Dutch university, Kmera X which is most used for like robotic control systems I think that's mostly academic. There's like new SMB which I think NASA's used for a bunch of stuff. I can keep going then of course there's all the this course is only for specifying like abstract models of systems. If you want to talk about verifying code then you've got things like

Daphne which is basically something that compiles to like .NET and lets you basically write proofable code you've got gml for Java check for like model checking Java code you've got like Frimacy for like checking C you've got Ada Spark you've got like any of the other improvers like um Rock and Lean and it's not like you 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 the Tarthi with max right? Maximal list. We can find like the specification of maxes it is in the list and for all elements of the list it is the largest element of the 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 is for terms of max of the list one of the terms of max of first three and then one of the terms of max of 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 or equal to. So this basically is all like our

formal verification spec our formal specifications 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 property testing is well that's very very hard and as we talked about very difficult doing practice can we instead generate a thousand random lists and try all those. I have it set that way it basically has the invalid max max of first three. We should be getting errors where it should catch some errors. Let me just run the command line that's faster.

Pytest test max. This is an old machine I built for conferences because it's easy to 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 0. This is because I said our bad max only looked at the first three values so I found the max was 0 but here are the actual list was 1. I broke down to two sub specs for part of the book where we have testing that max is the largest element and all sets 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 with this demo is show that it actually does not start with the largest list it actually starts with a much smaller with a print max and I do it like this I think it tries a lot of edge cases first. So it's basically trying huge list is trying like tiny list is trying like empty list etc 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 present in a way that is like car pencil for the average human because I think that it found the original bug with this list and I do not think that we're going to find a note problem is that's basically property based testing in a nutshell and as you can see it is less than a row 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 formats 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 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 on maybe formal verification or property based testing or some of these things that would be more useful. Do you think this will happen or because I see a lot of people talking about this I don't really see anyone doing much about it. I'm definitely seeing more business from people in my client as a client as a client as a client as a client is 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 key road like the Amazon spectrum development platform specifically advertising 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 kind of like exciting because as you saw like a lot of

the challenge of writing is like a lot of it is like rocking your head around like very very technical syntax and like semantics that said I've been doing a lot of experience this myself and I think the one thing AI is extremely bad at as of March I know that quad just released a new like quad 4.8 so maybe this is all the window changes every month it is a very bad at coming with properties it is very bad at that. What does coming with properties mean is it writing the actual form of application part? Yes like if you give it properties and like a spec it can tell you like hey we're gonna fix this back make these properties pass that's fine but you can basically tell it here's a spec also come with 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 property is about how like a system can evolve over a long period of time it just it's hard to pronounce it's just not good at that yet and often I find that I have to tell them like it's doing a good job at generating the actual design but 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 there's a blog post that I'll also link in the show notes from a year ago in March 2025

titled the coming revolution distributed systems and this was an engineer working on this person wrote how AI autonomously proves precise TLA plus specifications from as your storage production source code and it uncovered a subtle race condition that had debated traditional code reviews and then this person's 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 Changguang did come up with a tool called lampport agent where they demonstrated using this to specify parts of crack I think it's called RDC's crack I'm going to link both those in the thing here's my response I was writing about this and then the thing that they did he seemed to have 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 like already knows how to do this on his own without the LMS that means yeah he knows how to like get the results out of it as a general thing we've seen like to get the results or you know like get the results without it it just helps to get the results faster and also he wanted to see something to be able to create

the complicated properties for until I 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 cheated maybe that was like fine but we do see this a lot where when you're an expert in a domain and made that with software engineering or like back end or mobile AI works better for you then there's also this one interesting um person Claudia Colle did write it right up because she just did about a multi-year project and using frolmethes edam the big Chinese cloud provider where she talks about how in between her like working on this paper and like the time she got published she got really sophisticated and how long it took people to write frolmethes 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 useful from like all methods but it seems people with the most success right now are specifiers for using it to amplify their ability to specify and we haven't yet really seen I mean people post acronyms all the time like people who like they had a AI write the whole spec for them but those tend to not be very good specs and what's your take on again I've heard some voices say that AI might make form of verification go mainstream off based on this but outside of the do you see any movement outside of the this niche of people who already know how to do form of revocation I think it's making

more popular I don't know if it'll make it go mainstream but it's definitely making it a lot more popular it's bringing it from maybe like 0.1% to 0.3% which is huge there's also this uh this thinking that I've actually in in June 2025 in your news article you said that AI is a specification force multiplier and now of course we see that LMS are bad at dividing specifications what changed between that time where you saw that they were like a year ago they were pretty decent at doing it or they had science and now we have the proof they're not as good so what I wrote that was really good I was fixing syntax errors which is really big because um that's often trips people up it's good at understanding error traces which is huge because we'll take like a 35-some error trace and turn into like two paragraphs of English text major improvement could have boilerplate like mass changes like a bunch of small things like updating like boilerplate and it's okay at writing properties from a very precise description it's bad at fixing specs and it's a real bad at providing properties for spec I was consistent you know so I think I called it early back then that it like is really bad it's gonna translate in properties from English by English English into a spec but it's bad at cutting with properties on its own everything back was trivial understanding a couple of implementation

details so I think what I'm gonna 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 was really bad at this one thing that it continues to be continued to be bad 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 LMs 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 the ayes doing something wrong right and if you don't know the basics you can't really do that very well in your book logical programmers you argue that formal logic is probably one of the most useful parts for for day-to-day engineering why why is this first one on it you read my book or at least the early drafts I mean the official answer is because logic teaches us to work with like bullying and statements what we learn in elementary school how to work with numbers right essentially there's not a whole address between knowing that one plus one is two and true and true is true it's still the manipulation of values and it happens that booleans are so important to software engineering that having some formal grounding in that is very handy especially when we are not

taught that in school for the most part the other answer is that I've just I'm learning logic and getting better logic and teaching logic a lot as part of teaching tla plus I just find more and more applications where I'm like oh because of logic I can do this one thing and I find it people who don't have that background struggle to do that one thing I guess I'm saying it empirically logic keeps coming up as a useful format 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 at the 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 so just do some experiments that are cheap to do I'm going to just completely go 90 degrees here and I'm recommending this book by Nancy Levison engineering a safer world she was an aeronautics engineer who investigated things like etheric 25 radiation case and like the columbia disaster and she was really fascinated in how like systems 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 that I recommend is checking out that book looking ahead for 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 vite coding will be never going to suffer engineering 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 to think about is that the next five years keep being rewritten every few months right yeah so I wrote the following can all be true one by code 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 that I'm not an expert in like a game and it's an absolute just by coded mess yeah lms can significantly augment a significant professional software engineer's ability to quickly write high quality software I think also true I mean even if you don't have it running a single line of code just be able to be like okay what's this bug or like hey what why we're looking to solve this problem and we're 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 they're 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 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 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 just looking better maybe they're gonna cause job losses in the future yeah this is a no question the data that we had in the pragmatic engineer it did show that we are seeing overall more software engineering openings in the US and Germany and France they're declining a little bit at the same time and there seems to be a big shift on who is being hired and the scale 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 and engineering hiring while 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 job engineer like job specifically like don't care 10 years of job experience required and that's changed okay then

we'll have other jobs for any possibly farm and many software and 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 going to hire one developer right that's been true yeah the software jobs at lm's open up will be lower paid a lot of season the highest at 2022 and that's the thing that scares me the most is that as mentioned I decided to leave a field and just become a techy and I was able to do that and I was able to get a well paying job that led to me to now full time mathematically prove systems correct that's crazy what other fields somebody's going like what other engineering folks like I want to be an engineer just walks right into it what other field is going to send people to Budapest from the US to give a talk for 45 minutes like it is really precious and magical what we have here and I'm afraid of losing that I'm afraid of a place where it just becomes like any other like white colored 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 engineering might become just like every other engineering job yeah 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 compare it 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'd be nice every else about the same things we

are but I don't want to like equalize us by losing what makes software engineering so magical and precious yeah so this is a worry yeah that's my that's my here and the number six there'll be still be high paid professional software engineering jobs that they'll be rare more competitive and more unless you're a little bit 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 it used to be many of them very highly paid highly respected they're now fewer of them so highly paid highly respected it's hard to get into them yeah I mean I think I think most jobs do us apply over time like as like the centers are said and more people enter them um software engineering 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 predicted in the next 10 years software development will survive but it will become like any other white copper professional work no more two hundred thousand dollar salaries a notification of credible employee bargaining power I feel sad that we'll lose something so magical but I guess it can do less forever automation comes for all of us even us automators here's the crazy way of ending this actually this is actually going to be started with automation comes for all of us and like I want to have to like it was something really special on the other hand

a doctor friend of mine came to me like a few months back and was like hey we managed to like create a new shift scheduling platform for like our hospital like to trade shifts that really save us a lot of time and like made all this nurse and doctor so much happier and I was able to just buy them 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 like 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 coach he job or his job like I don't know and it's gonna we're gonna all find this out in the next ten years I guess. Brady was told me that this time reminds him of the time in the 19th late 1960s in our 1970s where people 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 at the gym told me that they're vibing something together it feels it's opening up the field and if anything a lot more people are realizing oh software is cool I can do it and now they're trying to learn the hard part of software engineering eventually.

The derivative of Clay Sharky is a 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 like happen if one of those people in that family that community that school was like really really into computers but now it's possible for everybody to have situated software and that again is gonna change the world in some strange and some terrifying and 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. Oh boy let's just leave this just for this and to just software books okay because otherwise we're gonna be here for like a month. So there's three books that I really love and software that I think of as like the books that influenced me so much. The first one I think I mentioned to be was on Nancy Levison's engineering safer world. I believe that's actually free online.

The second book is called Data in Reality by Bill Kent and this was actually hard to find because it was republished in 2011 but the republisher changed the book. So the last edition is the second edition which can be found like in Dark Quarter's Internet Online is actually kind of hard but like it is basically by this like famous database designer who like worked on IBM databases who was just asking what is data? What does it mean for something to have a data? What does it mean for something to have one? So we talk about a book is that the book, the physical copy, is that the series, is that an edition and it's just an entire book about these questions about what data is and how we need to represent it. The answer by saying that data isn't reality, it is our view of reality for our useful

purpose. Incredible book. It totally changed how we think about things. The last book is called Debugging the Nine Simple Rules by David Aigens and it's literally just like a book of war stories about debugging and like basic principles but this is the book I get to every junior engineer because I think nobody ever really talks about debugging as a discipline outside of like basic risks and it's like just something that's trying to do that and having something is better than nothing in this category. So really good book and I think it's like $10 for a used copy so like anybody can just get one. It's great. Those I think are the three most useful books for software

engineers. If you want to talk about other books I can keep going but this is great. Well, hello, this was very educational and I found it fascinating. Thank you. Thank you. I really enjoyed this

conversation especially the demos where Hello Shull tools like TLA plus alloy or hypothesis and how they get catch bugs by the end of the conversation. I'm starting to understand more why it's not likely that formal verification will go mainstream even with AI. I mean these tools feel very rigid for the real world for specific parts of a system that you can model mathematically like state spaces. Sure they can work but for everyday programs it just feels like it will be a bit pointless to create TLA plus specifications. One thing that I was also thinking about is how Hill talks 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 expert in this. I also find it fascinating how other engineering fields have similar eggs 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 a music to hear how source control is kind of an envy from other engineering fields that we software engineers have but not any others do. Check out the show list for related deep facts on distributed systems and tech depth that go into more detail into the topics they have talked about today and if you go enjoy this podcast please do subscribe on your favorite podcast platform and on YouTube. Special thank you if you also leave a rating on the show.

Thanks and see you in the next one.