Bridging Formal Methods and Software Development

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.