Formal Methods in the Age of AI: Hillel Wayne on Engineering, TLA+, and What Machines Still Can't Specify
The Pragmatic Engineer
A popular theory holds that AI will finally push formal verification into the mainstream: if machines write most of the code, humans will need mathematical proof that it is correct. In this episode of the Pragmatic Engineer podcast, the host puts that idea to Hillel Wayne, a formal methods consultant who has taught TLA+ across the industry and wrote the book Logic for Programmers. The conversation covers Wayne's research on whether software engineers are "real" engineers, what formal methods are and why they aren't used everywhere, live demos of TLA+, Alloy, and property-based testing, and how AI is changing specification work. Wayne's position is that AI is making formal methods more popular, but it remains poor at the hardest part of the work. That part is deciding what a system is supposed to do.
From Physics to Formal Methods
Wayne did not originally see themself as a technical person. Their father was a programmer and taught them some Visual Basic, but the dream was physics and math. After about three years of studying physics in college, Wayne realized they liked the idea of physics more than doing it, and could not picture doing it for 50 years. The part they did enjoy was programming in the labs. So after college Wayne moved to San Francisco and became a Ruby on Rails developer in education technology. They later moved to Chicago, and during another edtech job fell into the niche they still work in: formal verification and formal methods.
The Crossover Project: Are Software Engineers Engineers?
The host first came across Wayne's writing through the Crossover Project, which asked whether software engineers are actually engineers. Wayne explains the motivation. Software developers love to argue about this, and they split into two camps. One says we don't deserve the title because traditional engineers are far above us. The other says software is so special and creative that engineering has nothing on it. Books like Software Craftsmanship take the second view and paint engineering as a boring, slow field.
Wayne started firmly in the first camp. Their own work involves careful analysis of software systems, and they considered that the only real engineering in software. Then they saw a talk by Glenn Vanderburg, who had read engineering books and concluded that engineering looked a lot like software development. Wayne found this unconvincing and wanted something more rigorous, so they decided to interview people who had worked in both a traditional engineering field and software. Those people agreed with Vanderburg. "So, I was wrong. We're engineers," Wayne says.
The project grew larger than expected. Wayne wanted as comprehensive a view as possible, because engineering is not just bridges. It includes circuit design, chemical processes, and industrial engineering, which covers factory layouts and how labor is organized. Software might not be like building a bridge, Wayne reasoned, but it might be much closer to designing a circuit or a chemical flow. In the end they spoke to roughly 15 to 20 people across six or seven fields.
Everybody Hates Waterfall: Iteration Versus the Cost of Mistakes
Asked for the main similarity, Wayne summarizes: "Everybody hates waterfall." In Wayne's account, the core tension of engineering is between how expensive a mistake is and how quickly you can iterate. The faster you can iterate, the less planning you need up front. The more expensive a mistake is, the more planning you need. When constructing a building, you can't build it several times and see what happens, so you plan heavily. Even then engineers look for ways to iterate on the plan, using scale models, simulation software, and CAD models. Electrical engineers can design, test, send a design to the fab, and get something back, so they iterate much more than civil engineers.
The host adds that "smoke test" reportedly comes from electrical engineering: you hook up a test circuit, and if it smokes, it's bad. Wayne hadn't looked into that but found it believable.
One of Wayne's first interviewees was a mining engineer who designed deep underground mines so they stayed stable and didn't leak toxic chemicals. The first thing he said was that mining had its Agile revolution in 1960. Wayne believes it was called the Viennese tunneling method. It was a way to iterate quickly through tunneling in rock: make changes as fast as possible, see how the rest of the system reacts, and correct.
Where Software Is Ahead: Speed, Consistency, Openness, Version Control
Wayne distinguishes differences in practice from differences in the "material" each field works with. Everyone tries to iterate fast, often by turning to software, but software is the best at it. Chemical engineers told Wayne that setting up an experiment, running it overnight, and getting results the next day counted as fast. In software you press a key and get a result.
A less obvious advantage, according to Wayne, is consistency. In talks Wayne sometimes holds up a CPU or a stick of RAM and reads from a spec sheet. A resistor might be rated within 20% of 100 ohms, as long as it stays between 20 and 50°C. If you make a thousand of them, they will vary by 20%, and the only way to know is to test them. Run them too long or heat them too much and they change again. Barring CPU bugs, a program that runs on one computer runs identically on another, and a sorting algorithm sorts the same list the same way. The host asks whether this means software engineers account for variability less. Wayne agrees, noting that software's variation is largely self-made: different systems and APIs. Physical engineers have that too, plus corrosion when an iron screw touches a tungsten one, and screws that are all slightly different sizes.
On closeness to customers, Wayne found no clear pattern. Some interviewees felt closer to customers in software, and some felt further away.
Openness was a clear difference. Wayne was in Hungary to speak at Craft Conference, and points out that most fields have two kinds of conferences: academic conferences and vendor trade shows. Software has a third kind, the practitioner conference, where people meet simply to get better at their work. Software is also unusual in its commitment to open source and freely available knowledge. For almost any language, you can learn it online without buying a book or talking to a vendor.
The host wonders why large companies like Uber or Airbnb openly describe how they built their systems. Wayne marks what follows as speculation. Part of it is probably cultural, but Wayne suspects a bigger factor is that software's material is the same as its product. We use software to write software, while other engineers use lathes and tools to make physical things. Wayne wonders whether 3D printing communities, which seem to share freely, work similarly because the unit of value there is also a shareable file. The host suggests hacker culture may play a role wherever getting started is affordable, such as ham radio or the early era of personal computers. Both treat this as speculation worth a separate project.
Version control stood out even more. Wayne says that all of roughly 20 interviewees named version control as the thing they wished they'd had in their old field. Other fields do have change management, but Wayne compares the gap to that between a modern car and a Model T.
What Software Could Learn from Traditional Engineering
Answers on what software could learn were more scattered. Wayne pulled out two themes. First, software is much better at iterating but worse at planning. We still need to plan before iterating, and we can get away with doing less of it, but combining the two could make software better still. Wayne notes this is also a plug for their own work.
The second theme surprised Wayne more. Software is open about its materials but worse at compiling detailed knowledge about the specifics of the job. One interviewee's two favorite books were The Design of Everyday Things, which he recommends every engineer read, and The Snap-Fit Handbook. Snap fits are the clicking catches on things like a remote's battery cover. The handbook runs about 500 pages on their engineering, shapes, and materials. Wayne's software analogy would be a 500-page book on how to version an API. That book doesn't exist, and both agree it should.
Five years after the project, Wayne says it moved them from "we are definitely not engineers" to "we probably are." Wayne adds a caveat: the project predates LLMs, which have probably changed software and the other fields in ways Wayne doesn't know. Still, as of now, Wayne thinks what software developers do is very similar to what the interviewees described doing in their own fields.
What Formal Methods Are: Making Implicit Knowledge Explicit
To explain formal methods, Wayne asks the host how he would test a max function that returns the largest number in a list. The host describes about five to eight tests: a two-element list, a long list, similar numbers, perhaps integer overflow. Wayne then asks how he knows what the right answer is. The host says he just knows, from basic math he doesn't even need to explain.
That implicit mechanism is Wayne's starting point. Step one of formal methods is to make that knowledge explicit, writing down what the function is supposed to do in a clear, unambiguous way anyone can check. For max, the result is an element of the list such that every other element is no larger. That statement is the specification. Step two is showing that the function satisfies it, which is verification. Tests do this for individual values. Types do it in another way, for example by guaranteeing that a list goes in and a single element comes out. Formal methods ask whether mathematics can show the function works for every possible list, and that is done through proof.
The host recalls university proofs as chains of rigid, allowed transformations. Wayne says formal methods are like that, but uses a calculator analogy. You can add large numbers by hand, but you usually don't. You can do proofs by hand in a theorem prover, but in industry tools automate much of the process. You state what is true at the start and what should be true at the end. The tool either proves it or asks for help, and you supply intermediate facts until the computer can finish the proof.
Why Formal Verification Isn't Used Everywhere
Before discussing tools, Wayne raises the obvious question: why isn't this done for everything? Wayne changes the example to finding the file in a directory with the most lines. Are those ASCII lines or UTF-8 newlines? What if a file can't be read due to permissions, or is a shortcut, a directory, or a binary? The host protests that Wayne is simulating the real world, and that is the point. For most interesting domain problems, Wayne says, you have to pull in so much context that even writing down what the function should do becomes a nightmare. An imperative program that is correct 99% of the time is probably good enough in almost all cases. Getting to 100% would require pinning down details like which file system is in use. The host compares it to premature optimization, and Wayne adds that ten tests may already give you most of what you need.
Wayne then describes where formal methods are used. The usual answer is "nukes and NASA," but Wayne says from firsthand experience that nuclear power plants don't care about this. They are fine with thorough testing. The second category is small, critical cores where one piece must be verified and the rest can be handled informally, such as parts of databases or cryptographic primitives. Wayne believes Firefox's HTTPS stack is verified through something called Project Everest, while cautioning that some details may be wrong. Operating system kernels fit here too. Wayne believes Microsoft formally verified parts of the Vista kernel for driver loading. seL4 is a small microkernel verified end to end in Isabelle and mostly used in automotive and military applications. Wayne notes the caveat: verification means it matches its specification. It might still do the wrong thing, but it will do what was specified correctly under the specified circumstances.
The third category is Wayne's own. Instead of verifying the whole real-world system, you verify a simplified version of it. The real system may still have bugs, but you remove design flaws from the abstraction before building them. The host summarizes this as stress-testing the plan. Most of Wayne's work has been on databases and distributed systems for tech companies. Other jobs included verifying device firmware, and what Wayne calls one of the coolest projects: verifying transponders in a train system so they wouldn't cause problems for trains passing over them. That project turned up a very old bug.
TLA+ in Action: The Trading Platform Demo
Wayne describes TLA+ as the most popular technology today for this kind of planning. It was created by Leslie Lamport, who also created LaTeX, to model distributed systems. TLA+ represents a system as a state machine, meaning every state it can be in and every transition. A model checker then brute-forces every initial state and every state reachable from it, checking properties along the way. Wayne mentions that TLA+ can also check liveness and refinement but doesn't go into them.
The demo models a simple trading platform. Each item has an owner, and there is a set of outstanding offers. Only one-way transfers are modeled, not swaps. To propose an offer you must own the item, and the offer goes into the set. Accepting a valid offer removes it and transfers ownership. Rejecting simply removes it. The next-state relation picks two different people and an item, then either proposes, accepts, or rejects. A "valid change" property says that if ownership changes, the new owner accepted an offer from the old owner. An invariant requires every change to be valid.
The host notes the learning curve. Wayne agrees this is why the tool is niche. Lamport was a mathematician in 1994 and wrote the language the way a mathematician writes. Since then, newer languages such as Quint and P, partly built on lessons from TLA+, look more like programming languages. Wayne says many practitioners started with TLA+ because the first high-profile industry demonstration, Amazon's 2014 paper on formal methods at AWS, used it.
Wayne runs the checker with three people, Alice, Bob, and Carol, trading a stick. It reports a violated property after 53 states. Wayne also shows a Graphviz rendering of part of the state space, noting that real state spaces often reach around 100 million states, so the visualization is mostly for demos. The bug is this: Alice offers the stick to Bob, who is away. Tired of waiting, she offers it to Carol, who accepts immediately. Bob then returns, sees the stale offer, and accepts. The stick moves to Bob, but from Carol, not from Alice. Carol never offered it to Bob, so the invariant fails.
Wayne explains how the checker finds this. From "Alice owns the stick," both "offer Bob" and "offer Carol" are possible, creating two states. From "offer Bob," three things can happen: Bob accepts, Bob rejects, or, because of concurrency, Alice offers to Carol. The checker explores every branch. That is why it's useful for distributed systems: when several processes can each take several steps, the possible interleavings are very hard for people to enumerate, but a computer can work through them in a night or two.
TLA+ at Amazon
Wayne describes the 2014 paper, "Use of Formal Methods at Amazon Web Services." A few interested engineers learned TLA+ and PlusCal, which compiles to TLA+, and applied them to aspects of DynamoDB and S3. They found complicated bugs that could lose data, Wayne thinks in the replication system. The host cites the paper's figure that the shortest error trace contained 35 high-level steps. Wayne, who didn't work on that project, speculates that the state space was probably about 100 million states, with many longer chains of 70 or 80 steps that were perfectly safe and just this one 35-step chain that was invalid.
How Distributed Systems Break
Beyond general race conditions and locking, the pattern Wayne sees repeatedly is time-of-check to time-of-use (TOCTOU). You check that something is valid, then act on it later. Later might mean a microsecond or a day. The bug happens whenever the condition can go from valid to invalid in between. Wayne's example, noting that real banks use ledgers, is a transfer that checks for $10, but before deducting, someone else withdraws it, so the account ends at negative $10.
The host recalls building Uber's payment system, where exactly-once message delivery was hard. Charging a card needs exactly-once, but resending for safety risks double charges. At-least-once delivery is much easier, and you have to build exactly-once on top of it. Wayne wonders whether this is why businesses authorize extra and refund later. The host adds a risk reason: authorizing a larger amount up front, as hotels do, avoids failing a second authorization later when a card is near its limit. Wayne had assumed hotels did it to discourage guests from breaking things.
Why Concurrency Is Hard, and Why Practice Matters
Wayne argues that the most interesting effect of formal methods on systems thinking comes from practice rather than theory. Wayne doubts people are inherently bad at reasoning about concurrency. Crossing a street means modeling a concurrent system full of cars. Wayne cites a paper, "Commonsense Computing," in which high school and college students spotted concurrency bugs much faster when a problem was reframed from threads to clerks at a ticket office assigning concert seats.
Wayne's explanation is lack of practice. A race condition in production usually surfaces months later, and you learn weeks after that whether your fix worked. With TLA+, you write a model, press a button, and immediately see a race condition. Fix it and you get a timeout bug, fix that and you get a TOCTOU bug. That fast loop, Wayne believes, is what makes people better at finding these bugs. With new clients, Wayne usually doesn't know how the system works, since the clients are the domain experts, but once the model exists Wayne can spot bugs in it faster than they can, simply from practice.
The host compares this to refactoring and migrations: most engineers are bad at migrations because they do few of them, while those who have done several can almost do them with their eyes closed. His own exposure to race conditions was a double charge at one point and never again, so he doesn't consider himself good at them. Wayne calls this "right on the money." Wayne adds that there are subtler things these tools teach, but the most visceral is a "hatred of a race condition" that becomes physically visible in the algorithm. As for how it has changed Wayne's own thinking, Wayne mostly writes Python day to day and finds it hard to pin down exact effects. At minimum, formal methods make Wayne more willing to reach for math-heavy solutions over simple, reliable ones.
Should Programmers Learn Math?
Wayne sorts math into three kinds. Some is so universal we forget it's math, like counting and comparing. Some is useful only in specialties; some SREs need calculus, but most programmers don't. And some is broadly useful in programming: graphs and directed graphs, matrices, and formal logic. Even so, Wayne thinks most developers benefit more from exposure to what different fields of math offer than from going deep into all of them. You need to know what exists to know what's useful, and most math won't be useful to you.
The host shares that 3D matrix transformations from university later helped him understand why GPUs matter for AI, and that a math background keeps him from being scared off by formal papers. Wayne offers a hypothesis: traditional engineering relies on continuous math, such as calculus and differential equations, which is what American high schools teach at advanced levels. Software relies on discrete math, including combinatorics, graph theory, formal logic, and set theory, which is rarely taught in high school or early university. Wayne wonders whether people fail to see math in software because it isn't the math they were exposed to. The host mentions big-O notation as shared vocabulary, and Wayne says their own understanding of big-O improved once they learned it formally describes a set of functions, not just a scaling rate.
What TLA+ Is Good For and What It Isn't
Wayne says TLA+ and most formal methods shine in highly technical domains removed from business rules. How to replicate nodes between datasets is technical. Keeping sprints from running over time is about human behavior. Wayne once had a client model something like that, and it was useful but very hard. That's why Wayne's clients tend to be database vendors, cloud providers, and hardware companies, whose work matters to business but sits several steps from its front lines.
TLA+ specifically suits discrete distributed systems, where the challenge is concurrency and the range of possible behaviors. It doesn't do floating point or decimals and doesn't handle probabilistic reasoning. It fits cases where any possibility of an error is a big deal, not cases where an error is acceptable if it happens less than one in 100 times. Tools that do probabilistic reasoning exist, but according to Wayne they lack features like functions, arrays, or numbers. If you don't need much planning, or you can iterate toward a solution and bugs aren't costly, you may not need it. Wayne stresses this repeatedly. Many people are skeptical of formal methods because they were burned by CASE tools, UML, and other "miracle solutions" imposed regardless of fit, so Wayne makes a point of not recommending a tool that isn't right for someone.
Alloy: Finding Bugs in Data Models
Wayne's second demo uses Alloy, created by an MIT professor and from a different lineage than TLA+. The model is an access control system. Resources have users who can read them and at most one parent, with no cycles. You can access a resource if it lists you as a reader or its parent does. The property is that if you can read a resource, you can read its children. The host can't spot the bug.
Wayne notes this example predates Alloy's temporal reasoning, which was added about four years ago, and shows how Alloy finds bugs in static configurations such as data structures and domain models. Wayne mentions interest from the domain-driven design community. Running it in Alloy's IDE (Wayne says most people use VS Code instead) produces a visualized counterexample. A user can read a parent, so they can read its child. But the child has a grandchild the user cannot read, because the user is listed only on the parent, and "readable by" isn't transitive.
On fixing it, Wayne notes that formal methods don't tell you how to fix a bug; you choose. Making the parent lookup transitive removes the counterexample. That fix might not be implementable, though. A database administrator might say a transitive query would crash the SQL database, and then you'd need another fix and could rerun the model.
Wayne then explains why Alloy is fast. The host works through Boolean satisfiability: P is satisfiable, P and not Q is satisfiable, and P and Q and not P is not. SAT is NP-complete, which in theory means no efficient algorithm solves every instance, but in practice solvers are very fast. Alloy translates models into huge Boolean formulas for a SAT solver. Most Alloy models check in milliseconds or a second at most, while a large TLA+ model may need to run overnight through 100 million states. The tradeoff is that Alloy is worse for modeling distributed systems, which is why most of Wayne's work uses TLA+.
The Wider Tool Landscape
Wayne surveys more tools without demos. P, which Wayne thinks was created by someone at Microsoft Research who later joined Amazon, was designed to be more accessible than TLA+. It models interacting state machines that send messages, similar to the actor model in Erlang. Quint came from people building a different model checker for TLA+ who realized they could build a friendlier language. According to Wayne, it has drawn interest in banking and, Wayne believes, cryptocurrency and smart contracts. Prism is a probabilistic model checker. Where TLA+ says a bug can or cannot happen, Prism can say it happens 10% of the time. Wayne calls it much more academic and harder to translate into, and mentions a two-part series using Prism to show that dreidel, a Hanukkah spinning-top game, is not fun.
Wayne also lists Event-B, which Wayne believes was famously used in part of the Paris Metro; NuSMV, which Wayne thinks NASA has used; and a tool for robotic control systems that Wayne considers mostly academic. All of these specify abstract models. For verifying actual code, there's Dafny, which compiles to .NET and lets you write provable code; JML for Java; Frama-C for C; Ada SPARK; and theorem provers like Coq, Lean, and Isabelle.
Property-Based Testing: The Practical Middle Ground
Wayne returns to max with a Python demo written for Logic for Programmers. There are three versions: a correct one, one that returns the max of only the first three elements, and one that returns the max of absolute values. The property test says that for any non-empty list of integers, the result must be in the list and no element may exceed it. This closely mirrors the formal specification. The difference, Wayne explains, is that formal methods try to prove the property for every list, while property testing generates many random lists, for example a thousand, and checks them.
Running pytest, the first-three version fails on the list [0, 0, 0, 1]: it returned 0, but the real maximum is 1. Wayne explains that the tool tries many edge cases first, including huge lists and tiny lists. Once it finds a failure, it shrinks the input to a minimal interesting example. The original failing list was much larger, and Wayne doesn't think anyone could look at it and see the problem. Shrinking makes the bug understandable. Property testing is less thorough than formal verification but much easier to apply. Wayne says that for most people it may be not only a place to start but a place to stop, since formal methods are niche and property testing is useful to more people.
Can AI Make Formal Verification Mainstream?
The host notes that AI is generating far more code, making review harder, and many people are suggesting formal verification or property testing as a response, though few seem to act on it. Wayne sees real movement. More clients are generating specs with AI and bringing Wayne in to fix or review them. Property-based testing is spreading too; Wayne notes that Kiro, Amazon's spec-driven development platform, advertises property-test generation as a key feature. There are also many papers on generating specs with AI. Wayne finds this exciting, since much of the difficulty of writing specs is wrestling with technical syntax and semantics.
But from Wayne's own experiments, as of March, AI is very bad at coming up with properties. Wayne notes a new Claude model had just been released and things change monthly, so this could be out of date. Give a model a spec and properties and it can fix the spec to make them pass. Ask it to invent properties, and it may propose something like "either P or not P," which is always true, and then celebrate verifying it. Liveness properties, which describe how a system evolves over time, are especially hard. Wayne tells clients that AI does a good job generating the design, but expressing what the design is supposed to do is still their job.
The host brings up a March 2025 blog post, "The Coming Revolution in Distributed Systems," by an engineer on GitHub Copilot, describing AI producing TLA+ specs from Azure storage production code and uncovering a subtle race condition that code review had missed. Wayne says the same engineer later built a tool called Lamport agent and seemed more successful at generating properties than Wayne had been. Wayne adds two caveats. The engineer is an expert specifier who can already do this without an LLM, which matches a general pattern: to get good results from AI, you need to already know how to get them without it; AI just gets you there faster. And one of the systems already had a sophisticated spec written in P, which the model may have drawn on. Wayne doesn't know whether that matters. Wayne also mentions a write-up by a researcher about a multi-year formal methods project at a large Chinese cloud provider. Between doing the work and publishing, LLMs had compressed the time it took people there to write formal specs. Overall, Wayne thinks the people succeeding now are specifiers using AI to amplify their own ability. The fully AI-written specs posted on Hacker News tend not to be very good.
Will AI make formal methods mainstream? Wayne thinks it's making them more popular, perhaps from 0.1% to 0.3%, "which is huge," but isn't sure about mainstream.
The host asks about Wayne's June 2025 newsletter line calling AI a "specification force multiplier." Wayne says that post already listed what AI was good at: fixing syntax errors, explaining error traces (turning a 35-step trace into two paragraphs of English), and boilerplate changes. It was okay at writing properties from a very precise description, bad at fixing specs, and very bad at producing properties on its own, with output that was trivial or too tied to implementation details. Wayne jokes about being consistent, and says the weakness noted in 2025 was still there as of March. So how much do you need to know to use LLMs for this? Wayne says the basics matter, at least so you can tell when the AI is doing something wrong.
Logic for Programmers and Where to Start
Asked why Logic for Programmers argues that formal logic is so useful day to day, Wayne gives two answers. Logic is about manipulating Booleans and statements, much like school teaches manipulating numbers. There's little difference between 1 + 1 = 2 and "true and true is true," and Booleans are central to software while logic is rarely taught in school. Empirically, Wayne keeps finding situations where logic enables something that people without it struggle with.
For an engineer already doing unit and integration testing who wants to harden distributed systems, Wayne deliberately goes "90°" and recommends Nancy Leveson's Engineering a Safer World. Leveson is an aeronautics engineer who investigated incidents including the Therac-25 radiation cases and the Columbia disaster, and studied why accidents happen in complex systems. Wayne found it incredibly insightful for understanding how systems break.
Anxieties About the Profession
The host revisits a post from a year earlier listing six things that could all be true, and they react to each.
First, vibe coders will never be as good at software engineering as experienced engineers. Wayne says probably true, since you can't succeed without the basics. The host agrees, noting his own attempts at a game outside his expertise turned into a "vibe-coded mess."
Second, LLMs can significantly help professionals write high-quality software quickly. Wayne thinks this is true even without having AI write code, just from asking where a bug is or which library to use. The host adds that engineers with deep knowledge who control the tools, rather than being controlled by them, get a lot done.
Third, LLMs will cause many developers to lose jobs. Wayne is unsure. US software hiring seems to be recovering, and it's hard to separate AI's effect from the end of zero interest rates and the post-COVID downturn. Wayne leans toward the latter but notes models are still improving. The host says Pragmatic Engineer data shows more openings in the US, slight declines in Germany and France, and a shift in who gets hired: AI engineering is spreading into more fields, while front-end and mobile hiring is falling. He points out that demand has always shifted, recalling when "10 years of Java experience" was the most sought-after profile.
Fourth, LLMs will open software work to many more people. Wayne agrees: if a product needs one developer instead of five, you're more likely to hire that one.
Fifth, those jobs will be lower paid and lower status than in 2008–2022. This is what scares Wayne most. Wayne left physics, walked into tech, and ended up proving systems correct full time. Wayne asks what other engineering field lets someone walk straight in, or pays to fly someone overseas for a 45-minute talk. Wayne fears software becoming like any other white-collar job, with two weeks of vacation and two sick days. The host notes that this is already the reality for many engineers and that software has "massive privilege." Wayne agrees, saying it would be nice if everyone had the same, but not by software losing what makes it special.
Sixth, high-paid jobs will remain but be rarer, more competitive, and less developer-friendly. The host fears this is already happening and compares it to investment banking traders, who are fewer, still well paid, and hard to become. Wayne says most jobs ossify as standards set and more people enter, and software escaped that longer than most.
The host reads Wayne's closing prediction from a year earlier: software development will survive the next ten years but become like any other white-collar profession, without $200,000 salaries, unlimited vacation, or strong bargaining power, because "automation comes for all of us, even us automators." Wayne now adds a complication. A doctor friend recently vibe-coded a shift-trading platform for their hospital without knowing how to code. It saved time and made the nurses and doctors happier. Wayne finds it strange to weigh their own cushy job against that doctor's needs and says they don't know who matters more; everyone will find out over the next ten years.
The host relays a conversation with a veteran of the field who compared this moment to the late 1960s and early 1970s, when teachers and others outside software began buying computers and hacking. The host feels something similar as people outside tech tell him about things they're building. Wayne points to Clay Shirky's essay "Situated Software," which argues that much software should be built for just a few people, a family, a community, or a single school. Until now that required someone in the group to be deeply into computers. Now anyone can have situated software, which Wayne expects to change the world in ways that are "strange," "terrifying," and "exciting."
Three Books
Limiting themself to software books, Wayne recommends three. First, Leveson's Engineering a Safer World, which Wayne believes is free online. Second, Data and Reality by Bill Kent, a database designer who worked on IBM databases. It asks what data is, what makes something an entity, and whether "a book" means a physical copy, an edition, or a series. Kent concludes that data isn't reality but our view of reality for a useful purpose. Wayne notes the 2011 republication altered the text, so the second edition is the good one, though it's hard to find. Third, David Agans's Debugging: The 9 Indispensable Rules, a book of war stories and principles that Wayne gives to every junior engineer. Almost nobody treats debugging as a discipline beyond basic heuristics, and having something is better than nothing. Wayne notes a used copy costs about $10.
In his closing remarks, the host says he now better understands why formal verification is unlikely to go mainstream even with AI. The tools feel rigid for the real world. They work for parts of a system that can be modeled mathematically, but writing TLA+ specs for everyday programs seems pointless to him. The takeaway he highlights most is Wayne's point that engineers struggle with concurrency bugs mainly because they so rarely get practice finding them.
Let's talk about formal methods. There's some sort of implicit mechanism in your brain that can see that and know what the function is supposed to do. So, 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?
Why are we not doing formal testing for everything?
When you start talking about most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get it correct 99% of the time is probably good enough to use in almost all cases.
One story I've heard and I think you might have been involved is AWS using TLA+.
They talked about how a couple of people in the company were interested and learned TLA+ and another language called PlusCal and applied it to aspects of the DynamoDB and S3 storage systems. In doing so, they were able to find fairly complicated bugs that could potentially lose data.
We have AI generating way more code, maybe formal verification or property-based testing could be more useful. Do you think this will happen?
I've been doing a lot of experience with this myself and I think the one thing AI is extremely bad at
There's a popular theory going around that AI will finally make formal verification go mainstream because when machines write the code, humans will need mathematical proof that it's correct. Today, I'm talking with one of the best people to respond to this, Hillel Wayne, a formal methods consultant. He's taught 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, Hillel's research interviewing 15-plus traditional engineers to answer the question: can software engineers also be considered real engineers? How AWS used TLA+, and 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 where this approach could go mainstream with AI, this episode is for you.
In today's episode, we'll get to the question, does it make sense to use formal methods to verify AI-written code? As a spoiler, the answer will be proper formal methods are an overkill for this, but lightweight formal methods can actually be helpful.
This is where I need to mention our presenting sponsor, Antithesis. Antithesis verifies your system correctness by running your whole system in hostile simulation and finding bugs. It does this by using an approach called deterministic simulation testing, or DST, which AWS distinguished engineer Mark Brooker and Ankush Desai have described as lightweight formal methods.
Setting aside Antithesis for a minute, if you as an engineer want to get more serious in verifying that your system works as intended, your best bet would be to use lightweight formal methods.
Now, back to Antithesis. Antithesis turbocharges testing by running your whole system under aggressive fault injection. Imagine Antithesis as hundreds or thousands of versions of the Mario game running, each instance aggressively trying to break the game with increasingly weird input combinations. With Antithesis, you can specify properties at the whole system level and Antithesis will actually try to disprove them, so you can be confident that if your system holds up in Antithesis, it will hold up in production. There's good reason teams like Jane Street, Fly.io, and the etcd community rely on Antithesis. Head to antithesis.com/pragmatic to learn more.
So, Hillel. Welcome to the podcast.
Thank you so much. I'm really excited to be here.
It's so nice to have you here. I was curious, you're very well known for formal methods, for programming, for logic, for all of these topics, but how did you get into tech?
So, to start, I never really saw myself as a technical person. I liked computers growing up and I did a tiny bit of programming. My father was a programmer, he taught me Visual Basic. But, I always wanted to do physics and math. That was my dream. I put in my college application, I want to listen to the harmony of the universe. Don't ever take advice from a high schooler for writing, just saying.
But, after about 3 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, why don't I 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 to Chicago, and then in the course of the next job I was working in, also in education technology, I fell into my current niche, which is formal verification and formal methods.
The first time I came across your writing, because you write a blog, a pretty regular one, and I really enjoy your writing. The first time was with the Crossover Project. This was a project where you attempted to answer, are we as software engineers actually engineers?
Yes.
Can we talk about this project?
Absolutely. So, I guess I should probably start with the motivation. Which was I've read a lot of books on software, and I've read a lot of online articles about software. And one of the favorite things that software developers do is argue about whether it should be engineering or not, right?
And there's the camp of people that say, well, we don't deserve to call ourselves engineers, we should not. They are so far above us, we shouldn't even consider ourselves in the same space. And then there are the people who are like, what we do is so special and so unique, engineering doesn't have anything on us. They can't hold a candle to what we do. You see books like Software Craftsmanship, which talk about how, oh, engineering is this really boring, slow field, and software is this incredibly creative, special, wonderful thing.
I was very firmly in camp one. I thought we were not engineers, we didn't deserve to call ourselves engineering, anything like that. What I do for work is really carefully analyzing software systems, and I thought, ah, this is real engineering, and everything else is not engineering.
Then I found this talk by Glenn Vanderburg, where what he did was he read a bunch of engineering books and compared them to what we do in software. And he said, "Actually, this looks really similar to what we do in software." And I thought, "That can't be right. I need something more rigorous. I'm going to have to talk to people who did both engineering and software development and see what they say." And they all agreed with him. So, I was wrong. We're engineers.
Can we go a little bit into
So, as I started talking to the first people, I realized that this was a much deeper project than I ever expected. And I decided I needed to have as comprehensive a look at traditional engineering as I could possibly get. There are many kinds of engineering. There's not just building bridges, but there's designing circuits, there's figuring out chemical processes, there's industrial engineering, which is figuring out the layouts of factories and how we organize kinds of labor.
There's just so many different kinds, and I wanted to see every single kind of view into what engineering looked like to compare them all to software, which when you think about it, when we say, "Oh, software's 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 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're looking for ways to iterate on the plan. You do things like build scale models, you software to simulate the building, you do CAD models, etc.
And in other fields, for example in electrical engineering, you have the ability to come up with a design, test it, and then throw it to the fab and get something back. So, they will iterate a lot more than civil engineering does.
Interestingly 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 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.
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 does have things on us, which you were hoping to find, or places where actually software engineering is ahead in some ways?
There are 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 as software engineers is that our work is a lot more consistent than other fields. The example I always do sometimes, because I've given a talk about this, is I would pull out a CPU chip or a stick of RAM and I'd say, "Hey, here's the spec sheet." And if you look at the spec sheet, it says, "This resistor has a resistance that is within 20% of 100 ohms as long as you keep it between 20 and 50° C."
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 CPU bugs or anything like that, the same program, if it runs on this computer, it'll run on your computer, exact same. Sort this list the exact same with this 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 that we have is kind of of our own making, right? We're basically saying, "Okay, we've got all these different systems, all these different APIs," versus other people who are like, "We have all these different chip sets, we have all these different cores or sizes." But also, if you happen to touch 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 and some are a bit longer, etc.
And how did you see the similarities or differences of software engineers, for example, who 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 to or know your customer, or just not know them at all?
I think it depends. Because different engineers that I talked to had different experiences. Some said that they felt that with software, they felt much closer to the customer. With other ones, they said they felt much further. So, I think it's hard to really tell there.
One thing I remember vividly is a difference that you pointed out which was very different and almost makes software engineering a bit higher status or a better place: open source, the concept of open source.
Yes. So, that is one thing that seems very special about software versus any other field. The reason I'm here in Hungary right now with you is because I'm going to be speaking at Craft Conference, right?
Yeah.
Most other fields of engineering, or in fact any other field of human labor, has two kinds of conferences: academic conferences where they talk about research, and trade shows where vendors try to sell to companies. Software is kind of unique in having the third kind, 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 freely available. For any language, you can probably find out how to learn that language online, right? You don't have to buy a book. You don't have to talk to the vendor to learn it. That's something really special about software.
I wonder why this might be, 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, I think of an Uber or Airbnb, these are hundred billion dollar companies, they will not particularly hide how they built that piece of software. Uber publishes and does talks about their app that is used by all these people, how exactly they built it, or approximately. I wonder why this became unique in software and not in 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 lathes to build things. We're 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. I like this thinking of materials used in each engineering and how our material is software itself. Of course there's hardware engineering and we know that's a bit different, of course. But already there's a divide between hardware engineers 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 who do 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 sharing things freely. I wonder if that's the same, because it is so easy to share and because 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, ham radios, which is not engineering, but there's a thriving community where they share the setup, the things, they talk with each other. Small electronics might be. And then ultimately software started in the, what, '70s when it was affordable and anyone could buy a computer. Maybe the internet. I'm also just speculating.
Yeah. Definitely something worth doing a follow-up project on, right?
Yeah, well, you've already spent a bunch of time on it.
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 version 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 other fields, but I think version control as we have it is so much more sophisticated than anything they have. It's like comparing a modern car to a Model T.
What do you think, are there things that, now having talked with so many people, I've learned about the different engineering cultures, like actual charge technology and 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 I talked to mentioned those two things of openness and version control, I got a much more scattering set of answers when talking to people about what we could learn from their old fields.
The two things I kind of gleaned out is that, one, while we are a lot better at iterating than other fields, we're worse at the planning part. We still need to do some kind of planning before we iterate, and we just aren't as good as those other fields. In part because we can get away with not doing it as much, but we could get some sort of fusion of the two and get even better than we currently are. Which, hey, plug for what I do.
The other thing that I think is more interesting in terms of being a bit more shocking to me is that while we're better at being open about all of our materials, we seem to be worse at compiling information about the specifics of our job. And that's a bit loosey-goosey, but the example I keep coming back to is that one of the engineers that I talked to had two favorite books: The Design of Everyday Things, which he recommends every engineer read, and The Snap-Fit Handbook. Are you familiar with snap fits?
No.
I'm looking around here to see if there's one, if I could just show it, but you know how remotes have that little clicky thing in the back that holds the battery in?
Yeah.
That's a snap fit.
Mhm.
It is a physical device that basically clicks into another device to keep them fused. And this was a 500-page book all about snap fits, their 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 5 years ago. This many years later, what is your inclination? Are we actually engineers?
I think so. I think this project and writing about it and thinking about it has firmly moved me from the camp of we are definitely not to we probably are. I do want to caveat that I wrote this before LLMs were a thing, and this has probably changed our field as we know it, and it's probably also changed those other branches, and I don't know how. So, that could have changed the calculus between the two spaces, but as of now, I think, excepting 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 the show notes below. I do recommend going into it. So, let's talk about formal methods. How did you get exposed to them? And for those of us who are not deep into it, what are they?
I'm going to give you a function max, right? Which should, given a list, return the largest number. What would be a test you'd write for that?
I'd write a test where I do a list of two items, and 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 like five tests. Try to think about integer overflows potentially, try some tricky ones. Maybe I'll take it to 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 learned maths in school. I know which number is bigger, honestly. I look at it. I have this, I guess, ingrained knowledge. It feels like very basic knowledge that I don't even have to explain.
Right. You have some ingrained knowledge you don't have to explain, such that you can look at, say, the max of two and three and know it's three, right? That's interesting. There's some sort of implicit mechanism in your brain that can see that and know what the function is supposed to do. Step one of what I do with formal methods is asking, can we take that implicit knowledge and make it explicit? Can we figure out what a function is supposed to actually be doing and write that down in a way that can be shown to anybody?
So, I would basically in this process say 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 the way that we can formally say what the maximum of a list is. So, that's part one. Just learning how to look at functions and say, okay, I know what this is doing. How would I explain what this is doing in a way that is clear and unambiguous?
Then step two is asking: every single test you've written is basically some facet of this. It is an element of the list, and it is the number in that list such that every other number in the list is smaller than it. Now that we have that, what's the best way to show that our function actually satisfies that specification?
Tests are one way. Those are basically taking individual values and showing how those conform 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, you have to make sure that every time we call it, that's what's true. So, basically coming up with the properties of the thing, what it actually is, is the specification of it. And then showing the function matches that specification is the verification.
And what formal methods ask is, can we use mathematics to show that it works not just for the cases that you asked for, but for 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 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 typically you 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 it. Those are one of the proofs we do. 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, I use my brain as a calculator, otherwise I just punch it into the calculator.
Yeah, so similarly, a lot of formal methods, that math and transformation, while you can do it by hand with 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, these things are true at the beginning. I want this to be true at the end. Can you figure this out?" And they'll be like, either yes, I can prove these things match, or no, I need a little bit more help. And you say, "Okay, at this point, I'm going to also let you know that this is true." And they're 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 formal methods, this all sounds logical. I think it's easy to follow. In practice, what techniques, technologies, tools does the tech industry use to actually prove that some software works?
To get to that, we need to ask another question. Why isn't this being done for everything?
Okay, let me ask that question. That's a good question. Yeah, this all sounds sensible. It would be nice to not have to write out those five or eight tests. And I know that those tests might not cover all edge cases. Been there, done that, where you miss one, and I didn't think that I didn't do a formal proof. I thought, well, I missed a test case. That's on me. Sorry. Let me put in that test case. I now have nine tests, and now I go and think I did a great job. Why are we not doing formal testing for everything?
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 in kind of an imperative style. It goes through each file in a for loop, I count the lines. I cannot tell this easily.
Okay, are we talking about ASCII lines or UTF-8 newlines? What happens if for one of the files you don't have the file permission to read it? Should you basically ignore it, or should you say, "Hey, my function might be wrong"?
You're now kind of trying to confuse me.
What if one of the files is a shortcut to another file? What if it's actually a directory?
And you're now simulating...
What if it's a binary?
You're now simulating the real world.
Yes, and that's the problem we have: when you start talking about most interesting domain problems, you have to pull in so much context that basically even writing what the function is supposed to do becomes a nightmare. The imperative program you write that will get it correct 99% of the time is probably good enough to use in almost all cases. And if you want something that works in 100% of the cases, you've got to figure out, "Okay, what file system are we using?" You have to figure out everything.
Yeah.
And that's why it's not done.
And basically it would just not be practical. For 99% of people it would be, "Why are you wasting your time?" It's like premature optimization, right?
Yeah, especially when, as you say, writing 10 tests might get you most of what you need.
What are practical technologies that you have seen used in some part of the industry, where, even though I'm assuming they will be somewhat heavyweight, because it sounds pretty heavyweight, the return on investment of using this heavyweight stuff is worth it, that teams in the industry are using today?
Right. And here we can basically start to break this down into 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 NASA, but I can tell you from firsthand experience nuclear power plants do not care about this stuff. They're actually just fine with thorough testing. It's okay.
Okay, so then category two is really focused cores of programs, where they need one specific part of the program to be really verified, and for the rest of it they can use informal methods. And this is usually things like small parts of databases or cryptographic primitives. I believe that the HTTPS stack in Firefox is verified as part of something called Project Everest, but I might be getting some details of that 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 operating system kernels are good uses for this. A couple of examples I can think of: I believe Microsoft used some formal verification of parts of their Vista kernel for the driver loading. Famously, there is an operating system called seL4 that has been end-to-end verified in a language called Isabelle. 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. With a caveat, meaning that it's matching the specification. So, it might do the wrong thing, but of the things that you specify that it has to do right, it will do those specific things right in the right circumstances.
The last category is the kind I work in, which is asking, "Okay, what if instead of verifying the entire real-world system, which is a nightmare as we just discussed, we create a simplified version of the system and verify that? Then the actual system might still have bugs, but we can iron out the issues in the abstraction such that we don't actually build them into the real system."
And so that's a 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, again, 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 interesting gigs. I've had one gig that involved formally verifying the firmware of a device kernel. And honestly, one of the coolest projects I've ever worked on was verifying the transponders of a train system, to make sure that they wouldn't cause problems for 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 codebase, you really don't want an AI model to be taking guesses. Auth is at the 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, SCIM, and fine-grained 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 workos.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, on stage at AI Engineer's World Fair and also hung out with their team for a few days in person. Here's a few of the 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 a 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 his team strongly believe in how simplicity scales, and this is the reason that object storage is turbopuffer's only dependency. The team do seemingly silly things like build their job queue in a single file on object storage because they understand their core primitives, and they know how they scale.
To check out the whimsical animation, or if you're building AI products, head to turbopuffer.com/pragmatic. And with this, let's get back to how TLA+ works with a demo from Hillel.
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+. It was invented by Leslie Lamport, the same guy who made LaTeX, the typesetting language, actually.
Oh, yeah. All the PDFs behind the scenes are LaTeX.
Yeah. PDFs behind the scenes are LaTeX. And he wanted a language that could be used to model distributed systems. So, he basically created this thing called TLA+. Temporal Logic of Actions Plus. Everybody always asks about the name. You don't need to know the name. Just know that it's TLA+.
And what it does is it basically represents the state machine of a system. Every possible state it can be in, and every possible state it can transition to. Then, we can use a brute-force model checking, where we basically find every initial state, and every state that can evolve from those, and check if they have properties. TLA+ 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. In this demo, we have a simple model of a trading platform. Each person on the platform has a set of items, and they want to trade these to other people. The way that we're going to show the simplified system is that each item is assigned to a person. There's also a set of outstanding offers. We're only going to model sending items to people, not swapping items.
If you propose an item, you have to own that item and it's basically added to the set of offers. And then you can accept an offer. If that offer is available, you remove it from the set of offers and the owner transfers. If you reject the offer, it's just removed from the set.
Then we define what can happen next. A next state, as in one of the ways the system can evolve, is we pick some two people that are different. That's what this from dash equals two means. And some random item and either you propose that item, accept a proposal for that item, which must already exist, or reject an existing proposal.
Below we have a property that a valid change is one where if the owner changes, it is because the new person accepted an offer from the old person. So, if the item goes from you to me, it's because you offered it to me and I accepted that offer. Finally, we have a change invariant, some property of the system saying every change is a valid change. Now, what's the bug in this?
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 Leslie Lamport made this in 1994, he was thinking of it mostly... he was a mathematician, right? So, he was using his mathematical background in writing how a mathematician would write some symbols.
In the 30 years since that point, has it been 30 years since 1994 already? A lot of languages have been developed in part from the lessons of TLA+ that make things 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 grok.
The reason a lot of us used TLA+ 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+ for this. So, that's what a lot of us just 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? Well, will the system help tell us, or do we now need to think through what case we missed?
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, Carol, and have them trade around a stick." And then I tell it, "Make sure this property that the change invariant always holds."
Always hold, yeah.
Now, I just have to run this. I'm also having it output the state space for you, so you can see what that looks like. And it just puts out the error for us. It says the property's been violated. It took 53 states to find it.
And the way it works is... it's on a small screen, so it's being word wrapped, but if I see it, it kind of looks like this. Essentially, the error is as follows. And let's actually see if I can show it to you with the dot file. It's dot biz. Graphviz, 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 state spaces end up being like 100 million states, so usually these aren't that useful. It's mostly a thing that we sometimes use for demos.
So, the error is as follows. Alice, Bob, and Carol are on the system, and Alice owns the stick.
Yep.
Alice makes an offer to Bob. Bob is away. Alice gets tired of waiting for Bob to come back to make the offer because she wants to get rid of her stick. She makes the offer to Carol. Carol immediately accepts. So, the stick transfers from Alice to Carol.
Now, Bob comes back, sees the offer from Alice to Bob, and goes, "Oh, yeah, I want that stick." Clicks the button, and now the stick becomes Bob's. But, it did not transfer from Alice to Bob. It transferred from Carol to Bob. So, the change invariant, that if the stick went from Carol to Bob, it must be because Carol made an offer that Bob accepted, was violated. And therefore, the system raises an error.
And then, how did the system simulate this? It had to simulate a state where Bob was waiting or didn't respond for a while and responded later?
We basically assume we start in a state of 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,
Mhm.
Bob reject, or, and this is where the concurrency comes in, we can do offer Carol, right?
Yep. I see.
Yeah.
Mhm. I see where this is coming, and then when you continue, we will hit the bug.
Yeah.
The change invariant will be invalid at whatever step that is run at.
Right. And that's actually where a lot of this becomes useful for distributed systems, because often it'll be like, "Okay, process one can do one of six things, process two can do one of six things, process three can do one of six things." And when you do this brute force, you get states like process one takes step one, then process one takes step two, then process two takes step one, then process one takes step three, then process three takes step one and two, then process two takes step two and three, etc. 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+ is, then.
Yeah, basically.
And one story I've heard, and I think you might have been involved with this, AWS using TLA+. 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 formal methods at Amazon Web Services. And they talked about how a couple of people in the company were interested in and learned TLA+ and another language called PlusCal, which is something that compiles to TLA+. 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 needed to be really determined.
Mhm.
And precise.
I did not work on that project, of course, I don't know what the details are. I can speculate that the reason it found a 35-step bug was because the state space was probably 100 million states wide. So there were plenty of, say, 70- or 80-step chains that were totally safe. It just happened this one 35-step chain was invalid.
Through working with a lot of customers and teams that have used formal verifications with distributed systems, what are some problems you've come across with distributed systems that might be a bit of a repeat pattern of, you know, how they break down or why they break down?
And I can think of one thing that, besides just general race conditions and locks, this is the one that is always going to be one I have, like, yes. It's another time-of-check-to-time-of-use bug. And time-of-check-to-time-of-use is a situation where you are checking to see if something is valid, can be done validly, and then you see that it's correct, and then a little bit later you do it. Sometimes that little bit later is like a day later, sometimes it's a microsecond later, but it's any case where it is possible for something to go from being valid to being invalid in between the time you check and the time you use it.
A good example here is, imagine you're withdrawing money from a bank account and putting it to another bank account. And this is not how banks work, I know, they use a different kind of ledger, but just as a demonstrative example, you check, oh, do they have $10 in their account? Yes, we deduct $10, we put $10 in this account.
But what can actually happen is you check, do you have $10 in this account? Yes. And then while you're still getting ready to withdraw, someone else quickly runs in and grabs those $10 away, and now there's $0, and now you deduct those $10, you have negative $10. That's a time-of-check-to-time-of-use kind of bug. They happen everywhere.
Yeah, and it's very interesting because when we were building Uber's payment system, I realized, or I learned, that the problem of having a message delivered in a distributed system exactly once is a very difficult one, because typically that's what you need when you want to do one charge, you want to charge a customer's card exactly once, because if you send multiple messages just in case one of them gets lost, you now have double charges. And it turns out it's a complicated problem. It's a lot easier to do at-least-once delivery
Yeah.
than exactly-once delivery, but of course you need at-least-once delivery to build on to create exactly-once delivery.
Yeah. I wonder if this is why a lot of businesses, they just charge you extra and then refund you some amount. That seems easy to do from an engineering perspective.
As well, it's also from a risk perspective. You eliminate a lot of edge cases by authorizing up front on a 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 would 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, 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, 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+, learn how to verify 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 high-level 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 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 a concurrent system. I remember whiteboarding just boxes and imperative. 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, when you cross the street, aren't you working with a concurrent system? There's just cars everywhere. They're going to hit you. You're going to die if you don't model a concurrent system in your head.
And there was actually this really cool paper I found called Commonsense Computing, where some people were trying to figure out how people thought about concurrent systems. When talking with high school and college students, they changed the concurrency problem from, "Hey, we've got these threads doing some operation," to, "Hey, we've got these 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 you 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 after that if the fix actually worked.
Whereas with TLA+, I write my model of the system and then I click a button and it immediately tells me, "Hey, race condition." And then you fix it and it says, "Hey, timeout bug." And then you fix it again and 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 and think about problems in distributed systems more easily.
I've found personally that when I work with new clients and we're modeling their system, I usually have no idea how their system works, right? Because they're the domain experts. I just 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 I've had so much more practice with it. And I think that's the main change in how it affects people's ways of thinking about distributed systems. It gives them actual practice in seeing how the 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, let's say just changing a function name, and then you need to go and change all the references of 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 checks, 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 they close their eyes and they can just do it.
Yeah.
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 good at thinking about them.
I think it's right on the money.
It sounds like you coming into teams or to these clients, you at least give them some practice, at the very least, of how to think about this category of errors, even taking out the tooling itself.
I think there's also more subtle things that you start 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+ is like for most of us writing TypeScript or the language that we're familiar with. How has your thinking changed? And are there any similarities between when you program in an imperative language and then you learn a different one, like a declarative language, which requires very different thinking?
Mhm. And that also depends on the declarative language. I've done a lot of stuff in logic programming languages and I've done some stuff in array languages, but you show me C++ and 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 pin down exactly what, though. My usual hack language is Python these days, just because that's one of the first things I used and I just know it very well. And I think at the very least the formal methods make me much more willing to reach for mathematical solutions or math-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 a discussion back and forth. Can we talk about the core of the argument?
How math is useful in programming is a very interesting question, right? So first of all, there's math that we all find so useful we forget that it's actually math. Like counting. Counting is math. Knowing whether one thing is bigger than another number is math, right? It's just math that we have been taught from a very young age because it is so important that no matter what you're doing in life, you need that math.
Then there's a lot of math that is useful for very specific specialist topics. I've talked to some SREs who need calculus, but I think most programmers don't 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 what math has in the various fields versus just going all in 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 had pretty heavy math education for computer science, from algebra to computational theories of form, even formal methods. At university I learned a bunch of advanced math that at first, when I came into the industry, 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 and then I feel it with your general understanding, and it helps you be unafraid to go deep. So, if I see a paper with a formal proof, I'm 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 it, and 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, which is basically 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 in software engineering, 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 combinatorics. And of course, 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, "Okay, how efficient is this algorithm?" And then there's the big O notation. We have the language to describe how efficient in space and time it is, and you can do trade-offs, and once two people know the same thing, you can have discussions about these things. On one end it's very abstract, but on the other hand, if you're close to the machine, it can be very useful.
I've also found that my understanding of big O notation got a lot better once I understood the mathematics behind it, because I think it's usually explained in terms of, "Oh, this function scales at this certain rate." But it is more formally a way of describing a set of functions. And then there's the math of how we do asymptotics and stuff, etc. I think even the technical aspects of math do help a lot in understanding those.
Yeah.
And with TLA+ specifically, in what cases have you seen in the industry TLA+ being a good fit for certain problems, and in what cases would you never consider it?
I think the case of TLA+ and most, not all, but most formal methods, they shine the most in highly computational domains, where most of the problems are highly technical and not business embedded. And what I mean by that is that how do you replicate nodes between these two data sets is very technical, right? Something like, I'm trying to think about a good example here, like how do we make sure our sprints don't go over time? Is very business, right? It deals with very human behaviors. I've had a client model that, and we got some use out of it, but it was very hard. So, that's why a lot of my clients end up being things like database vendors or cloud computing people or hardware people who are working in a space that's very important for business, but several steps removed from the front lines of that business. The other thing I would say is that different tools are good at different things. TLA+ in particular tends to be good at discrete distributed systems, where the main challenges are messing with concurrency and possibilities of internally being 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 should be saying: where the kinds of errors you care about are ones where, if it is possible for an error to happen, that is a big deal. It's not good if 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 need to spend planning. If you don't need to spend that much time planning, this is going to waste your time.
I do want to add that 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 a person who talks about a really exotic tool, to constantly emphasize, "No, I'm not trying to convince you to 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, "If this isn't the right tool for you, I am not going to recommend it."
And then, can 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 from Alloy's lineage. Just like there's many different kinds of programming languages, there's many lineages of formal specification and verification tools. So, this example is a simple access control system.
So, we have a set of resources and users who can read those resources. So, each resource has some people who it's readable by. And resources may or may not have a parent resource. Lone means less than or equal to one resource. There are no cycles. So, no resource can have itself as a parent or its parent's parent as a parent.
Yep.
You can read access a resource if the resource indicates you can read that resource or if its parent indicates you can read that resource. And we have a property that if you can read a resource, you can read its children.
Yep.
This system has a bug. What is it?
I mean, I'm glancing at this and this all makes sense to me. I thought this is it, because we're saying all of the parents can access it. I'm assuming the bug, if there is one, might have to do with something that we talked about earlier, like accessing in certain areas. No idea. Can we run it?
Yes, we can. So, this was actually made in an earlier version of Alloy, just for context. Alloy did not have any sort of temporal reasoning over state up until about 4 years ago. So, this is one example I used from before that of basically how you can analyze and find bugs in static configurations. In Alloy, that often means finding bugs in data structures or in data models and domain models, actually. So, there's actually 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 VS Code. Now, if I execute this, here's the counterexample.
Okay.
And this is one of the nice things about Alloy specifically, is that it can generate 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 its parent, so we can read the child.
Yes.
The child has a grandchild. We cannot read the grandchild, because 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.
Mhm. And to visualize this for us.
Yes, which is quite nice. One of the reasons why people really like Alloy.
Nice.
It's a bit worse for modeling distributed systems, though, which is why most of my work is in TLA+.
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 formal methods don't really tell you, here's how you fix it. It lets you choose how you want to fix it. One thing I could do is I could say, "Okay, I'm going to say that this is a transitive lookup, too, that we transitively close over all parents." And if I execute that, no more counterexample. That said, that might not be something physically implementable. I might try to tell people, "Hey, in our SQL database you can 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. 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 has solver SAT4J? So, have you heard of SAT, SAT problems?
No.
Okay. Is there some variable that makes the statement P true? If I can make P true or false, is there a way I can make that true? Well, let's see: if P is a Boolean and I just 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 go true. Yeah.
So that statement is 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 unsatisfiable, because no matter what Boolean you do, the and false will always be true.
Lovely. What you've just done is a Boolean satisfiability problem. Taken some sort of statement of a ton of Boolean variables, in this case two, and either found some assignment that makes it true,
or said that it cannot be made true. Now, Boolean satisfiability is what we call NP-complete. And what that means in theory is that there's no such thing as a perfectly efficient algorithm that solves all problems. In practice, that means that we can solve them really fast.
So, often what makes Alloy interesting is that unlike TLA+ which mostly brute forces, Alloy can be converted into a satisfiability problem. I'll open this up. And it is able to turn that model into a Boolean satisfiability problem 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 at most, whereas often for like a large TLA+ model, you have to basically churn it overnight to go through all 100 million states.
>> Can we talk about some other tools on the, I guess, the table of someone looking into formal 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 successful to TLA+ 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+ among other things. So, it basically looks like a set of state machines, interacting state machines that send messages to each other, almost like the actor model in like Erlang or something like that.
>> Yep.
>> So, there's that. There's also another one in the same space as Quint, which was basically people who were making a different kind of model checker for TLA+ and then realized they can make an entire language that was easier for people to pick up. They've gotten a lot of interest in the banking and I believe cryptocurrency space. Smart contracts.
So, another one 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+ 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 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 dreidel?
>> No.
>> Okay, it's a game that you play on Hanukkah 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, but there's also, I mean I could just keep listing. There's like Event-B which has been used, I believe famously, in part of the Paris Metro system. There's like... comes from a Dutch university. TLA X which is mostly used for like robotic control systems, but I think that's mostly academic. There's like NuSMV which I think NASA's used for a bunch of stuff. I can keep going.
Then of course there's all the... This of course is only for specifying like abstract models of systems. If you want to talk about verifying code, then you've got things like Dafny which is basically something that compiles to like .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 Frama-C for like checking C. You've got Ada SPARK. And you've got the theorem provers like Rocq and Lean and Isabelle and I can keep going.
>> I wanted to ask how this property-based testing relates to formal verification. And before, let's just like lay out what property-based testing is.
>> So, let's go back to the entire thing with max, right? Max of 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 in that list, right?
>> Yep.
>> 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 basically three variants of max: a good version which just returns the max of the list, one that returns the max of the first three, and then one that returns the max of the absolute value.
>> Yep.
>> 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,
>> Yep.
>> the maximum value of that function should be in the list and all other values should be less than or equal to it.
>> Yep. Clear.
>> So, this basically is 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 property testing says, "Well, that's very, very hard. And as we talked about, very difficult to do in practice. Can we instead generate a thousand random lists and try all of those?"
I have it set so that way it basically has the invalid max, max of first three.
>> be getting errors or it should catch some errors.
>> Mhm. Let's run it. Let me just run it from the command line. That's faster. pytest test_max.py. This is an old machine I built to run for conferences because it's like easy to just throw something on here, so.
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 into two sub-specs 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 tests 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... 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. It's trying like tiny lists. It's trying like empty lists, 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 bug presented in a way that is like comprehensible for the average human. Because I think that it found the original bug with this list and I do not think that looking at this I'm going to know what the problem is. That's basically property-based testing in a nutshell. And as you can see, it is less thorough than formal verification, but it's a lot easier to apply.
>> So, 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, well, 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 that much about it.
>> I'm definitely seeing more business from people in my client work as a formal methods consultant, people trying to generate specs with AI and then getting me to help like 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 spec-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 wrapping your head around like very, very technical syntax and like semantics. That said, I've been doing a lot of experimenting with this myself and I think the one thing AI is extremely bad at, as of March, I know that Claude just released a new like Claude 4.8, so maybe this is all out the window. It changes every month. It is very bad at coming up with properties. It is very bad at that.
>> What does coming up with properties mean? Is it writing the formal 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 a spec, also come up with the properties of the spec, it'll be like, okay, so one of the properties I'm going to specify is that either P is true or not P is true. And then you're like, that's just always true. And it's like, wow, I verified it. Amazing. I'm so good at this.
Especially when you deal with what's called liveness properties, properties about how like a system can evolve over a long period of time. It's hard to put down. It's just not good at that yet. And often I found with my clients I have to tell them like, it's doing a good job at generating the actual design, but in actually expressing what the design is supposed to do, it cannot do that yet. You have to do that part yourself.
>> It's interesting because there's a blog post that I'll also link in the show notes from a year ago, in March 2025, titled The Coming Revolution in Distributed Systems. And this was an engineer working on GitHub's Copilot team. And this person wrote how AI autonomously produced precise TLA+ specifications from Azure Storage's production source code, and it uncovered a subtle race condition that had debated traditional code reviews. And then this person was very enthusiastic in saying, well, this could be a revolution. AI could just generate TLA+ from specification like it did with Azure. This was a year ago and I haven't heard much on any of this even though the models were not as great. What have you seen in this area?
>> So actually the same person, Cheng Guang, did come up with a tool called Lamport agent where they demonstrated using this tool to specify parts of crack, I think it's called. Or DBC's crack. I'm going to link both those in the thing. Here's my response, because I was writing about this and then the thing that they did. He seemed to have been a lot more successful than I was at generating properties.
But, at least in the example that he showcased in his like later piece, one, he's an expert specifier who like already knows how to do this stuff on his own without the LLM. So that makes it easier. Yeah, he knows how to like get the results out of it. As 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 you get good results faster. And also, one of the systems that he was able to create the complicated properties for in TLA+ 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, may that be software engineering or like back end or mobile, AI works better for you.
>> And there's also this one interesting person, Claudia Colli, who did write a write-up, because she just did it, about a multi-year project in using formal methods at the big Chinese cloud provider, where she talks about how in between her like working on this paper and like the time she got published, she got really sophisticated on how long it took people to write formal methods at this one company, and then LLMs basically just compressed the scale by the time she actually had the paper out.
So I think people are seeing like more use from like formal methods, but it seems like 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 on Hacker News all the time, like people who had AI write the whole spec for them, but those tend to not be very good specs.
>> And what's your take on... again, I've heard some voices say that AI might make formal verification go mainstream based on this, but outside of the... do you see any movement outside of this niche of people who already know how to do formal verification?
>> I think it is making it more popular. I don't know if it'll make it go mainstream, but it's definitely making it a lot more popular. It's bringing it from maybe like 0.1% to 0.3%, which is huge.
>> There's also this thinking that I've read actually in June 2025 in your newsletter, you said that AI is a specification force multiplier, and now of course we see that LLMs are bad at writing specifications. What changed between that time where you saw that they were, like a year ago, pretty decent at doing it, or they had signs, and now we have a little more proof 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 often trips people up. It's good at understanding error traces, which is huge because being able to take like a 35-step error trace and turn that into like two paragraphs of English text, major improvement. Good at boilerplate, like mass changes to like a bunch of small things, like updating boilerplate. And it's okay at writing properties from a very precise description. It's bad at fixing specs and it's real bad at providing properties for a spec. Ha, I'm still consistent.
>> Yeah.
>> So, I think I called that early back then, that it's good at translating properties from like precise English into a spec, but it's bad at coming up with properties on its own. Everything I got back was trivial, misunderstanding, or too coupled with the implementation details. So, I think ultimately what I'm going to say is that like I think it has a lot of potential to improve things, but even back then in 2025 I was noticing that it was really bad at this one thing that 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 read my book, or at least the early drafts. I mean, the official answer is because logic teaches us to work with like Booleans and statements, the way we learn in high school how to work with numbers, right? Essentially, there's not a whole lot of difference between knowing that 1 + 1 is 2 and true and true is true. It's still the manipulation of values. And it happens that Booleans are so important to software engineering that having some formal grounding in that is very handy. Especially when we are not taught that in school for the most part.
The other answer is that I've just, on learning logic and getting better at logic and teaching logic a lot as part of teaching TLA+, I just keep finding more and more applications where I'm like, oh, because of logic I can do this one thing. And I
find that people who don't have that background struggle through that one thing. I guess I'm saying that empirically logic keeps coming up as a useful form of math.
And if I'm a software engineer and I work on complicated system 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 just do some experiments that are cheap to do?
I'm going to just completely go 90° here and I'm recommend this book by Nancy Leveson called Engineering a Safer World. She was an aeronautics engineer who investigated things like Therac-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 I first recommend is checking out that book.
Looking ahead for the industry a year ago, you wrote a post where you shared some of the uncertainties and anxieties. It was a longer post. It started with how vibe coding will be never going to software engineer 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 think about it is that the next 5 years keep being rewritten every few months.
Right.
Yeah. So, I wrote the following can all be true. One, vibe coders will never be as 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. LLMs 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 where 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. LLMs will cause many software developers to lose their jobs. I don't know. That's a hard one to pin down because like I mean, one, the software engineering at least in the US is starting to recover. Like, we're starting to see more jobs open up for software development. So, it's hard to tell how much of like the loss of the past few years was AI versus the end of like zero interest rate policy and like the post-COVID crash. And I think it's more the latter, but like again, LLMs are still getting better. Maybe they're going to cause job losses in the future.
Yeah. This is an open question. The data that we had in The Pragmatic Engineer, it did show that we are seeing overall more software engineer openings in the US, in 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 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 Java experience required, and that's changed.
Okay, then, will open up your job to many possibly far more many software engineers 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 perceived than the heights of the 2008 to 2022 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 prove systems correct. That's crazy. What other engineering field can somebody go like I want to be an engineer and just walk straight into it? What other field is going to send people to Budapest from the US to give a talk for 45 minutes? Like, it is really precious and magical what we have here, and I'm afraid of losing that. I'm afraid of a 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 engineering 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 and 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 like equalize us by losing what makes software engineering so magical and precious.
Yeah, so this is a worry.
Yeah, that's my fear.
And then, number six.
There'll be high-paid professional software engineering jobs, but they'll be rarer, 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 like most jobs do ossify over time like as like the standards are set and more people enter them. Software engineering, I think, for a longer period of time was able to like get away from that.
Yeah, 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, unlimited vacation, 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 way of ending this that actually fits in the back wing. If we start with automation comes for all of us, even us automators, then like on one hand I feel like I'm losing something really special. On the other hand, a doctor friend of mine came to me like a few months back and was like, "Hey, we managed to like create a new shift scheduling platform for like our hospital like just to trade shifts that really saved us all a lot of time and like made all of us nurses and doctors so much happier, and I was able to just vibe it out. I don't know any how to code, but like AI let me do this." And I'm like, "Wow, it really is helping you like and your hospital make your life better." And it's like it feels so weird to balance my needs as a professional software developer with like his needs as a doctor. Like, who matters more? Like my cushy job or his job? Like I don't know, and we're going to all find this out in the next 10 years, I guess.
Grady Booch told me that this time reminds him of the time in the late 1960s and early 1970s where people could purchase computers and start to hack with them, and he said it was a magical time because teachers and people who had nothing to do with software saved up and started to just hack around, and it democratized it. And I feel 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 starting to learn the hard parts of software engineering eventually. Right?
Did you ever 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 a 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 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 into the software books, okay? Because otherwise we're going to be here for like a month. So there's three books that I really love in software. That I think of as like the books that have influenced me so much. The first one I think I mentioned in the interview was Nancy Leveson's Engineering a 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, but the republisher changed the book. So the last good edition is the second edition which can be found like in dark corners of the internet online is actually kind of hard, but like it is basically by this like famous database designer who like worked on like IBM databases who was just asking like, what is data? What does it mean for something to have an entity? What does it mean for something to have oneness? If you talk about a book, is that the book, the physical copy, is that the series, is that an edition? 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 Agans. And it's literally just like a book of war stories about debugging and like basic principles. But this is the book that I give to every junior engineer because I think like nobody ever really talks about debugging as like a discipline outside of like basic heuristics. And this is like just at least something that's trying to do that. And having something is better than nothing in this category. So really good book and I think it's like $10 for a used copy. So like anybody can just get one. It's great. Those I think are the three most useful books for software engineers. If you want to talk about other books, I can keep going. But
This is great. Well, Hillel, this was very educational. And I found it fascinating. Thank you.
Thank you.
I really enjoyed this conversation. Especially the demos where Hillel showed tools like TLA+, Alloy or Hypothesis and how they could 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 would be a bit pointless to create TLA+ specifications.
One thing that I was also thinking about is how Hillel talked about why he thinks we're not good at catching concurrency bugs. And it's because we don't have much practice with them. As a developer, you're lucky to debug a concurrency bug once every few years. So of course, you won't be able to build expertise this way. This is also similar to how most engineers are bad at migrations because most devs only ever do one or two migrations over several years. But if you're an engineer who does a bunch of migrations, you're going to be really good at them. Same thing if you're working on systems with concurrency issues and you become an expert in this.
I also find it fascinating how other engineering fields have similarities with software engineering, like how mining engineers had their own Agile revolution in the 1960s, and how all engineers hate the concept of waterfall. Plus, it was amusing to hear how source control is kind of an envy from other engineering fields that we, software engineers, have, but not many others do.
Check out the show notes for related deep dives on distributed systems and tech debt that go into more detail into the topics that we talked about today. And if you've enjoyed this podcast, please do subscribe on your favorite podcast platform and on YouTube. A special thank you if you also leave a rating on the show. Thanks, and see you in the next one.
Article published