Cedar Verifies Who Can Access What. Who Verifies What Decision Gets Made?

Amazon's Cedar does something almost no policy tool does. It does not only evaluate your policies. It lets you prove things about them.

That is a real engineering result, and it landed in authorization first for reasons that make sense once you look at the shape of the problem. But it leaves a question sitting directly next to it, and nobody in the rule engine market has answered that one.

Authorization is one kind of decision. The discount applied to an order, the eligibility check on a loan application, the fraud threshold that blocks a transfer, the tier gate on a feature — those are decisions too, and they are the ones that change every week.

Who proves anything about those?

This post is about that gap: what Cedar verifies and how, why business decision rules are a harder verification target than access policies, and where LexQ stands on it. The short version of that last part is that LexQ stands on the problem statement, not on the solution.

What Cedar actually proves

Cedar is Amazon's open-source authorization policy language, and the language behind Amazon Verified Permissions. A policy reads roughly like this:

permit (
  principal in Group::"engineering",
  action == Action::"viewDocument",
  resource in Folder::"internal"
) when {
  resource.classification != "restricted"
};

The syntax is not the interesting part. What matters is what the Cedar team built underneath it. Cedar's semantics are modeled in Lean, a proof assistant, and properties of the language itself are established as machine-checked proofs rather than as test suites. Around that sits automated reasoning tooling that answers questions about whole policy sets: whether one version is equivalent to another, whether a change made access strictly more permissive, whether a given policy can ever grant access at all.

Those are not questions a test suite answers. A test tells you about the inputs someone wrote down. A solver tells you about every input in the space, including the ones nobody thought to write down.

So Cedar is formal verification inside a shipping commercial product, aimed at a real operational concern, used by engineers who are not researchers. That deserves to be stated plainly before anything else here, because the rest of this post is about a place Cedar does not go.

Access and outcome are different questions

An authorization decision has a small, well-behaved shape. Principal, action, resource, and context go in — one bit comes out. Allow or deny. You can pile attribute conditions onto a policy and the output stays one bit. Composition is fixed by the language rather than by the policy author, so in Cedar an explicit forbid overrides any permit, and the absence of a permit means deny.

A business decision does not have that shape. Ask what discount applies to this order and the answer is not a bit. It is a value, and it is produced by rules that read facts, write facts, and then read what earlier rules wrote.

In LexQ a rule does one of three things: set a fact, mutate one arithmetically, or block the decision outright. Rules evaluate in priority order within a version, which means a rule that mutates cartTotal changes the input every rule below it sees. Mutex groups constrain which rules in a set may fire together, either exclusively or up to a cap of N. A rule with an empty condition is a catch-all that always applies.

Stack those and what comes out is not a verdict. It is a set of values, the order in which they were produced, and a record of what each step overwrote. I wrote earlier that a Decision Operations Platform is not authorization, and that policy-as-code tools like OPA and Cedar decide access rather than business outcomes. That was one sentence doing a lot of work, and this is the part of it that got the least space.

That makes the verification target different too

For access policies, the object you reason about is a boolean function over attributes. Still hard, but it sits in a fragment that SMT solvers handle comfortably: booleans, sets, string equality, integer comparison.

Business decision rules drag in everything else. Arithmetic that goes beyond comparison, because rules multiply, subtract, and cap. Ordering, because priority means rule 7 evaluates against a world that rule 3 already edited, so the formula has to model state at each step instead of one static set of conditions. Cross-rule constraints, because a mutex group is a statement about combinations of rules rather than about any rule on its own. Accumulation, because when three rules each shave a percentage off the same fact, the real question is what the composition can reach at its extremes.

The questions worth asking change too. Not "can this principal ever get access", but:

• Unreachable rules. Can this rule's condition ever be true, given everything above it in priority order?
• Conflicts. Are there inputs where two rules both fire and write the same fact with different values?
• Gaps. Is there a region of the input space where nothing fires and the fact is never set at all?
• Runaway composition. Is there an input where stacked mutations push a value past a bound nobody intended?

Every one of those is a claim about all possible inputs. That is precisely the class of question a solver answers and a test suite cannot, and why sampling inputs structurally cannot settle them is the other half of this argument.

The part where LexQ is the follower

I want this on the record before any positioning: on formal verification, LexQ is behind. Cedar productized it. LexQ has not productized anything of the kind. If verified authorization policy is what your evaluation needs, Cedar is the answer, and I would rather say so than win a paragraph by talking around it.

What is also true is that the move Cedar made for authorization has not been made for business decisions by anyone. I went looking through the commercial rule engine market for it, and the number of engines that ship formal verification over a rule set is zero. Not weaker variants of it. Zero. The comparison teams actually run between those engines is about hosting model, operations, and cost. None of them are compared on what they can prove, because there is nothing to compare.

So the position splits cleanly. On the technique, LexQ is a follower. On the domain, the ground is unclaimed.

Cedar verifies who can access what. LexQ verifies what decision will be made.

I am not going to let the tense in that second sentence do work it has not earned. It states what the two problems are, not what two products do today. There is no verification engine in LexQ. Nothing described in this section runs anywhere. The name for the work is LexQ Verify, and what exists under that name right now is a problem statement, a design direction, and this post.

The design direction, since a name without a shape is just marketing: a compiler that translates LexQ rule conditions into first-order logic formulas for the Z3 SMT solver, then asks the solver about conflicts, gaps, and unreachable regions across the entire input space. The output I have in mind has roughly this shape. Read it as a sketch of an interface, not a screenshot of one:

✅ No unreachable rules
⚠️  2 potential conflicts:
   "vip-discount" ∧ "loyalty-bonus"
   → Resolved by mutex group "promo-exclusive"
❌ 1 gap:
   tier=STANDARD, cartTotal < 5000 is uncovered

Why has nobody built this for decision rules? Not because the idea is obscure. Engineers with real SMT solver experience are rare, and a compiler from a rule condition DSL down to SMT formulas is an academic-grade design problem — not a feature ticket. I would rather name that difficulty than let a design sketch pass itself off as a product.

What LexQ has today, and what it does not

Here is the line, in one paragraph, because this is the part that decides whether anything else here is worth trusting. LexQ can tell you what happened and what would have happened. LexQ cannot tell you what could ever happen.

Everything on the first side of that line exists and runs. Impact Simulation replays a rule version against real historical production traffic and shows the outcomes it would have produced. Decision Replay re-runs a specific past decision and diffs it against another version, so the rule that changed the answer is visible rather than inferred. Every execution carries a decision trace: which rule fired, on which inputs, at which version, and why the others did not. Per-rule latency profiling shows where evaluation time goes. Versions are managed and reversible, and every decision lands on an immutable audit ledger. Testing a change against real traffic before it ships and proving after the fact which rule produced a given outcome each have their own post.

All of that is empirical. Every one of those tools answers a question about inputs that actually occurred.

Formal verification answers a different class of question: one about all possible inputs, including the ones your traffic has never produced. A gap in your rule set that no customer has hit is invisible to simulation by construction, because simulation can only replay what happened. That is why I do not describe simulation as verification and do not intend to start. Testing produces evidence. Proof is a different object. LexQ has the first one — and only the first one.

When you don't need any of this

Formal verification of decision rules is not a universal need, and neither is LexQ.

• Your rule set is small and stable. Six rules that have not changed in a year do not need a solver. Read them. At that size, reading is the proof procedure.
• Your actual problem is access control. If the question is who can do what to which resource, that is a boolean policy problem with mature tools built specifically for it, and Cedar or OPA will serve you better than a Decision Operations Platform will.
• Your rules cannot overlap by construction. A single lookup table where exactly one row matches has no conflicts to find, and no gaps that the table does not already show you.
• Nobody ever asks you why. If no decision your system makes is disputed, audited, or reconstructed months later, the whole lifecycle around decisions is machinery you will not use.

And the one that matters most in this post: nobody needs LexQ Verify today, because it does not exist. If formal verification is a live requirement in your evaluation, LexQ does not meet it. Saying that costs me a line in a blog post. Not saying it would cost considerably more.

LexQ is a Decision Operations Platform: business decisions live as versioned rules outside application code, get tested against real production traffic before they ship, and carry a full trace afterward.

The reason to write this before there is a feature to announce is that the question deserves a name regardless of who ends up answering it. Cedar's team showed that formal verification of a policy language is tractable and worth productizing, and they showed it for access. The decisions that set prices, clear transfers, approve claims, and gate features are bigger, messier, and by comparison completely unexamined. Cedar answered the question for access. For business decisions it is still open, and an open question nobody is naming stays open longer.

→ See what LexQ does today — start free at lexq.io