Cedar
El lenguaje de políticas open source de AWS — más simple que Rego, verificable formalmente con Lean. Impulsa Amazon Verified Permissions.
Sintaxis: permit (principal, action == Action::"view", resource) when { resource.owner == principal };. Tres conceptos: principal/action/resource + condiciones when/unless. AWS lo usa internamente para políticas estilo IAM v2. Verificación formal con Zelkova (basado en SMT) — puedes demostrar que la política A es más estricta que la B. Competidores: OPA/Rego, Casbin, OSO (lenguaje Polar), los especializados SpiceDB/OpenFGA.