Cedar

In short: Cedar decides access; Arxo reasons about norms. Where they meet — an authorization verdict with reasons — Cedar’s single Deny is a deliberate semantic choice, not a missing explanation. This page is for engineers who know Cedar’s permit-and-forbid shape and want the precise boundary with a norms engine.

Key differencesChoosing and combiningEvidence & limitations

What Cedar is for

Cedar is an authorization language with a tiny decision core: permit and forbid policies evaluated over a request of principal, action, resource, and context. Its strengths are deliberate semantics (deny by default, a forbid always wins, several permits can jointly decide), answers that name the deciding policies and computation errors, optional schema validation, and a verification story unusual for the field — a formalized authorizer and validator plus policy-set analysis that answers never-errors, always-allows, subsumption, and equivalence with counterexamples.

Where it meets Arxo

The shared task is authorization verdicts on the same requests and policy sets: explicit forbids, several firing permits, erroneous input — Arxo’s verdict with its witness against Cedar’s decision with its deciding policies. Time and editions of the policy text sit outside Cedar’s purpose and outside this comparison.

Key differences

• A forbid always wins — by design. There is no conflict status analogous to a dual answer; competing permit and forbid resolve to one decision. Do not read that as Cedar failing to explain: the deciding policies are part of the answer.
• “No permit” and “explicit forbid” collapse to one Deny. Only the deciding-policy set differs (empty versus the forbid). An Arxo-side analysis keeps “not permitted” and “prohibited” apart; a comparison must carry that collapse explicitly instead of calling it a mismatch.
• Erroneous policies are skipped with diagnostics, while Arxo blocks a computation on global issues. Different stage, same honesty about bad input — a contract class, not a defect.
• Analysis versus certificate. Cedar’s policy-set analysis and engine proofs are strengths no per-answer certificate replaces; Arxo’s per-answer derivation costs more and proves less about the whole set. Each side’s strength is the other’s honest gap.

A concrete scenario

The prepared experiment runs a static bank of sixteen authorization cases plus four revision cases (punctuation-level edits, entity removal, warning behavior, attribute-presence chains) through the Cedar command line and the Arxo package, comparing decisions with their deciding and witness sets. Cases touching date and decimal extensions are held back until their semantics are confirmed — excluded openly, not silently.

Choosing and combining

Choose Cedar for access control with a small auditable core, schema-checked policies, and set-level analysis. Look to Arxo when the question is normative rather than operational: conflicting grounds that must stay visible, judgment calls, editions, and provenance to the article text. Combined, Cedar enforces the access decision while Arxo holds the normative reasoning that justifies the policy content.

Evidence and open questions

• Sources checked: September 2026 (authorization docs, SDK and example repositories with pinned commits, and the engine formalization paper; command-line flags were read from sources, not executed).
• Studied profile: Cedar language 4.5 with SDK 4.13.0.
• Basis: confirmed by documentation and source reading plus a prepared protocol; comparative run not performed.
• Open: extension-type semantics for the held-back cases, and any claim about current releases beyond the studied pins.

Sources and reproducible materials

• Companion page: Coming from Cedar — the same authorization rules written in Arxo.
• Authorization and policy documentation: docs.cedarpolicy.com
• Engine and examples: github.com/cedar-policy/cedar
• Engine formalization (POPL 2024): popl-24-src-abs.pdf