cardano-keri

cardano-keri projects a rotating KERI identity into a stable Cardano checkpoint.

Play the design before you read it

The accepted design is a proved Lean machine, and the two simulations below are transcriptions of it, checked against the Lean by replay on every step. Pick a story and play it; every refusal names the rule that refused.

The checkpoint simulator — one identity, its keys, its three sums of money, the hunters (anyone paid to land a rotation, or to freeze a checkpoint whose pool cannot pay), the treasury: fifteen stories with their forks, the theorems lighting up as you play.
The registry simulator — one incarnation per identity: requests, batches, the gating plugin, the leaf every identity has.

KERI is Key Event Receipt Infrastructure, the identity protocol used by the Global Legal Entity Identifier Foundation's verifiable LEI ecosystem. A KERI AID (Autonomic Identifier) keeps its identity while its controller keys rotate. Cardano applications can refer to the AID-derived checkpoint token instead of permanently binding themselves to one key.

How to read these pages

The project is mid-way through adopting the accepted design: a design settled in September 2026 that keeps the checkpoint, adds a poison (the owner's own lock on the checkpoint) and a registry (one leaf per identity), and removes the enforcement economy that main still carries. Older issues and the wiki call this design the M1 return: the return, inside the first milestone, from an abandoned enforcement economy to a checkpoint that only projects key state. So every claim in these docs is in one of three states, and each page says which one it is making:

State	What it means	Where it lives
Shipped on `main` today	Code you can run, or a program published on preprod	`onchain/`, `offchain/`, `deploy/preprod/m1-manifest.json`
Accepted design	Proved in Lean and playable in the simulator; no on-chain code yet	`lean/CardanoKeri/Checkpoint.lean`, 87 theorems in `CheckpointGoals.lean`, no `sorry`
Planned	An epic with an issue number and an acceptance criterion	the roadmap

Nothing here that is only designed is described as if it were deployed.

Shipped on `main` today

Six applied programs are published as reference scripts on Cardano preprod: five from deploy/preprod/m1-manifest.json (published 2026-07-28 from commit 50a5820) and the endpoint board from deploy/preprod/board-manifest.json (published 2026-07-29 from commit 95b554f):

Program	Role	Size
`hash-proof`	minting policy	9,233 B
`observer-lifecycle`	withdrawal observer	6,523 B
`observer-advance`	withdrawal observer	16,130 B
`observer-enforcement`	withdrawal observer	14,417 B
`checkpoint-register`	validator and minting policy	11,512 B
`endpoint-board`	the witness endpoint board	3,158 B

Deployment parameters: registration bond 1,000 tADA, freeze bond 5 tADA, freeze window 10,000 slots.

The checkpoint datum is pure key state — nine fields, no lifecycle flag: the AID, current keys and threshold, next-key commitments and next threshold, witnesses and toad, the Cardano sequence, and the native KERI sequence (onchain/lib/cardano_keri/checkpoint/datum.ak). Enforcement state is carried by role addresses around the same token.

The packaged ckeri exposes deploy, manifest verify, register, advance, close, status, list, checkpoint, payer, and the five board verbs. It does not expose freeze, claim, or convict: those transactions exist only in the end-to-end harness.

The transaction path does not require cardano-cli

The packaged ckeri can deploy the reference scripts, register an identity, advance a rotation, post/update/retire endpoint-board records, and close a checkpoint on a machine with no cardano-cli installed at all. Its runtime closure does not include cardano-cli; a closure check enforces that boundary and has been demonstrated to fail when the retired dependency is reintroduced.

Current evidence

Settled on preprod on 2026-08-06 with a genuine KLI identity: registration 6ecc2e07…, advance f0f3a18f…, close 446f0d83…. Earlier, on a protocol-11 development network running production transaction limits, a two-key identity settled Register, Close, Advance, and two Freeze/response rounds. Dates, transaction IDs and their sources are on the story ladder. Separately, a witnessed 2-of-5 KLI identity has registered and advanced its live V1 checkpoint on preprod; see Rotate your identity.

Not a production deployment

Settled development-network and preprod transactions prove the vertical path through the production validators and the node boundary. They do not make this a mainnet service. Claim/thaw, conviction, real three-of-seven scale, full vLEI credentials, and wallet integration still have open stories.

The accepted design

The design settled between 2026-09-02 and 2026-09-03 (project rulings D-022 to D-040). It is proved in lean/CardanoKeri/Checkpoint.lean — 87 theorems in CheckpointGoals.lean, no sorry, standard axioms only — and the simulator above is a transcription of that Lean, checked by replay.

One UTxO per identity, holding the current key state, a token minted once and never again, and three sums of money that never mix:

D_reg, the conviction bond — the stake a duplicity proof seizes. Never a fee source.
B, the freeze bond — what a hunter takes when the pool cannot pay for a rotation.
the pool — advance funds; pays the premium P, the fee for landing a rotation, to whoever lands it.

No owner exit, no withdraw. An identity is active (live, poisoned or frozen), in pending conviction custody, or convicted (terminal after the associated Registry fold). The owner keeps it alive until it is convicted: there is no close, no parking and no revival. A rotation is the only thing that moves the keys; it carries a bond option (keep or deposit). deposit is the unfreeze: it refills B when a hunter has taken it, and it is signed by the keys of the epoch the rotation opens (D-038) — so a relayer landing a public rotation can never unfreeze the owner. The refund address is chosen by whoever pays the registration and no step ever changes it.

flowchart TB
    start(( )) --> Absent["<b>Absent</b><br/>register — registry insert, once ever"]
    Absent -->|register| Active["<b>Active</b><br/>rotate — next keys + toad receipts, clears the poison<br/>poison — current quorum, once per epoch<br/>freeze — anyone, when the pool is short<br/>deposit — next keys refill B (the unfreeze)<br/>top-up — anyone"]
    Active -->|duplicity proof| Pending["<b>Pending conviction</b><br/>retained custody#59; no local exit"]
    Pending -->|associated consuming Registry fold| Convicted["<b>Convicted</b><br/>token burned#59; registry key permanently retired"]

The poison is the piece that is genuinely new: a declaration signed by the current keys at their own threshold, over a short preimage bound to the policy, the AID and the sequence. Anyone may relay it; it is never witnessed. It makes the checkpoint unconsumable, and any witnessed rotation clears it — it belongs to the epoch of the keys that signed it, because in KERI possession of the next keys is control. It buys the owner the window between noticing a theft and rotating.

The registry maps each AID to absent, active or permanently retired. A live carrier and pending conviction custody keep the key active. Only the associated consuming fold retires it. The registry uses the public model from singular, where it runs on a development network; see where the registry is built.

There is no leaving. A checkpoint ends only by conviction. The current keys keep exactly one Cardano power, the poison; everything else answers to the next keys, never the current ones. What happens to the bonds and pool of an owner who stops maintaining a checkpoint is an open economic question, left visible rather than answered.

The consumer's rule, and the only thing outside the machine: authorize iff the checkpoint is present, both bonds are full, it is not poisoned, it is older than the juvenility window W (the age a checkpoint must reach before a consumer trusts it), and the payment's own signature satisfies the current threshold. Everything else fails closed.

What the accepted design removes

The record tree and its cursor, occupancy maps, the MPF fork and its upstream proposal, ever_duplicitous, and the whole ARMED/FROZEN enforcement economy — freeze-for-lag, the bounty, the entitlement, and the reaping of a paused checkpoint after a grace period; the owner's close and parking are removed as well. Interaction events (ixn) never touch the chain. Delegated identities are a later milestone.

The freeze that survives is a different thing: it is what a hunter takes when the owner's pool has run dry, not a punishment for lag.

What is planned

The accepted design is one milestone across two repositories, thirteen epics. The roadmap carries the ordering, the dependencies and the measurements that size the numbers still open. The short version: slim main (#319), measure it (#321), build the owner's edges (#322) and the hunter's (#323), integrate the registry (#324), put every role behind a ckeri command (#325), replay the fifteen stories as the acceptance suite (#326), and cut over preprod (#328).

Start here

Why Cardano — how this differs from anchoring a KEL on a ledger, and what non-oracular trust buys.
Story ladder — what has actually settled, dated.
Roadmap — the plan for the accepted design and its thirteen epics.
KERI primer — AIDs, key events, pre-rotation, witnesses, and Veridian.
The KERI specification — KERI 1.1 as published by the Trust over IP working group; every story page links the clause it relies on, at the version the watcher conformance review pins.
The constitution — the rules every contributor works under; since 2026-09-11 the accepted Lean model is the behavioral authority, and a model error is escalated as a user story and fixed in the Lean before any code moves.
Identity operations — the operations, one by one, shipped and designed.
Observer architecture — thin checkpoints, reference scripts, zero-lovelace withdrawals, and the BLAKE3 premint fact token.
Register — Alice's identity appears on Cardano.
Rotate — Alice rotates, Hal lands it.
Poison — Mallory steals the current keys.
No owner exit — a checkpoint is alive until it is convicted.
Hunters — the pool, the freeze, two hunters racing.
Consumer checklist — the treasury reads the checkpoint.
ACDC primer — the separate credential layer.

For the financial and institutional concepts behind the later use cases, see the Finance primer.

The engineering constraint

observer-advance measures 16,130 bytes against a 16,133-byte applied-script limit — three bytes of headroom. The accepted design's datum change lands on exactly that script, which is why epic #319 ends with a size table and epic #322's datum decisions are taken from it rather than from taste. Two things move in the plan's favour: the advance observer's ARMED-response branch goes, and the three enforcement role addresses go from checkpoint_register. The net effect is unmeasured until #319.

Full measurements are in Observer architecture.

Real-world direction: vLEI

The longer-term goal is to let Cardano applications combine:

a current, consumable AID checkpoint;
an ACDC credential chain proving a legal or organizational role; and
current TEL non-revocation evidence.

Registering an AID answers "which keys control this identifier?" It does not answer "which legal entity is this?" The latter is a credential claim and remains a later roadmap layer. See the vLEI design and the roadmap.