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
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.
Inner-Loop Testing Multiplies Velocity
- Deterministic simulation testing (DST) raises developer velocity by surfacing distributed bugs early in the inner loop.
- Finding bugs in the IDE or build cycle is far cheaper than discovering them later in integration or production.
Convergent Evolution Of DST At AWS
- Several AWS teams independently evolved distributed simulation and deterministic testing around the same time.
- Alvaro's early S3/ALF work influenced wider adoption across storage teams.