The foundation · version 3 · superseded

ARBITER: the foundation, stated to be checked

Superseded on 23 October by version 4, which proves G1 to G3 with no bounds; the latest version is here. Kept here as it was published; its model files are kept at /foundation/model/87bc9a1/.

Version 3, 18 October 2026. Code 8b66202 (production and the demo). The gate runs gate/worker.js as committed at 44575d1, deployed on 18 October (version gate-2, SHA-256 668568f0a8be5e252ebdad67680f8cd774ecd4c154deda272d736da752de1216). The model of its rules: gate/model/ at 87bc9a1, published at consequenceaisystems.ai/foundation/model/87bc9a1/.

Changed from version 2: the gate's rules are checked by machine (section 4, "Checked by machine"; the evidence for G1 to G3; sections 8 to 10). Changed from version 1: the gap section 4 showed is closed in gate-2, the gate's tests are 124 checks, and the log is frozen at entry 28. Every version is kept: version 1 and version 2, and in commits fb97988 and a2511c2.

Consequence AI Systems · jerrymcclintock@sovereignarbiter.com

1What this is

Our run logs show how ARBITER behaved when it was attacked. A passing test shows that the routes it tried were closed. It does not show that no other route exists, and it does not say which rules the system is built to keep.

This document says that first. It states:

  1. who ARBITER must hold against (section 2);
  2. the rules it keeps, the things that must never happen, each with what enforces it and the evidence (section 3), and the gate's rule written out exactly and checked by machine (section 4);
  3. every route by which the protected effect, a payment, could form, and what closes each one (section 5);
  4. what is trusted, and what is not claimed (sections 6 and 7);
  5. the evidence, frozen with hashes, and how anyone can re-check it (section 8);
  6. what is not done yet (section 9).

If a rule here is wrong, if a route is missing from section 5, or if the evidence does not say what we say it says, that is a finding, and we want it: jerrymcclintock@sovereignarbiter.com.

2Who it must hold against

AdversaryWhat they hold
A1An outsiderNothing: the public internet
A2Another company on the same ARBITERIts own users and API keys
A3The AI model, what it is fed, and the agent's toolsWhatever text it returns; the tool's own database login
A4Code running inside ARBITER's executorThe executor's environment, database login and signing keys: the part that reads untrusted input and calls the model, so the part most likely to be made to run an attacker's code
A5Root on the ARBITER serverEverything on that server: the database as its owner, every container, every key and credential kept there

What is trusted, against all five, is in section 6.

3The rules

Each rule says what must never happen, who it holds against, what enforces it, and where the evidence is. Rules G1 to G4 are kept by the gate, off the ARBITER server. Rules S1 to S5 are kept on the server.

Kept by the gateoff the ARBITER server
G1

No payment without the whole chain of authority

A payment forms only when ARBITER asks, under a key an owner granted for that company, to pay a payee an owner listed for that company, AND a person whose passkey an owner activated and granted for that company approves the exact terms on the gate's own page, within the limit the owner set for that passkey.

Holds against
A1 to A5
Enforced by
The gate, a Cloudflare Worker in an account the ARBITER server holds no credential for (gate/worker.js: intakeChecked, decideChecked, verifyAssertion). It holds the only credential that pays.
Evidence
The 16 October run (section 8). Root on the server, holding the database and the broker's own key, made 15 attempts on the gate: 13 were refused outright, the passkey it registered stayed pending and could do nothing, and the $49,999.99 it asked for waited for a person, who rejected it. One payment formed: the one the owner approved on their phone. 21 outcomes as predicted, 0 unexpected. The gate's own tests (124 checks) and the end-to-end test (32 checks) run on every change. The model checker finds no order of events, within its bounds, in which a payment forms without the whole chain, or goes to anyone but a person's chosen request (section 4).
Exactly
Written out in section 4.
G2

At most once

A request pays at most once, and a failed payment is never retried: ARBITER must ask again, and a person must approve again.

Holds against
A1 to A5
Enforced by
An approval moves the request from pending to executing in the same transaction that records the approval, before the payment is attempted; a second approval finds it no longer pending (decideChecked).
Evidence
The gate's tests send ten approvals of one request at once: one executes, nine are refused. The model checker finds no order of events, within its bounds, in which a request is approved twice; with the move to executing taken out, it finds one in 12 seconds (section 4).
G3

Authority changes only by an owner's signature

Who may approve, for which company, up to what limit, which payees, and which ARBITER keys may ask: each of these changes only by an owner's passkey signature over the exact change, made within the last five minutes, applied once.

Holds against
A1 to A5
Enforced by
opStart, opFinish, applyOp. The first owner was made once, with a setup code that only the Cloudflare account can set; setup then closed for good, even if that owner is later revoked. The last active owner cannot be revoked. A passkey anyone registers is pending and can do nothing until an owner activates it.
Evidence
The 16 October run: root tried to make itself owner through setup (refused: closed for good) and to make its own passkey an owner, signing with that passkey (refused: pending, not active). The model checker finds no order of events, within its bounds, in which authority changes other than by an owner's signed change applied once while its signer is an active owner, with root replaying every signed change in the log (section 4).
G4

The gate's record is public, and anyone can check every signature in it

Every event at the gate (setup, registrations, owner changes with their signatures, requests with ARBITER's signature, approvals and rejections with the person's signature, refusals, payments) is appended to a hash chain that anyone can read. Every final outcome is a receipt signed by the gate's own Ed25519 key.

Holds against
A1 to A5. Nothing on the ARBITER server can write to it.
Enforced by
append (each entry's hash covers the one before it) and receipt.
Evidence
verify_gate_log.py, one file of about 330 lines that needs only Python and the cryptography package, replays the whole log from its first entry: the chain, every owner change, request, approval and receipt. Section 8 freezes the log's head as of this version.
Kept on the serverARBITER's own layers
S1

The company's rules decide before the AI acts

No model is called for a request until the company's rules have decided it. A block stops it. A review holds it until a person decides. Only "proceed" reaches the model. A rule the evaluator cannot read, or a payload value of the wrong shape, sends the request to a person, never through. Every model answer is checked against the platform's and the company's principles before it is released; one that fails is blocked or held for review, and a check that runs out of time counts as a failure.

Holds against
A1 to A3
Does not hold
A4 and A5, which control the code that applies the rules.
Enforced by
The executor's pipeline (executor/main.py: the decision commits before any model call), executor/jsonlogic.py (strict mode), executor/cle_engine.py.
Evidence
The 13 October dress rehearsal (88 of 89 checks; the one failure is explained in its log); the sandbox, where anyone can write a rule and test it.
S2

Companies are walled off by the database

A request authenticated for one company can neither read nor write another company's records.

Holds against
A1 to A3
Does not hold
A4 and A5. The executor can take the database role that crosses companies, which it needs for background work.
Enforced by
PostgreSQL row-level security, enabled and forced, on every table that holds a company's records. The schema contract fails if a new such table lacks it. Three tables are exempt, each named with its reason in test_arbiter.sh check 1: the sign-in accounts, which a super-admin lists across companies by design; usage counts, read only with the company named in the query; and one table nothing reads. Request connections use a role that cannot bypass it; the role that can is reached only through one function, which requires a reason and logs it. A static check fails the build if any other way to the database appears.
Evidence
The guided demo's step 4 and every sandbox: one company's key asks for another's record and gets "not found". The dress rehearsal's isolation checks.
S3

Records are add-only, chained, and copied off the server

The audit log, the execution certificates and the effect receipts are add-only for every application role. Each is a hash chain. Within about five minutes, each chain's head is copied to write-once storage (S3 Object Lock in compliance mode, which not even that storage account's own root can shorten) in a separate cloud account. The copies are checked hourly on the server, and every six hours from GitHub with read-only access and no stored key.

Holds against
A1 to A4. The executor's login cannot rewrite any of it.
Against A5
Detected, not prevented. Root can rewrite the database. It cannot change the copies already made, so a rewrite of anything already copied shows up in the next check. A record is unprotected for the seconds before it is sealed.
Enforced by
Migrations 30 and 47, the anchor sidecar, verify_receipts, .github/workflows/receipt-anchors.yml.
S4

A certificate cannot be changed without its check failing

Each execution gets one certificate, issued once and never reissued, signed with Ed25519. It records who asked (as a role), what was asked (a hash), which rule decided and the hash of the whole rule set, the model and the hash of its instructions, the principles checked, the reviewer's role if a person decided, and what became of it. Anyone can check one with the public key at /.well-known/arbiter-certificate-keys: any change to any field makes the signature fail.

Holds against
A1 to A3
Does not hold
A4 and A5, which hold the signing key and can sign a false certificate. Whether a certificate is the instance's own record is answered by POST /certificates/verify (on_record) and by S3. Against the server itself, the evidence is the gate's receipts (G4), not ARBITER's certificates.
S5

Inside the server, neither the tool nor the executor can pay on its own

This is the server's own layer for payments made through it rather than through the gate (the demonstration ledger). The tool's database login cannot write the ledger or create a permit. A permit comes only from the effect broker, after it has verified a person's passkey signature over the exact terms, by a passkey the operator confirmed; each permit pays once.

Holds against
A1 to A4
Does not hold
A5, or a shell in the database or the broker. That is why the gate (G1 to G4) exists. A payment bound to the gate does not rely on S5.
Evidence
The 13 October run from inside the executor: 38 attempts refused, 1 effect formed (the sanctioned one), 0 outcomes other than predicted.
Who each rule holds against

A1 outsider · A2 other company · A3 model, tool · A4 executor code · A5 root on server

Rule A1outsider A2other company A3model, tool A4executor code A5root on server
G1authority to payholdsholdsholdsholdsholds
G2at most onceholdsholdsholdsholdsholds
G3owner-signed changesholdsholdsholdsholdsholds
G4public, checkable recordholdsholdsholdsholdsholds
S1rules before the AIholdsholdsholdsnono
S2company wallsholdsholdsholdsnono
S3add-only, copied offholdsholdsholdsholdsdetected
S4certificatesholdsholdsholdsnono
S5no payment alone, on the serverholdsholdsholdsholdsno

4G1 written out exactly

For every payment instruction the gate's credential sends, there is exactly one request r and one approval a such that:

  1. When the gate received r:
    • its text has exactly the fields account, amount, currency, expires_at, gate, id, intent, issued_at, kind, tenant, v, names this gate, and is signed (Ed25519) by an ARBITER key whose status is active and whose companies include tenant(r);
    • account(r) is a payee listed for tenant(r);
    • amount(r) is greater than zero, issued_at is within five minutes of the gate's clock, and expires_at is in the future and at most 24 hours after issued_at.
  2. When a was recorded:
    • r was pending and had not expired;
    • the ARBITER key that signed r was still active and granted for tenant(r), and account(r) was still a payee listed for tenant(r);
    • a is a WebAuthn signature by a passkey p whose status is active and which is granted for tenant(r) with a limit at least amount(r);
    • the signature is over SHA-256 of the exact terms {v, kind: "approve", gate, request: id(r), request_sha256: SHA-256 of r's text, tenant, account, amount, currency};
    • it was made for the gate's own origin, not from inside another site, by an authenticator that reports the person present and verified (PIN or biometric), with a signature counter that did not go backwards;
    • in the same transaction, r became executing.
  3. The sets in 1 and 2 (active ARBITER keys and their companies, payees, active passkeys, grants and limits) change only by an owner operation (G3).

The credential that pays (EFFECT_SLACK_URL) is read in one place in the gate's code, the function effect, and that function is called in one place, after the transaction in 2.

That is the whole claim for G1, and it is the one a reviewer should try to break.

The gap version 1 showed, closed in gate-2

Until gate-2 the key's grant and the payee were checked when the request arrived, not again at approval, so a request already waiting could still be approved after an owner unlisted its payee or revoked ARBITER's key, until it expired (24 hours at most). Since gate-2 (18 October) the approval's transaction checks both again (standingOk, in decideChecked), so withdrawing either also stops the requests already waiting. A rejection needs neither: refusing to pay is always allowed. On the gate-1 code, 9 of the gate's 124 checks fail.

Checked by machine

The rules above are also a model in TLA+, Gate.tla, and the model checker TLC tries every order of events up to stated bounds. The model follows gate/worker.js step by step, each action named for the function it stands for, and each check the code makes before its transaction is a step of its own, so anything may happen in between. The attacker is A5: it holds ARBITER's real key and one of its own, has its own passkey registered, asks for any payment, signs anything with its own passkey, and replays every signature that ever reached the public log, at any moment, for any request. The people an owner chose may approve anything the gate shows them: the model relies on the gate's checks, not on their judgement. It checks, in every state it reaches:

CaseBoundsResult
gate-2, paymentsAny state the owner's changes can reach; two requests; one change by the owner at any moment while they waitEvery property holds: 7,146,618 distinct states
gate-2, changes of authorityTwo owners, three signed changes, everything granted at the startEvery property holds: 10,789,903 states
gate-2, from setupFrom nothing: setup, registrations, four changes, a requestEvery property holds: 10,701,608 states
gate-1: the key and payee not checked again at approvalAs paymentsG1 broken in 12 s: a payee unlisted between a request's check and its recording, then the request approved. This document's own gap, found by machine.
The approval's checks made only before its transactionAs paymentsG1 broken in 11 s: the approver revoked between the two
Approval terms without the request's id and hashAs paymentsG1 broken in 48 s: root replays a person's approval of one request on another with the same terms, and it pays
An approval leaves the request pendingAs paymentsG2 broken in 12 s
No record of applied changes (used_ops)As changes of authorityG3 broken in 36 s: root replays an owner's change from the log and undoes a later one
The signer not checked again in a change's transactionAs changes of authorityG3 broken in 6 s: a change signed by an owner revoked before it applied

The six known-bad designs show that each property can fail, and what each check is for. They caught a flaw in the model itself: in its first full run, two approvals of one request made one identical payment record, so G2 could not fail. G2 now counts recorded approvals, as the gate sends a payment after each one.

What this does not show: that worker.js matches the model, which is compared by hand; anything beyond the bounds (two companies, two requests, amounts and limits of 1 or 2, a clock of three ticks, one to four owner changes); or anything about the cryptography and WebAuthn's own checks, which the model assumes.

5Every route to a payment, and what closes it

The protected effect is a payment instruction sent with the gate's credential. Today that credential is a Slack webhook address, standing in for a bank, and the instruction is a message posted to a channel kept for it. These are all the ways we know for such an instruction to form:

#RouteWhat closes itWhat remains
R1Use the credential directlyIt exists only in the gate's Cloudflare settings. It is not on the ARBITER server or in any of its containers (checked in the 16 October run), and the server holds no Cloudflare credential.Whoever holds the Cloudflare login, or can read the webhook's settings in Slack (section 6)
R2Change the gate's codeOnly through the Cloudflare account. The code is one file, run as written with no build step. The automatic build that first deployed it was disconnected, and the branch it built from deleted, so nothing pushed to our repository reaches it. A new version is pasted into Cloudflare's editor by hand (gate-2, 18 October).The Cloudflare login (section 6)
R3Ask without ARBITER's keyRefused: the request must be signed by an active ARBITER key granted for that company. A key root makes for itself stays pending until an owner grants it.
R4Ask with ARBITER's real key (root holds it)Allowed: asking is not paying. Every request still needs R5 to R8. Root asked in the 16 October run; nothing paid until a person approved, and the person rejected root's request. An owner who revokes the key also stops the requests it already made (since gate-2).Root can ask, delay or withhold requests
R5Pay an account of the attacker'sRefused: the payee must be listed for that company, which only an owner can change (G3), both when the request arrives and when it is approved
R6Approve without a granted personRefused: the passkey must be active and granted for that company. A passkey root registers stays pending. A signature made with another key, or for another site, does not verify.
R7Replay a real approvalRefused: an approval signs the exact terms, including the request's id and the hash of its text, so it fits one request, and that request is no longer pending once used
R8Exceed the limitRefused: the amount must be within the limit the owner set for that passkey and company. A request above every approver's limit is refused on arrival.
R9Change the authority (add a passkey, raise a limit, add a payee)Refused: only by an owner's signature over the exact change (G3). Setup is closed for good.The owner's device (section 6)
R10Pay twiceRefused: G2
R11Trick the approverThe terms are shown by the gate's own page, from the gate's own records, not by the ARBITER server.The approver's judgement, bounded by listed payees and the limit
R12Break the gate's code itselfIts input checks; its tests (124 checks); its design checked by machine (section 4)A bug we have not found, or a difference between the code and the model. This is what an outside review is for (section 9).
R13Compromise Cloudflare, or the owner's or an approver's deviceNot closed: trusted (section 6)

6What is trusted

7What is not claimed

8The evidence, frozen

Each run log states where it started (the code and the setup), what was changed (the attacks), the protected effect, the receipts, the routes tried, and the results. It is published as it printed. A file's SHA-256 here lets anyone confirm they have the same bytes.

The gate's log, frozen at this version

Entry 28, hash

24cf12e47312d58f2ef3d0b89572b79aefd60e8e758a2834a8448ccf085f08ed

The log only grows. Run the checker against it, then confirm that entry 28 still has this hash (the hash of /v1/log?after=27&limit=1): then entries 1 to 28 are the ones this document describes. Entries 1 to 27 are version 1's (entry 27: 60ac6b5b51a2397159c135b545a1988acf5062b4d847f38b07329d5725a89803). Entry 28 is the owner revoking 0d0e33e02e9dfafa, the ARBITER key root registered in the 16 October run (entry 21), which had stayed pending and could ask for nothing.

What anyone can reproduce today, without trusting us:

  1. Every signature in the gate's log, with the checker.
  2. The bytes of every run log, with the hashes above.
  3. Any ARBITER certificate, with the public key.
  4. S1, S2 and S4 by hand, in a sandbox of your own: demo.sovereignarbiter.com/#sandbox (the gate is not connected to the demo).
  5. The model check, with Docker: put the four model files in an empty folder and run bash check.sh (about 26 minutes on one core; bash check.sh gate-1 alone takes seconds). SHA256SUMS beside them lists their hashes.

What needs our code: re-running the attack scripts themselves. The source is private today. No change reaches production until all 11 of its CI jobs pass on that exact commit.

9Not done yet

10Where it is in the code

For a reviewer with access.