A decade of mathematical certainty: Reflections on the Automated Reasoning Group

In 2016 a small research team at Amazon announced our presence to the world with the launch of the Automated Reasoning Group (ARG). Our vision was bold: use mathematical logic to not just test AWS systems but to prove, with mathematical certainty, that they work correctly. In the intervening decade, we’ve gone from exploring whether advances in formal verification could mitigate previously intractable problems — at AWS scale — to building systems fundamental to how AWS approaches security and reliability. Our group’s production services process billions of queries daily. This is a look back at how we applied cutting-edge formal-verification and program analysis techniques to Amazon's unique challenges. We were motivated by the belief that real-world security and infrastructure problems could be solved with mathematical rigor at AWS scale. After all, tools like the ones we were researching had already proven successful at places like Intel and NASA. What we didn't fully anticipate was…