Scaling Correctness: Marc Brooker on a Decade of Formal Methods at AWS

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, we talk with Marc Brooker, a senior 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—powerful techniques for verifying software correctness. 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.