The BugBash Podcast Scaling Correctness: Marc Brooker on a Decade of Formal Methods at AWS
Aug 6, 2025
Marc Brooker, Distinguished Engineer at AWS, shares insights from his nearly 17 years of experience building essential cloud services like S3 and Lambda. He reveals how AWS's journey into formal methods transformed software correctness, enhancing both reliability and development speed. The discussion highlights innovative testing strategies, the challenges of applying these methods in complex systems, and the game-changing potential of AI in programming. From the intricate landscape of verification to the tech scene in Cape Town, Marc offers a glimpse into the future of software development.
AI Snips
Chapters
Transcript
Episode notes
Adoptability Drove Formal Methods Shift
- AWS shifted from heavy TLA+ use to lighter, more adoptable formal techniques to increase engineer uptake.
- Making tools and mental models easier drove broader adoption across teams and domains.
Verify The Implementation Directly
- Use code-level formal tools (like Kani or Daphne) to verify the actual implementation and reduce the spec-to-code gap.
- Expect remaining assumptions but gain major bug-elimination benefits by checking real code.
Lower Friction And Show Velocity Wins
- Lower barriers by simplifying tools and matching developers' mental models to increase uptake of formal methods.
- Show teams that upfront correctness work reduces debugging and speeds overall delivery.