The main benefits of Cedar are: *Verifiable/Analyzable *Deterministic Low Latencies *No Security Sandboxing Needed *Ergonomic (easily readable) *Enables parallel execution More here: https://www.youtube.com/watch?t=1798&v=k6pPcnLuOXY&feature=y...

I love the dual implementation, I hadn’t heard of Dafny.

Can you speak to the point about latency? I wasn’t aware it made performance guarantees

OPA allows you to make API calls from it. This doesn't. This makes the latency more deterministic.

Ah, I didn’t realize that. I was thinking in the context of pure policy evaluation. I know rego/opa had a policy performance doc so was curious. Thanks :)

If you're all in on AWS, use it, if not, use OPA. Lots of vendors support OPA/rego, I can't think of anything I use outside of AWS that supports Cedar.

I think that is part of why they open sourced it, to try to get more folks to use it. :)

The challenge with authorization is that mistakes are catastrophic.

The foremost benefit of Cedar is that the implementation is formally proven. Which means that you are extremely unlikely to have to deal with unexpected behavior! Of course, the modeling needs to be reviewed manually for completeness, but the verifier can tell if the model is buggy or inconsistent.