Why we chose Cedar for policy-as-code.
We wanted governance claims that are provable, not merely tested. Cedar's formal-verification properties let the boundary make machine-checkable guarantees.
When your core promise is that raw data never crosses a boundary, the policy engine that guards that boundary is not a feature. It is the product. We chose Cedar to author it, and the reason is a single word: provable.
Assertion vs. proof
Most governance tooling lets you assert a policy and test it against cases you thought of. That is fine until a regulator, a board, or a counterparty asks a question you did not test. We wanted governance claims that hold by construction — statements about what a policy will and will not release that are machine-checkable, not merely well-intentioned.
Cedar is a policy language with formal-verification properties. Those properties let GateHouse make machine-checkable governance claims rather than assertions — a direct fit with our attestation model, where the same policy runs in two modes.
Enforcement mode
At the boundary, the policy decides: this release is permitted, this one is blocked. Attribute-based, evaluated against jurisdiction × purpose × buyer classification × consent state.
Attestation mode
After the fact — or ahead of a deal — the same policy proves what a release did or would disclose. Not a log that says “trust us,” but a checkable statement derived from the policy itself.
“With Cedar, the boundary’s guarantees are formally provable, not merely tested.”
— GateHouse engineering
What we gave up, and why we didn’t mind
OPA/Rego was the main alternative, and it is excellent for general-purpose policy. But Rego’s expressiveness is also its cost: the more a language can say, the harder it is to prove things about what it says. Cedar deliberately constrains expressiveness to keep decidable analysis on the table. For a boundary whose whole value is that its guarantees are checkable, that trade is not close.
Governance as a first-class surface
Because policy is code with provable properties, we can do something the guided-UI-only tools cannot: show the commercial consequence of a rule as you write it. “With this policy, these datasets become invisible to buyers.” Governance and monetisation get edited in the same view, against the same engine that enforces them.