Listen "Scaling Correctness: Marc Brooker on a Decade of Formal Methods at AWS"
Episode Synopsis
How do you prove the correctness of services that underpin a huge portion of the internet? At the scale of Amazon Web Services, traditional testing falls short.In this episode, Antithesis’ own Will Wilson and Ben Collins talk with Marc Brooker, a Distinguished Engineer who has spent nearly 17 years building core AWS infrastructure like S3, Lambda, and Aurora Serverless. Marc gives us the inside story on AWS's decade-long journey with formal methods, from the early days of using complex tools like TLA+ to the current focus on "lightweight" approaches that any engineering team can adopt.He shares the counterintuitive lesson learned at AWS: investing in correctness up front doesn't just improve reliability, it actually boosts development velocity and leads to faster delivery. We also explore the convergent evolution of deterministic simulation testing, the challenge of applying these techniques to user interfaces and control planes , and what role AI will play in the future of programming and verification.
More episodes of the podcast The BugBash Podcast
Ergonomics, reliability, durability
12/11/2025
No actually, you can property test your UI
30/10/2025
Fixing five "two-year" bugs per day
01/10/2025
No really, some bugs aren’t real
18/09/2025
Every map is wrong, but we made one anyway
03/09/2025
Fail loudly, fail fast, fail in production
20/08/2025
FoundationDB: From Idea to Apple Acquisition
23/07/2025
ZARZA We are Zarza, the prestigious firm behind major projects in information technology.