In this AWS re:Inforce 2024 session, Lucas Wagner and Sean McLaughlin discuss how AWS used automated reasoning to prove the correctness of their new authorization engine. They explain the process of building, proving, and validating the engine, which handles one billion API calls per second. The speakers detail how they used the Dafny programming language to create specifications and proofs, and how they validated the new engine against quadrillions of production authorizations. The talk highlights the benefits of this approach, including a 65% performance improvement and increased confidence in making future changes. The session concludes by introducing Cedar, a proven-correct authorization language, and Amazon Verified Permissions, which customers can use for their own applications.