Cedar policy language is now open source

"We want to assure developers that Cedar’s authorization decisions will be correct. To provide that assurance, we follow a two-part process we call verification-guided development when we’re working on Cedar. First, we use automated reasoning to prove important correctness properties about formal models of Cedar’s components. Second, we use differential random testing to show that the models match the production code."

I'm excited to see you've found a way to bring verification that exists in non-policy-based authorization solutions to Cedar. Was that functionality the driving factor that made the team create something new instead of leveraging the widely adopted Rego/OPA[0] stack for policy?

It looks like this talk[1] briefly covers why you made Cedar, but I'd be eager to hear more about the trade-offs in design, because other policy languages are leveraging decades of formal research on Datalog.

Disclosure: I work on SpiceDB[2], an authorization database inspired by Google's Zanzibar system[3], but I wouldn't say Cedar is directly competitive as SpiceDB is not a policy-based system.

[0]: https://www.openpolicyagent.org/docs/latest/policy-language/

[1]: https://youtu.be/k6pPcnLuOXY?t=2037

[2]: https://github.com/authzed/spicedb

[3]: https://zanzibar.tech

AWS Creates New Policy-Based Access Control Language Cedar - https://news.ycombinator.com/item?id=34865768 - Feb 2023 (83 comments)

Cedar: A New Policy Language - https://news.ycombinator.com/item?id=34449828 - Jan 2023 (3 comments)

The pedigree of Cedar is also really interesting to me, coming from the angle that Torlak was previously part of the UNSAT group @ Washington, and was the developer of Rosette. I was hoping there might be a semantic description of Cedar using Rosette as well! Maybe writing one would be a good challenge...