Descriptions:
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.
—
Brought to you by:
• Antithesis – verify your system’s correctness without human review or traditional integration tests – and avoid bugs or outages https://antithesis.com/pragmatic
• turbopuffer – a vector and full-text search engine built on object storage. It’s fast, cheap, and extremely scalable https://turbopuffer.com/pragmatic
• WorkOS – everything you need to make your app enterprise ready https://workos.com/
—
*The Pragmatic Engineer deepdives relevant for this episode:*
• How to debug large, distributed systems: Antithesis https://newsletter.pragmaticengineer.com/p/antithesis
• How AWS S3 is built https://newsletter.pragmaticengineer.com/p/how-aws-s3-is-built
• Paying down tech debt https://newsletter.pragmaticengineer.com/p/paying-down-tech-debt
• How Big Tech does quality assurance (QA) https://newsletter.pragmaticengineer.com/p/how-big-tech-does-qa
• Bug management that works https://newsletter.pragmaticengineer.com/p/bug-management-that-works-part-1
• Resiliency in distributed systems https://newsletter.pragmaticengineer.com/p/resiliency-in-distributed-systems
—
*Where to find Hillel Wayne:*
• LinkedIn: linkedin.com/in/hillel-wayne
• Newsletter: https://buttondown.com/hillelwayne
• Website: https://www.hillelwayne.com
—
*In this episode, we cover:*
00:00 Intro
04:32 The Crossover Project
11:37 What software engineering does better
15:30 What traditional engineering does better
18:17 Formal methods
29:32 TLA+: what it is and demo
36:58 TLA+ at Amazon
38:10 Ways distributed systems break
41:03 Formal methods and systems thinking
46:20 The value of learning math
50:23 What TLA+ is good for and isn’t
52:50 Alloy: a declarative language for software modeling
58:53 Other formal methods tools
1:01:24 Property-based testing
1:05:31 AI and the need for formal verification
1:12:29 Logic for programmers
1:14:35 Hillel’s 2025 prediction on AI’s impact
1:21:30 Book recommendation
—
See the transcript and other references from the episode at https://newsletter.pragmaticengineer.com/podcast
—
Production and marketing by https://penname.co/.
