Overview of Formal methods with Hillel Wayne
Gergely Orosz talks with formal methods consultant Hillel Wayne about how software engineering compares to traditional engineering, what formal methods actually are, where tools like TLA+ and Alloy shine, and whether AI will make formal verification mainstream. The episode combines practical examples, a live-style demo of model checking, and a broader discussion of engineering culture, concurrency bugs, property-based testing, and the limits of AI-generated specs.
Key themes and takeaways
-
Software engineering and traditional engineering have more in common than many people think.
- Across fields, engineers optimize for the same tension: how expensive mistakes are vs. how quickly you can iterate.
- “Waterfall” is widely disliked in almost every engineering discipline.
- Software is unusual in how fast it can iterate and how consistent its materials are.
-
Software has several unique advantages over other engineering fields.
- Open source and freely shared knowledge are unusually common.
- Version control is far more mature than change-management tools in other industries.
- Software engineers can often test and deploy much faster than civil, chemical, or mechanical engineers.
-
Traditional engineering can still teach software a lot.
- Other disciplines are generally better at up-front planning and compiling deep reference material.
- Hillel uses examples like the 500-page snap-fit handbook to show how software lacks similarly rich domain-specific references.
- Software could benefit from stronger planning habits without losing its iteration speed.
Hillel Wayne’s background and “Are software engineers real engineers?”
- Hillel originally wanted to study physics and math, but realized programming was the part he enjoyed most.
- He became a developer, then moved into formal verification / formal methods.
- In his “crossover project,” he interviewed engineers across multiple traditional fields to ask whether software engineers count as “real engineers.”
- His conclusion:
- He moved from “probably not” to “probably yes”.
- The comparison became even more interesting once he looked beyond bridges and civil engineering to electrical, chemical, mining, and industrial engineering.
What formal methods are
Hillel explains formal methods as a way to make your implicit understanding of a program explicit and mathematically checkable:
- Specification: define what the system should do.
- Verification: prove or check that the implementation matches the spec.
- Proof / model checking: use mathematics or automated tools to show correctness across all possible inputs or states.
Simple example: max(list)
- Instead of writing a handful of tests, formal methods ask:
- What is the precise definition of “maximum”?
- Can we express that as a property?
- Can we prove the function satisfies it for all lists?
Why formal methods are hard to use everywhere
Formal methods are powerful, but often impractical for ordinary business logic because:
- Real-world systems are full of edge cases and context.
- Writing a complete spec can become as hard as writing the program itself.
- For most systems, a good implementation that works 99%+ of the time is enough.
- Trying to fully model the whole real world can become a nightmare of assumptions:
- file permissions
- symlinks
- filesystem semantics
- concurrent changes
- time-of-check/time-of-use issues
Where formal methods are actually used
Hillel explains that formal methods are best for highly technical, high-cost failure domains, especially where concurrency and state transitions matter.
Common use cases
- Distributed systems
- Databases
- Cryptographic primitives
- Operating system components
- Firmware
- Safety-critical systems
Examples mentioned
- Parts of AWS DynamoDB and S3 were modeled with TLA+.
- The model found a deep bug in Amazon’s replication system; the shortest trace in the paper reportedly took 35 high-level steps to reproduce.
- Formal verification has been used in parts of:
- operating system kernels
- HTTPS/security stacks
- microkernels like seL4
- train transponder systems
- firmware and device kernels
TLA+: the main tool discussed
TLA+ (Temporal Logic of Actions) is presented as the main practical language for modeling distributed systems.
What it does
- Describes a system as a state machine
- Enumerates possible states and transitions
- Uses model checking to explore behavior and catch bugs
Why it matters
- It exposes bugs caused by interleavings, race conditions, and unexpected sequences of events.
- It is especially useful when:
- multiple processes act concurrently
- exact order matters
- bugs are rare but catastrophic
Demo takeaway
Hillel shows a simplified trading-system model where a bug appears because:
- one person offers an item to Bob
- then offers it to Carol
- Carol accepts
- Bob later accepts the earlier offer
- the item transfers in a way that violates the intended invariant
This illustrates how formal models can reveal bugs that are hard for humans to reason about manually.
The most common distributed-systems bug: TOCTOU
Hillel emphasizes time-of-check / time-of-use bugs as a recurring pattern:
- You check that something is valid.
- By the time you act, the world has changed.
- This is common in:
- bank transfers
- authorization
- concurrency
- payment systems
- exactly-once delivery problems
He also notes that exactly-once delivery is very hard in distributed systems, and many systems settle for easier guarantees like at-least-once delivery plus compensating logic.
Alloy and other formal tools
Hillel also demonstrates Alloy, which is better suited for analyzing static data models and access-control structures.
Alloy example
- A resource hierarchy had a bug where:
- a user could read a parent resource
- and therefore its child
- but not necessarily the grandchild
- The issue was that the access rule was not transitive
Why Alloy is different
- Alloy can translate models into SAT problems
- SAT solvers often find counterexamples very quickly
- It is typically faster and more lightweight than brute-force model checking with TLA+
Property-based testing as a middle ground
Hillel strongly recommends property-based testing as a more accessible option for many engineers.
How it works
Instead of handpicking a few tests, you define properties like:
- the result of
max(list)must be an element of the list - it must be greater than or equal to all others
Then the tool generates many randomized inputs and tries to break the property.
Why it’s useful
- It finds edge cases you wouldn’t think of
- It shrinks failing examples to minimal counterexamples
- It is much easier to adopt than full formal verification
Bottom line
- Formal methods: strongest correctness guarantees, but expensive and niche
- Property-based testing: easier to use, very practical, and a strong default for many teams
AI and formal methods: helpful, but not a silver bullet
The episode’s central AI question is whether LLMs will make formal verification mainstream.
Hillel’s view
- AI is good at some supporting tasks
- It is bad at inventing meaningful properties
- It can help with:
- syntax cleanup
- boilerplate
- translating precise English into specs
- summarizing long error traces
- It struggles with:
- coming up with the right invariants
- liveness properties
- original specification design
Main conclusion
- AI can be a specification force multiplier
- But it does not remove the need for human understanding
- The strongest results still come from people who already know how to specify systems well
How formal methods change the way engineers think
Hillel argues that formal methods help engineers build intuition through fast feedback:
- When modeling concurrency, you can see race conditions immediately.
- This gives people more practice with failure modes they rarely see in production.
- It makes distributed-systems bugs feel more concrete and visceral.
He compares it to:
- learning refactoring through repetition
- learning migrations by doing many of them
- learning debugging as a discipline
Hillel’s broader view on math in programming
He argues that software engineers do need math, but not necessarily the math many people think of first.
Important math for programmers
- counting
- boolean logic
- graphs
- directed graphs
- matrices
- set theory
- formal logic
- discrete math
His point
- Traditional engineering leans heavily on continuous math
- Software leans more on discrete math
- Many developers don’t recognize the math they use because it isn’t the math they were taught most prominently
Books Hillel recommends
1. Engineering a Safer World — Nancy Leveson
- A major influence on systems thinking and accident analysis
- Focuses on why complex systems fail
2. Data and Reality — Bill Kent
- A deep book about what data really is
- Explores identity, representation, and how data models relate to reality
3. Debugging: The 9 Indispensable Rules — David Agans
- Practical debugging wisdom
- A good book for junior engineers
Final thoughts on AI and the future of software work
Hillel expresses mixed feelings about AI:
- It can democratize software creation
- It can help professionals work much faster
- It may also reduce the special advantages software engineers have enjoyed
His concerns
- Software engineering may become more like other white-collar professions:
- fewer exceptional salaries
- less bargaining power
- more competition
- more standardization
His hope
- AI will also let more non-engineers build useful tools
- It may enable more “situated software” for families, teams, clinics, schools, and small communities
Main takeaway
The episode argues that formal methods are powerful but specialized. They are best for systems where failures are costly and the state space is complex, especially in distributed and concurrent systems. For most day-to-day engineering, property-based testing and better system thinking are more practical. AI may help accelerate specification work, but it does not eliminate the need for engineers who understand how to define correctness in the first place.