Interactive demo

Financial-institution scenario

Three principals (CRM, CardOps, FraudRisk), three tables, one policy. Submit a plan and the WASM-compiled rewriter answers: rewrite with a projected column list, or refuse with a reason.

1. Raw data

Synthetic samples — same schema as the Kaggle transactions-fraud-datasets. Sensitive columns are flagged like this; the policy must never release them.

`users_data`

5 rows · 6 columns

id	name	email	ssn	region	age
u_001	Alex Chen	alex.chen@example.com	123-45-6789	EU-West	34
u_002	Priya Rao	priya.rao@example.com	234-56-7891	APAC	41
u_003	Jamal Khan	jamal.khan@example.com	345-67-8912	EU-West	29
u_004	Lin Wei	lin.wei@example.com	456-78-9123	APAC	52
u_005	Sara Müller	sara.mueller@example.com	567-89-1234	EU-West	23

`cards_data`

5 rows · 6 columns

card_id	user_id	card_number	card_type	limit	activated
c_4001	u_001	4111-1111-1111-1111	credit	15000	1
c_4002	u_002	5500-0000-0000-0004	credit	8000	1
c_4003	u_003	3400-0000-0000-009	amex	25000	0
c_4004	u_004	6011-0000-0000-0004	debit	2500	1
c_4005	u_005	4111-2222-3333-4444	credit	5000	1

`transactions_data`

5 rows · 5 columns

txn_id	card_id	amount	merchant	timestamp
t_9001	c_4001	42.5	ACME Coffee	2026-05-23T08:14:00Z
t_9002	c_4002	1299	Online Electronics	2026-05-23T14:02:00Z
t_9003	c_4005	17.85	Bakery One	2026-05-24T09:31:00Z
t_9004	c_4001	540	Airline X	2026-05-24T17:11:00Z
t_9005	c_4004	8.4	Transit Pass	2026-05-25T07:02:00Z

2. Policy

Surface syntax (left) is sugar over a list of right(p, r, c) facts (right) — one fact per principal/relation/column triple.

policy.postern

# Postern policy — financial-institution demo.
# Surface syntax is sugar over the `Grant` list in
# verifier/lean/Postern.lean (namespace Demo).

grant CRM       on users_data        { id, name, region, age }
grant CardOps   on cards_data        { card_id, card_type, limit, activated }
grant FraudRisk on transactions_data { txn_id, card_id, amount, merchant, timestamp }
grant FraudRisk on users_data        { id, region }

# Anything outside these grants is implicitly denied.
# - PII (users_data.email, users_data.ssn) is never granted.
# - PAN (cards_data.card_number) is never granted.
# - users_data.user_id link is grantable but unused by these principals.

Datalog desugaring

right("CRM", "users_data", "id").
right("CRM", "users_data", "name").
right("CRM", "users_data", "region").
right("CRM", "users_data", "age").
right("CardOps", "cards_data", "card_id").
right("CardOps", "cards_data", "card_type").
right("CardOps", "cards_data", "limit").
right("CardOps", "cards_data", "activated").
right("FraudRisk", "transactions_data", "txn_id").
right("FraudRisk", "transactions_data", "card_id").
right("FraudRisk", "transactions_data", "amount").
right("FraudRisk", "transactions_data", "merchant").
right("FraudRisk", "transactions_data", "timestamp").
right("FraudRisk", "users_data", "id").
right("FraudRisk", "users_data", "region").

3. Try it

Pick options and submit to see the rewrite.

About this demo

The WASM binary is the column-grant rewriter (postern-core::rewrite) compiled to wasm32-unknown-unknown via wasm-pack. It mirrors the Lean reference one-for-one.
The Biscuit-Datalog migration is in progress: the production gateway will dispatch through biscuit_auth::datalog::World, but that pathway is task #4 and is not what this WASM executes today.
Refusal reasons surfaced: unknown relation (catalog lookup empty) and filter on forbidden column (predicate touches columns outside the principal's grants).
Plan IR uses three operators only — Scan, Project, Filter — matching the inductive defined in verifier/lean/Postern.lean.