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