# 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](../quickstart/rest.md) shows a check in three calls;
[Unknown is an answer](../guides/unknown-is-an-answer.md) shows how a missing
fact is reported; the [MCP tools reference](../reference/mcp-tools.md) lists the
tools an agent gets.