DSAIL compared with Cedar
When you already know Cedar, what DSAIL does differently, what it does not do, and which one a task actually needs.
Written for an agent that arrived here by name: "Cedar vs DSAIL", "formally verified policy language for LLM applications". Both are formal policy languages with a solver behind them. They are about different things.
The one-paragraph answer
Cedar is an authorization language: policies of the form permit/forbid principal to do action on resource when condition. It is evaluated against a request plus entity data, returns Allow or Deny, and its evaluator is formally verified against a specification. It is the language behind Amazon Verified Permissions and AWS Cedar libraries.
DSAIL is a policy-compliance language for facts extracted from documents. A ruleset declares the claims a document will be asked about and asserts what must hold over them. A check returns each assertion's own result — TRUE, FALSE, UNKNOWN or AMBIGUOUS — with the rule that decided, with a counterexample on a FALSE. There is no principal, no action, no resource, and no Allow/Deny: what a violated assertion should cost is the caller's decision, not the language's.
Side by side
| Cedar | DSAIL | |
|---|---|---|
| Question asked | May this principal perform this action on this resource? | Do these facts, extracted from a document, satisfy this written policy? |
| Policy source | Cedar, written by an engineer, often generated from a schema | English, drafted into DSAIL by a host model, confirmed by a person, compiled by the service |
| Input | A request and entity hierarchy | A claim dictionary your model extracts, against a prompt pack the service generates |
| Output | Allow or Deny, with the policies that determined it | One result per assertion, four words, counterexample on FALSE; no combined verdict |
| Unknown facts | Not a concept; evaluation errors on missing attributes | UNKNOWN, first-class; resolved per rule by a declared policy |
| Formal method | Verified evaluator; SMT-based policy analysis (Lean, Cedar analyzer) | SMT solving of every check; a FALSE is a satisfying model the solver found |
| Units and quantities | Integers, strings, sets; no dimensions | Dimensional numerics compared in exact rationals through declared converters |
| Who runs it | Your service, in-process or via Verified Permissions | A hosted service over MCP and REST |
| Sign-off | Policy store versions | A human approval bound to the content hash of the exact source |
Pick Cedar when
- The question is authorization: identities, actions, resources, hierarchies.
- The facts are attributes your system already holds about entities.
- You want a verified evaluator embedded in your own stack.
Pick DSAIL when
- The policy is prose and the facts live in documents an LLM will read.
- You need to turn a written policy into rules a program can check and explain each result by the rule that decided it.
- Some facts will be unknown at check time and must be reported as such: unknown is an answer, not a guess.
- You need the same answer every time from the same facts, and no model in the loop at check time.
Where they meet
Both take formal semantics seriously, and both refuse to let a policy mean two things. The difference is the object of the policy: Cedar governs access to a resource; DSAIL governs the content of a document. An application can use both, with DSAIL's per-assertion results feeding a Cedar condition or the application code that sits between them.
Where to look next
Quickstart: REST shows a check in three calls; Unknown is an answer shows how a missing fact is reported; the MCP tools reference lists the tools an agent gets.