Releasing Decern: The Proof and the Record

An agent does not borrow your credentials. It exercises your authority.

When you connect an agent to a system, you are not lending it a password. You are handing it a piece of your authority, and it will spend that authority thousands of times, through chains of sub-agents and tools you did not author, at hours when you are not awake to be asked.

That is a different problem from the one authorisation was built for. Access control assumed a person at the other end: someone who decides a few hundred times a day, who can be asked, who stops when the session ends. None of that survives contact with an agent.

Three questions arrive with it, and only the first has a standard answer:

• Did it actually have the authority, all the way down the chain?

• Who is answerable for what it did?

• Can anyone verify that afterwards, without trusting the system that ran it?

The industry has spent this decade standardising how agent authority is represented: tokens, delegation envelopes, decision-request formats, tool manifests. The guarantee is deferred to the implementer. That attenuation actually holds across a handoff. That nothing was dropped from the log. That a decision stayed inside its mandate.

decern is an attempt at the guarantee.

The failure that matters

The interesting agentic failure is not a stolen token. It is a legitimately authorised agent, doing something squarely inside its permissions, that nobody intended.

No authorisation system reads intent, and decern does not claim to. What a kernel can do is narrower and still worth having: bound how far a mistake reaches, make sure the boundary cannot quietly widen as authority passes from hand to hand, and guarantee that when it happens there is a record nobody can edit afterwards.

None of that is achieved by asking the agent nicely. An instruction in a prompt is a request. A refusal in a kernel is a mechanism.

What it is

A small, deterministic authorisation kernel. People, AI agents, and workloads are one principal type, decided by the same pure function, because an agent acting for you should not get a softer code path than you do.

Every decision is written to a tamper-evident ledger before it is returned. The kernel’s safety properties are machine-checked rather than tested on examples.

Two binaries over seven small crates: a proven decision core, an SMT proof harness, a signed ledger, and pure-Rust persistence and primitives.

Apache-2.0. The default build pulls in no TLS stack, no openssl and no cmake, though Cedar’s stacker dependency does compile an assembly routine, so a C toolchain is still required. And it is early enough that the most useful thing you can do with it is break it.

Authority you can prove

An agent chain is where authority quietly grows. You approve an agent; it spawns a helper; the helper calls a tool; three hops later something happens you would not have approved, and every individual step looked reasonable. Attenuation by convention does not survive that. It has to be structural.

Nine properties hold, each stated as exactly what the solver certifies:

• A revoked principal is allowed nothing.

• Nothing is allowed once authority has expired.

• No access without ownership, a delegation ancestor, or an explicit grant.

• No decision crosses a tenant boundary.

• No privileged money action without explicit approval.

• Bounded actions require their named scope; residency, role, and consent conditions bind the rest.

These are not tested examples. A decision that is a pure function of (principal, authority graph, policy, now) is small enough to reason about exhaustively, so the Cedar model is compiled symbolically and cvc5 is asked whether each invariant can be violated anywhere in the modelled domain. Every invariant also ships with a negative control: strip the guarantee out of the policy, and the suite fails unless cvc5 finds the counterexample. A green run is evidence the proofs are load-bearing rather than vacuous.

Where a property depends on a derived attribute, the solver does not certify the derivation. The transitive delegation closure is the main one: cvc5 reasons over the model, and the closure that feeds it is ordinary Rust, covered today by dedicated re-derivation unit tests rather than property-based ones. That is the weakest link in the chain and I would rather name it than let it hide behind the word proven. The solver runs in decern prove and in CI. It is not on the request path.

Missions are what this buys in practice. An approver grants an agent a scoped, fail-closed-attenuated context: these tools, until this time. A Mission whose approved tools exceed what the approver holds, or whose expiry outlives the approver’s own, is refused, and nothing is recorded. A terminated Mission never revives. Because its reference is a pure function of the approval parameters, re-approving an identical terminated grant is refused outright; a fresh grant has to differ in something real.

That is a tool-calling permission that cannot widen, cannot outlive its grant, and cannot be resurrected by replaying the same approval. A tool list, by contrast, is a manifest, not a bound. The registry is local and durable, consulted in-perimeter, with no phone-home.

A record you can verify

A person generates an audit trail a human can read. An agent generates one nobody will ever read, at a rate where post-hoc reconstruction is fiction. The record has to be produced at decision time or it does not exist.

So every decision lands in an append-only, Ed25519-signed, hash-chained ledger, and a decision is served only if its record was written first. If it cannot be recorded, the server returns a 503, never a bare allow. There is no human awake to adjudicate the ambiguous case at machine speed, which is precisely why the ambiguous case must refuse.

Each record carries a derived accountable-owner: the root of the subject’s delegation chain, resolved server-side from the directory rather than read from the request. Three hops down, the record still names the principal ultimately answerable. It is an accountability column, not a gate; it never changes the allow or deny outcome.

Here is a real one, from the run in the quickstart above. The same request, now as it sits on disk.

{
  "entry": {
    "seq": 0,
    "ts_ms": 1785682110000,
    "subject_type": "Principal", "subject_id": "corp",
    "action": "Read",
    "resource_type": "Resource", "resource_id": "claim1",
    "context": { "now": 1785682110 },
    "decision": true,
    "reasons": ["policy0"],
    "sponsor": { "kind": "Principal", "id": "corp" }
  },
  "prev": "0000000000000000000000000000000000000000000000000000000000000000",
  "hash": "8f658ccb5595b7e85a9f020f6a128985929865558c642505e206134337e40e41",
  "sig_b64": "I0DGsmUoYdsk58/yWZCoRJh0zij7pvcUbb9TsJSF8UOfnxmQqWRI+6ultRAXeNBv2Bbz8upBalMg7VwSsTPOAQ==",
  "kid": "d9396c76113e7aa7126b8358063331f9749ece673ddfdbe8b29661bf03714372"
}

sponsor is the accountable-owner. Here corp is a root principal, so it sponsors itself; a delegate three hops down would still name corp. A caller the directory does not recognise gets none. The all-zero prev is the genesis link, hash is what the next entry chains to, and the timestamps come from the server rather than the request.

Read it once more for what is not there. Mission transitions land in the same file under the same contract, so an agent’s whole grant history is as verifiable as the decisions it authorised.

decern verify re-checks the chain offline, and every signature when you pass the key.

$ decern verify --ledger /tmp/decern.jsonl --pubkey d9396c76…4372
OK  3 entries
    root: 0b8a4b21b8e920c5b04e9e9a8849b9a7dd168b021251b702c5d7048122277718
    signatures: verified

Without the key it checks the chain alone and says so, which is a weaker claim than it sounds and not the one that matters. A signature proves a record authentic; the chain proves nothing was dropped from the chain you were handed. Distinguishing that from a different, internally consistent chain shown to someone else needs the head committed somewhere the verifier already trusts. That is what the anchoring work is for, and it is not finished.

This is the witness record The Loop Forgets said we did not have.

What it does not answer

The PDP speaks AuthZEN, so a request looks like this:

{"subject": {"type":"Principal","id":"corp"},
 "action":  {"name":"Read"},
 "resource":{"type":"Resource","id":"claim1"}}

Read it closely. subject is the party asking. The party the decision is about, the one whose claim is being read, appears as a resource or not at all. Go back to the ledger record above and look for a field naming them. There isn’t one. There is a sponsor, and there is a resource_id, and the person sits inside the second of those.

Both of decern’s answers, who held authority and who is answerable, look at the action from the side of the party acting. Neither looks from the side of the party acted upon. Agents act on people at volume, and the person acted upon is the one participant in the whole exchange with no name in the protocol.

That is not a bug I can patch. A kernel can only say what its vocabulary lets it say, and no amount of proof inside my perimeter puts a name in a payload the rest of the industry has already agreed on. That is standards work, and it is the subject of the next letter.

One further limitation, stated here rather than only in the repository: decern’s HTTP endpoints are unauthenticated by design and are meant to sit behind an authenticating proxy. Mission approval in particular takes approver as a request-body field and does not verify it. The accountable-owner on a decision record is derived and trustworthy; the approver on a mission grant is asserted, and is only as good as whatever fronts the service. The default bind is loopback for that reason.

And a closing note, because it is the honest thing to say. A pre-release audit of every claim above found exactly one correctness bug: a terminated Mission could re-register after its own expiry, because the tombstone was evicted at the same moment the grant lapsed. It is fixed, with tests, before this went out.

Where it landed is the interesting part. Not in the proven kernel, which held. In the registry layer just above it, where the solver does not reach. And the ledger recorded every transition throughout, so the record would have shown it happening. One bug, precisely in the gap the proofs do not cover, with the audit trail staying honest across it. That is the whole argument in miniature, and it seemed worth handing you rather than tidying away.

Why I built it

If you have been reading Layer 8 over the past four months, you have already seen the pieces of this argument: delegation, observability, accountability, agent identity, and the records we fail to keep when software acts for us. Every essay ended in the same place, not a conclusion but a to-do. The mechanisms I kept describing did not exist as anything you could run.

This is the smallest honest version of them.

Further reading: Exit Is the Primary Agentic Right, Agentic Observability: Seeing Is Not Stopping, Wrappers, Not Records, The Compiler Forgives. The Loop Forgets., When the Customer Is Software. More at anivar.net/research.

Read it adversarially

The code, the nine invariants and their negative controls, the ledger format, and the limitations are all in the open. Contributions are welcome from people and from agents, under the same rules and the same sign-off, which felt like the only consistent position for a project about agent accountability to take.

→ github.com/anivar/decern
→ decern.anivar.net

Agentic systems will not become trustworthy by becoming more intelligent. They become trustworthy when authority can be bounded, decisions can be verified, and accountability survives automation. decern is an early attempt to make that practical.

Read the code. Read the proofs. Tell me where I am wrong.