Automated reasoning has revolutionized how AWS demonstrates the security of our controls. We call this provable security, where automated reasoning tools apply mathematical logic to help answer critical questions about your infrastructure. You will learn how AWS has used automated reasoning to prove the security properties of AWS access controls, namely IAM authorization. In addition, this session will share the capabilities and services AWS built for you to verify your own security posture. For example, AWS has used provable security techniques in the development of Cedar, an open source policy language, which is now available to use in your custom applications through Amazon Verified Permissions.