Summary
The Pragmatic Engineer podcast sits down with Hillel Wayne, formal methods consultant and author of “Logic for Programmers,” to examine whether the rise of AI-generated code makes formal verification more or less important — and what “lightweight formal methods” actually means in practice. Wayne, who has taught TLA+ across the industry and is joining Antithesis, argues that full formal verification remains overkill for most software but that property-based testing represents a middle ground most engineers should adopt.
The conversation covers several concrete topics: the famous story of AWS engineers applying TLA+ to DynamoDB and S3, where they discovered a rare but potentially data-losing bug that would likely never have appeared in conventional testing; a live demonstration of a TLA+ model checker finding a concurrency bug in a stick-transfer protocol (Alice offers to both Bob and Carol; Bob accepts after Carol already acquired the stick, violating ownership invariants); and Wayne’s “crossover project” research interviewing traditional engineers to ask whether software engineers qualify as engineers in the classical sense.
On AI specifically, Wayne addresses the popular theory that machine-generated code will finally drive formal methods mainstream — the argument being that when machines write code, humans will need mathematical proof of correctness. His answer is nuanced: AI is particularly bad at the kind of specification thinking that formal methods require, but tools like deterministic simulation testing (which Antithesis uses) offer a practical path to system-level confidence without requiring engineers to write full proofs. The episode is a thorough primer for any developer curious about verification techniques in an AI-assisted coding world.
📺 Source: The Pragmatic Engineer · Published July 29, 2026
🏷️ Format: Podcast
