# Formal methods with Hillel Wayne

Page: https://stenobird.com/podcast/the-pragmatic-engineer-7019833/formal-methods-with-hillel-wayne
Text version: https://stenobird.com/podcast/the-pragmatic-engineer-7019833/formal-methods-with-hillel-wayne.md
Podcast: [The Pragmatic Engineer](https://stenobird.com/podcast/the-pragmatic-engineer-7019833)
Published: 2026-07-29T16:22:31+00:00
Episode link: https://newsletter.pragmaticengineer.com/p/formal-methods-with-hillel-wayne
Audio file: https://api.substack.com/feed/podcast/208490793/f31ef801d61096f61c3c947eedfb56d2.mp3
Processing state: not_requested
JSON: https://stenobird.com/v1/public/podcasts/the-pragmatic-engineer-7019833/episodes/formal-methods-with-hillel-wayne
Duration seconds: 5022

## Resource

Brought to You By: • Antithesis – verify your system’s correctness without human review or traditional integration tests – and avoid bugs or outages. • turbopuffer – a vector and full-text search engine built on object storage. It’s fast, cheap, and extremely scalable. • WorkOS – everything you need to make your app enterprise ready. — There’s a popular theory that AI will finally make formal verification mainstream because mathematical proof of correctness will be needed when machines write most or all of the code. But will this happen? Today, I’m talking with one of the best people to tackle the prediction. Hillel Wayne is a formal methods consultant, educator, and author, who’s deeply interested in software history. In this episode of Pragmatic Engineer podcast, I sit down with Hillel to compare software engineering with traditional engineering, discuss where formal methods fit into modern software development, and we explore why they are essential for some of the world's most complex systems. We cover the formal specification language, TLA+, walk through several formal verification tools, examine why distributed systems are so difficult to reason about, and look into whether AI will make formal methods accessible to more engineering teams. — Timestamps 00:00 Intro 03:21 The Crossover Project 10:26 What software engineering does better 14:19 What traditional engineering does better 17:06 Formal methods 28:21 TLA+: what it is and demo 35:47 TLA+ at Amazon 36:59 Ways distributed systems break 39:52 Formal methods and systems thinking 45:09 The value of learning math 49:12 What TLA+ is good for and isn’t 51:39 Alloy: a declarative language for software modeling 57:42 Other formal methods tools 1:00:13 Property-based testing 1:04:20 AI and the need for formal verificati…

## Actions

- request_transcript: `POST https://stenobird.com/v1/public/podcasts/the-pragmatic-engineer-7019833/episodes/formal-methods-with-hillel-wayne/transcription-requests` — Idempotently request low-priority transcript generation for this episode.
- read_markdown: `GET https://stenobird.com/podcast/the-pragmatic-engineer-7019833/formal-methods-with-hillel-wayne.md` — Read the agent-friendly Markdown representation of this episode resource.

A page view does not enqueue transcription. Agents should invoke `request_transcript` explicitly when they need this episode processed.

## Transcript

Full transcripts are not published on public pages unless there is a clear rights basis.