▶ YouTube Summaries

• https://www.youtube.com/watch?v=KSkcgIYQy0U
• Original title: Formal methods with Hillel Wayne

Gergely Orosz interviews Hillel Wayne — formal methods consultant, TLA+ teacher, author of Logic for Programmers, soon joining Antithesis — on whether AI-written code will finally push formal verification mainstream. Spoiler stated up front: full formal methods are overkill for that, but lightweight formal methods and property-based testing are genuinely useful. Along the way: the Crossover Project comparing software to traditional engineering, live TLA+ and Alloy demos, and where LLMs actually help and fail in specification work.

Names are ASR-mangled in the transcript; corrected here where confident.

The Crossover Project — are software engineers really engineers?

Wayne started firmly in the "we are not engineers" camp, then read Glenn Vanderburg's talk arguing the practices look similar, disbelieved it, and went to check by interviewing ~15–20 people who had worked in both traditional engineering and software, across six or seven disciplines (civil, electrical, chemical, industrial, mining). They agreed with Vanderburg. He now says "we probably are" engineers, with the caveat that the work predates LLMs, which have likely changed the calculus on both sides.

Findings:

• Everybody hates waterfall. The core tension in all engineering is cost of a mistake versus speed of iteration — expensive mistakes force more up-front planning, but every field still hunts for ways to iterate (scale models, simulation, CAD, fab turnaround). A mining engineer told him his field had its agile revolution around 1960 with the New Austrian Tunnelling Method: change fast, watch how the rock reacts, correct.
• Software iterates fastest by a wide margin — chemical engineers considered "run it overnight, results tomorrow" fast; software presses F11.
• Software is far more consistent than other materials. A resistor spec sheet promises ±20% within a temperature range; the same program sorts the same list identically on any machine. The variability software deals with is largely self-inflicted (API and platform diversity), not material variance.
• Open source and practitioner conferences are close to unique to software. Other fields have academic conferences and vendor trade shows, but not the third kind where practitioners meet to get better. Wayne's speculation: our material and our product are the same thing, which makes sharing natural. He wonders whether 3D printing (where the unit of value is the schematic) shows the same pattern.
• Version control: all ~20 interviewees named it as the thing they wished their old field had. Other fields have change management, but "comparing a modern car to a Model T."
• What we could learn: we plan worse than other fields because we can get away with it, and we are worse at compiling body-of-knowledge references about our own materials. His example — an engineer's two favorite books were The Design of Everyday Things and a 500-page handbook on snap fits (the clicky plastic catch on a remote's battery cover). Software's equivalent would be a 500-page book on how to version an API, which does not exist.

What formal methods actually are

Take max(list). You write five to eight tests and check the answers against knowledge you can't articulate. Step one of formal methods is making that implicit knowledge explicit: the max of a list is an element of the list such that every other element is smaller. That statement is the specification. Tests verify it at individual points; types verify a shape; formal methods use mathematical proof to show it holds for every possible input. In practice the proof transformations are largely automated by tools — you supply extra facts when the prover gets stuck, like using a calculator instead of doing arithmetic by hand.

Why not do this everywhere? Because for real domain problems, merely writing down what the function should do becomes a nightmare. Orosz's example of "find the file in a directory with the most lines" immediately runs into: ASCII or UTF-8 newlines, unreadable files, symlinks, directories, filesystem semantics. The imperative version that's right 99% of the time is good enough almost always. Chasing 100% here is premature optimization.

Where the return does justify the cost, Wayne splits the landscape into three categories:

1. The "nukes and NASA" story — and from firsthand experience, nuclear plants don't actually care; thorough testing suffices for them.
2. Small, critical cores verified while the rest stays informal: parts of databases, cryptographic primitives (Firefox's HTTPS stack via Project Everest), OS kernel pieces (Microsoft verified driver-loading parts of the Vista kernel; seL4 is an end-to-end verified microkernel in Isabelle, used in automotive and military — verified against its specification, which is a real caveat).
3. His own work: don't verify the real system, build a simplified model and verify that. Bugs can still exist in the implementation, but design-level bugs get ironed out before they're built. Mostly databases and distributed systems, plus device-firmware verification and, memorably, verifying train transponders (which turned up a very old bug).

TLA+ demo

TLA+ (Temporal Logic of Actions) was created by Leslie Lamport — also the author of LaTeX — in 1994 to model distributed systems. It represents a system's state machine and brute-force model-checks every reachable state against stated properties, including liveness and refinement.

The demo models a trading platform: items owned by people, a set of outstanding offers, actions to propose/accept/reject, and an invariant that ownership only changes when the new owner accepted an offer from the old owner. The checker finds a violation in 53 states. Alice owns a stick and offers it to Bob. Bob is away; Alice gets impatient and also offers to Carol, who accepts — the stick is now Carol's. Bob comes back, sees the stale offer, clicks accept, and the stick transfers from Carol to Bob without Carol ever offering it. The invariant breaks.

Notes from the demo:

• The syntax is a real learning curve — Lamport was writing as a mathematician. Later languages (Quint, P) look more like programming languages. TLA+ persists largely because of the 2014 AWS paper.
• Full state spaces run to ~100 million states; the graph visualization is a demo toy, not a working tool.

AWS and TLA+

The seminal 2014 paper "Use of Formal Methods at Amazon Web Services": a couple of engineers learned TLA+ and PlusCal (which compiles to TLA+) and applied them to parts of DynamoDB and S3. They found complex bugs that could lose data, in replication. The shortest error trace exhibiting one bug was 35 high-level steps — a depth no human review would plausibly reach. Wayne's speculation is that the state space was ~100 million states wide, with plenty of safe 70–80-step chains, and that one 35-step path happened to be invalid.

Distributed systems: the recurring bug

Beyond race conditions and locking, the pattern that keeps coming back is time-of-check-to-time-of-use: you validate something, then act on it later — a microsecond or a day — and it stopped being valid in between. The illustrative example is checking a $10 balance, someone else draining the account, then deducting anyway into negative.

Orosz relates it to Uber's payment system: exactly-once message delivery is very hard, at-least-once is much easier, and you build exactly-once on top of at-least-once. The tangent on hotels authorizing a larger amount up front is framed as an engineering-risk decision — avoid the edge case where you need a second authorization and the credit limit is gone.

Why concurrency is hard — and why formal methods change how people think

Wayne's answer is not that humans are bad at concurrency in principle: crossing a street is concurrent reasoning. He cites a "common sense computing" paper where restating a threading problem as clerks at a ticket office assigning concert seats let students spot the bug much faster. The real problem is practice: in production you hit a race condition, find out months later, ship a fix, and learn weeks after that whether it worked. In TLA+ the loop is a button click — race condition, fix, timeout bug, fix. That feedback rate is what builds the skill. He notices it himself: on a new client's system he doesn't understand the domain, but once the model exists he sees the bug faster than they do, purely from reps.

Orosz's analogy: engineers are bad at migrations because most only do one or two in a career; those who've done five can do them with their eyes closed.

On math for programmers

Some math is so useful we forget it is math (counting, comparison). Some is specialist-only (most programmers never need calculus). Broadly useful branches: graphs and directed graphs, matrices, formal logic. His recommendation is exposure to what exists across fields rather than depth in all of them — you need to know what's available to know what's useful.

A structural observation: traditional engineering runs on continuous math (calculus, differential equations), which is what advanced high school teaches. Software runs on discrete math — combinatorics, graph theory, formal logic, set theory — which most people are never exposed to early. That mismatch may be why programmers think math isn't useful in their work.

When TLA+ fits, and when it doesn't

• Best in highly computational, technically-bounded domains (node replication between datasets), poorly in business-embedded, human-behavior domains ("make sure our sprints don't run over" — he's modeled it, got some value, it was hard).
• TLA+ handles discrete distributed systems with concurrency and eventual-behavior challenges. No floating point, no decimals, no probabilistic reasoning. It answers "can this happen at all", not "does this happen 1% of the time".
• If iteration is cheap and bugs aren't costly, this tooling wastes your time. Wayne is emphatic about saying so, because skepticism toward formal methods largely comes from people burned by CASE and UML being forced on them as miracle solutions.

Alloy demo and other tools

Alloy (from an MIT professor) is a different lineage, good at static structures — data structures, data models, domain models — with real interest in the domain-driven design community. The demo models resources with optional parents, an acyclic constraint, read access granted directly or via parent, and a property that read access flows to children. Alloy produces a visual counterexample: a user can read a parent and its child, but not the grandchild, because readableBy is not transitive. Formal methods find the violation; they don't pick the fix — you might close the relation transitively, or discover your DBA won't allow a transitive SQL query and need a different fix.

Fun fact from the demo: Alloy compiles models into boolean satisfiability problems and uses a SAT solver (SAT4J). SAT is NP-complete in theory but fast in practice, so most Alloy models check in milliseconds, while a large TLA+ model may churn overnight through 100 million states.

Other tools mentioned:

• P — Microsoft Research origin, author later at Amazon; interacting state machines passing messages, actor-model flavored, more accessible than TLA+.
• Quint — grew out of an alternative TLA+ model checker into its own language; traction in banking and smart contracts.
• PRISM — probabilistic model checker; can say "this bug happens 10% of the time", but academic and laborious to translate into. Wayne wrote a two-part series using PRISM to prove the dreidel game isn't fun.
• Event-B (used in part of the Paris Metro), mCRL2, UPPAAL (robotic control, mostly academic), NuSMV (used at NASA).
• For verifying actual code rather than abstract models: Dafny, JML for Java, Frama-C for C, Ada SPARK, and proof assistants Coq, Lean, Isabelle.

Property-based testing as the practical middle ground

Same specification as formal methods — the max is in the list, and everything else is ≤ it — but instead of proving it for all lists, generate a thousand random lists and try them. The demo runs three max variants (correct, max-of-first-three, max-of-absolute-value) against a Hypothesis-style property test in Python; the broken one fails on [0,0,0,0,1].

The property worth noticing: the framework tries edge cases first (huge, tiny, empty lists), then shrinks a failing input to the minimal interesting example — so you get a bug report a human can actually read, not the original 40-element list. Less thorough than verification, far easier to apply. Wayne's own recommendation: formal methods are niche, property-based testing is broadly useful, and stopping there is fine for most people.

AI and formal verification — the actual answer

Wayne is seeing more business, more spec generation attempts, more papers, and more property-based testing (Amazon's Kiro advertises generated property tests as a headline feature). What LLMs are good at, consistent with what he wrote in June 2025:

• Fixing syntax errors — big, because syntax is what trips beginners.
• Explaining error traces — turning a 35-step trace into two paragraphs of English is a major improvement.
• Boilerplate and bulk mechanical edits.
• Translating a precise English description of a property into spec syntax.

What they remain bad at, as of his testing this March:

• Coming up with properties on their own. Ask for properties of a spec and you get trivialities — "either P or not P is true" — followed by self-congratulation. Liveness properties (how a system evolves over time) are worse still.
• Fixing specs.

His framing to clients: the model does a good job generating the design, but expressing what the design is supposed to do is still your job.

On the widely-cited March 2025 post "The Coming Revolution in Distributed Systems" — a GitHub Copilot engineer had AI derive TLA+ specifications from Azure Storage production source and surface a subtle race condition that survived code review. The same author later built a "Lamport agent" tool. Wayne's caveats: that author is already an expert specifier (the general pattern that AI amplifies people who could already get good results), and one of the systems already had a sophisticated P spec available, which may have done much of the work. A separate multi-year formal-methods project at a large Chinese cloud provider found that between writing the paper and publishing it, LLMs had compressed the time cost substantially.

Verdict: AI is making formal methods more popular, not mainstream — "from maybe 0.1% to 0.3%. Which is huge." And you still need the basics yourself, if only to tell when the model is wrong.

Logic for Programmers, and the closing predictions

Why formal logic is the most useful piece for day-to-day work: logic is to booleans what elementary arithmetic is to numbers, booleans are central to software, and almost nobody is taught to manipulate them formally.

Asked what to adopt for hardening distributed systems, Wayne goes sideways and recommends Nancy Leveson's Engineering a Safer World — she investigated Therac-25 and Columbia, and her writing on how accidents emerge from complex systems is the better starting point.

Revisiting his six-part prediction from a year ago:

1. Vibe coders will never be as good as experienced engineers — probably true.
2. LLMs significantly augment professional engineers — true; deep-knowledge engineers who drive the tools get a lot done.
3. LLMs will cost many developers their jobs — unclear. US software hiring is recovering, so much of the recent loss may be the end of ZIRP and the post-COVID crash rather than AI. Pragmatic Engineer data shows openings up in the US, slightly down in Germany and France, with the shape shifting: AI engineering spreading, front-end and mobile hiring declining. (Compare: twenty years ago the in-demand engineer was specifically a Java engineer.)
4. They'll also open up new jobs — true in the sense that if one developer can build the product instead of five, you still hire that one.
5. The new jobs will pay less than the 2008–2022 peak — this is the one that scares him. He walked out of physics into a well-paid job and now proves systems correct for a living; no other engineering field lets you do that, or flies you to Budapest to talk for 45 minutes. The fear is software becoming an ordinary white-collar job with two weeks of vacation. Both agree software engineers have enormous privilege relative to other engineering fields, and he'd rather everyone got it than lose it for parity.
6. High-paid jobs will persist but be rarer and more competitive — already visible; he compares it to trading, where fewer, still highly paid, harder to enter.

The closing tension: a doctor friend vibe-coded a shift-swapping tool that made his hospital's nurses and doctors materially happier, knowing no code at all. Weighing a cushy software job against that is genuinely hard. Orosz relays Grady Booch's comparison to the late-60s/early-70s moment when individuals could buy computers and hack. Wayne points to Clay Shirky's essay "Situated Software": most software should serve three people, a family, one school — until now that required someone in that group to be deeply into computers, and now it doesn't.

Book recommendations

• Nancy Leveson, Engineering a Safer World — believed to be free online.
• Bill Kent, Data and Reality — second edition only; the 2011 republisher altered the book. A database designer asking what data even is, what identity and oneness mean. Ends on: data isn't reality, it's our view of reality for a useful purpose.
• David Agans, Debugging: The Nine Indispensable Rules — war stories and basic principles; the book he gives every junior engineer, because debugging is almost never taught as a discipline. Roughly $10 used.

Orosz's takeaway

Formal verification probably won't go mainstream even with AI — the tools are too rigid for the real world, useful for mathematically modelable parts like state spaces and pointless for everyday programs. The concurrency point stuck with him: developers are bad at race conditions because they hit one every few years, the same reason most engineers are bad at migrations.