Today, AWS open-sourced the Cedar policy language and authorization engine. You can use Cedar to express fine-grained permissions as easy-to-understand policies enforced in your applications, and you can decouple access control from your application logic. Cedar supports common authorization models such as role-based access control and attribute-based access control. It follows a new verification-guided development process to give you high assurance of Cedar’s correctness and security: AWS formally models Cedar’s authorization engine and other tools, proves safety and correctness properties about them using automated reasoning, and rigorously tests that the model matches the Rust implementation.