The foundation · version 5
ARBITER: the foundation, stated to be checked
Version 5, 23 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, their proof, and the replay that ties the code to the model: gate/model/ at 695b933, published at consequenceaisystems.ai/foundation/model/695b933/.
Note, 24 October 2026: the proof's prover, tlapm 1.6.0-pre, is a rolling pre-release, and its GitHub address now serves a later build, so Dockerfile.tlaps at 695b933 no longer builds. The same twelve files, with Dockerfile.tlaps fetching the exact build the proof was checked with from this site, are at consequenceaisystems.ai/foundation/model/e05ad81/ (only that file differs). The later build gives the same result.
Note, 25 October 2026: the gate now runs gate/worker.js as committed at d9aed52 (version gate-3, SHA-256 cffffb2766b204cdbe204ee576b481e12a57a7cd990b280c483f6b6728f43c65), pasted into Cloudflare's editor that day (R2), and ARBITER's production server runs d9aed52. It changes who may read a request. This note also corrects what G4 and section 4 say the log records. Both are set out in "Since version 5", at the end. G1 to G3, the model and the proof do not change.
Note, 26 October 2026: the gate now runs gate/worker.js as committed at 1e5553a (version gate-4, SHA-256 fcbc5e0fcf619c2a941152a745b8e5b571a60fa9fca8020a2b483af322e419d0), pasted into Cloudflare's editor that day (R2). It changes which refusals the log records, in whose name and under what allowances, so parts of the 25 October correction to G4 no longer hold. This is set out in "Since version 5", at the end. ARBITER's production server is unchanged. G1 to G3, the model and the proof do not change.
Note, 27 October 2026: a full dress rehearsal ran ARBITER's production code with a test gate that reports the same gate code (gate-4), and a passkey registered from a phone decided two of its payments: 115 checks passed, 0 failed. Its run log, and the copy of the test gate's log it checked, are listed in "Since version 5", at the end. The production gate and ARBITER's production server are unchanged.
Note, 1 November 2026: the production gate's owners are now two hardware security keys, and a new passkey on the founder's phone may only approve. The passkey made at setup, a passkey synced through the founder's Google account, is revoked. From the same day a job on GitHub's machines checks every hour that Cloudflare runs exactly the gate our repository records. The gate's code (gate-4), ARBITER's production server, G1 to G3, the model and the proof do not change. Both are set out in "Since version 5", at the end, which also says what they replace in sections 6 and 9.
Changed from version 4: the gate's code is tied to its model. The gate's own log of every change it makes is replayed against the model, step by step: the log of the gate's tests on every change to its code, and the live gate's whole log every day (section 4, "The code against the model"). Changed from version 3: G1 to G3 are proved for every behaviour of the model, with no bounds. Changed from version 2: the rules are checked by machine within bounds. Changed from version 1: the gap section 4 showed is closed in gate-2. Every version is kept: version 1, version 2, version 3 and version 4, and in commits fb97988, a2511c2, 3857290 and 1839f2b.
Consequence AI Systems · jerrymcclintock@sovereignarbiter.com
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:
- 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.
- 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.
- 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:
- G1: every approval was recorded with the authority of item 2 in force at that moment; every payment instruction went out on the signature of a person the owner chose, made for that very request on the gate's page; nothing is paid to an account the owner did not list.
- G2: a request is approved, and so paid, at most once.
- G3: authority changes only when a change an owner signed is applied for the first time while its signer is an active owner, or at setup, once; the gate always has an active owner after setup; the attacker's passkey and key never gain authority.
| Case | Bounds | Result |
|---|
gate-2, payments | Any state the owner's changes can reach; two requests; one change by the owner at any moment while they wait | Every property holds: 8,290,140 distinct states |
gate-2, changes of authority | Two owners, three signed changes, everything granted at the start | Every property holds: 15,052,721 states |
gate-2, from setup | From nothing: setup, registrations, four changes, a request | Every property holds: 28,481,992 states |
gate-1: the key and payee not checked again at approval | As payments | G1 broken in 13 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 transaction | As payments | G1 broken in 13 s: the approver revoked between the two |
| Approval terms without the request's id and hash | As payments | G1 broken in 58 s: root replays a person's approval of one request on another with the same terms, and it pays |
An approval leaves the request pending | As payments | G2 broken in 12 s |
No record of applied changes (used_ops) | As changes of authority | G3 broken in 49 s: root replays an owner's change from the log and undoes a later one |
| The signer not checked again in a change's transaction | As changes of authority | G3 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 the replay below checks for the runs that happened; 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), which the proof below covers; or anything about the cryptography and WebAuthn's own checks, which the model assumes.
Proved, with no bounds
TLC tries every order of events within its bounds; a proof covers them all. GateProof.tla proves, for every value of the constants (any number of companies, requests, owners, approvers, payees, keys and changes, any number of passkeys and keys held by the attacker, any amounts and limits, a clock that runs as long as you like), that every behaviour of the model keeps G1 to G3, the same properties TLC checks. The method is an invariant that holds at the start and that every step keeps, whose parts say why each property holds:
- every signed change, in a call or in the log, was made by an owner and names nothing of the attacker's;
- the attacker's passkey and key are never active, and nothing is granted to them;
- payees are only accounts an owner may list;
- setup closes for good, and after it there is always an active owner;
- every decision on its way, in the log or paying, was signed by a person the owner chose, for that very request;
- an approved request is never pending again.
The proof system TLAPS checks every step of it: all 629, in about five minutes on one core. The proof assumes only that the gate runs as modelled (no check removed) and that the people and keys are distinct: the attacker's passkeys are neither owners' nor approvers', and its keys are not ARBITER's. TLC's configurations satisfy these, so they cannot contradict each other (if they did, anything would follow). Run on gate-1's design, the proof fails at exactly one of its 629 steps: the one that says an approval is recorded with the authority in force, the gap version 1 showed.
What the proof does not change: it is about the model, not worker.js (the replay below ties the two), and the provers are trusted (tlapm, which divides the proof among Z3, Zenon, Isabelle and LS4).
The code against the model
The model and its proof are about Gate.tla; the gate runs worker.js. They are tied by the gate's own log, which records every change the gate makes to its records, signed and chained (G4). trace.sh turns a log into the steps of the model its entries stand for, with the logged values (who signed, which change, which request, account and amount, at what time), and TLC takes exactly those steps, in order, from an empty gate. Either the model takes every entry, so every change the code made is one the model allows at that point, or TLC stops at the first entry it does not allow, and the replay names it. Since version 4 the model has sets of people and keys where it had one of each, so that it can stand for any log: an owner who also approves, several approvers, several passkeys and keys that were registered and never given authority.
| Log | Result |
|---|
The gate's own tests (gate.test.mjs) on gate-2 | The model takes all 101 entries |
| The live gate, from its first entry | The model takes all 28 entries |
The same tests on gate-1's code | Stops at entry 73: an approval recorded after entry 72 unlisted the request's payee, the gap version 1 showed |
Every change to the gate's code must pass this before it can land: the tests' log is replayed as part of the gate's CI job. Every day, the live gate's whole public log is replayed against the model on GitHub's machines. Anyone can run the same replay on the live gate (section 8).
What the replay does not show: it checks what the code did, not what it refused (a refusal changes nothing in either, so it is skipped, and that the model would refuse it too is not checked); it covers the runs that happened, not every run the code could make; and it reads the log, so it checks the code's own account of what it did. G4 lets anyone check that account is signed and unbroken, not that it is complete. The one change the model leaves out, adding a company, is skipped: the model starts with every company added.
Since version 5
25 October 2026: who may read a request (gate-3)
What changed. Until gate-3, anyone who held a request's id could read the request and its terms from the gate (GET /v1/requests/<id> and /terms). An id is not a secret: every one is in this gate's public log. Now the gate shows them only to:
- an owner signed in with their passkey;
- an approver signed in with their passkey and granted for the request's company;
- a read signed by an ARBITER key granted for that company (Ed25519, over the gate, the request, the path and the time).
Anyone else gets the same answer whether or not the request exists: a refusal before the request is looked up when there is no sign-in or valid signed read, and otherwise the refusal an unknown id gets. A refused read writes nothing. A sign-in lets the person read, nothing more: approving still needs their passkey's signature over the exact terms (G1). It lasts up to eight hours. Signing out clears it from that browser; only revoking the passkey ends it at the gate, so a copy of it keeps working until then. Sign-in changed with it: its challenge is now a value the gate checks with a secret only it holds (HMAC-SHA256), not a stored row, so it has no gate-wide hourly limit for anyone to use up, and each challenge is accepted once.
What it holds against. A1 to A4. Not A5, nor a shell in the broker: both hold ARBITER's key (R4), so they can read every request of the companies that key is granted for; ARBITER keeps these requests in its own records too. The rule is not one of G1 to G4. It is not in the model or the proof, and the replay cannot see it: no entry records a read or who made it, and an allowed read logs only what reads logged before (an expiry, an expired request's receipt). Its evidence is the gate's tests.
What stays public on this gate. The log is public (G4), so each request's text, each decision's terms and each payment's receipt can still be read there by anyone. What the log does not hold is now private: the gate's signed receipt for a rejection. An expired request's receipt goes into the log when it is made, which is now when an owner, an approver or ARBITER first reads the request; until gate-3, anyone's read made it. On a gate whose log only its owners can read, G4's "anyone can read" does not hold, and this change keeps its requests' terms private, though not whether they exist or how they ended.
Limits that remain.
- Anyone who holds a request's id can learn from
POST /v1/requests/<id>/decide, without signing anything, whether the request exists, whether it is still waiting and, if not, how it ended.
- A signed read can be replayed, for that request and path, by whoever sees it, until five minutes past the time it carries: up to ten minutes after it is made if ARBITER's clock runs ahead of the gate's. ARBITER sends it only to the gate address it is configured with, an
https:// address in production.
- Reads are not in the gate's log.
- While ARBITER holds no key granted for a company, because its key was revoked or granted elsewhere, it cannot read that company's requests, and its own record of a request still open stays open. The gate holds the outcome, and an owner can read it there.
A correction to G4 and section 4. G4 says every refusal is appended to the log. Only four kinds are: a wrong setup code (while setup is open, within its ten tries an hour), an owner change whose signature does not verify or is not an owner's, a refused payment request, and a refused decision; and only once the call's body has been read, as a JSON object of at most 16 KiB. Every other refusal is answered and never logged, among them an owner change already applied or too old, any setup attempt once setup has closed, and refused sign-ins, registrations and reads. The four logged kinds share one allowance of 600 entries per clock hour, which limits how fast anyone can add to the log. Anyone can use it up with unsigned calls, and those refusals then go unlogged until the hour ends. Section 4 says the log records every change the gate makes to its records. It records every change of authority (G3), and every request's arrival, decision, expiry and payment outcome, but one: a payment interrupted after it was sent, which the log shows only as its approval, with the request left executing. It does not record a rejection's receipt, which is kept with the request, or the gate's own bookkeeping: challenges, used sign-ins, the signature counter a sign-in moves on, and the allowance's counts. All of this was so in gate-2 too. It hides no change of authority, no payment is sent before its approval is logged, and G1 to G3 do not depend on it. Since 26 October (gate-4) some of this no longer holds as written. An owner change that a passkey the gate knows signed is now also logged when it is refused as already applied, as too old, or because the gate refuses the change itself (revoking the last owner, for example). And the 600 is now one of three allowances, so using it up no longer stops a key that setup or an owner made active from having its refusals logged in its name, replays aside. See "26 October 2026: refusals in the signer's name (gate-4)", below.
The numbers now. The gate's tests are 170 checks and the end-to-end test 40. G1's evidence says 124 and 32 and R12 says 124; section 4's "9 of the gate's 124 checks" is about that older suite. The tests' log is 109 entries, and the model takes all of them. The live log is unchanged: entry 28, with the hash in section 8. Gate.tla, GateProof.tla and the checker are byte for byte the files section 8 lists. trace.sh in our repository has changed since (4cb2fe0: it retries a dropped read of a live gate and stops if it read only part of the log); the published copy still works.
26 October 2026: refusals in the signer's name (gate-4)
What changed. A logged refusal now names the key that signed the refused attempt, as by, when that signature verifies with the registered public key the attempt names (a passkey's credential id, an ARBITER key's fingerprint). For a passkey, that means an assertion over the attempt's own challenge (an owner change's or a decision's) that passes every check the gate makes of it, up to and including the signature; a counter that went backwards is checked after that, and its refusal names the key too. For an ARBITER key it is a signature over the request's text. The key may be active, waiting for an owner, or revoked.
Anyone can register a key to wait for an owner, and registering one shows nothing about who holds its private half (an ARBITER key is registered with its public key alone, and the gate checks no signature when a passkey registers), so by says which registered key made the signature, not who sent the attempt. A signature that does not verify names no one, so naming someone else's key costs that key nothing. Refusals the gate makes before it has the named key's signature to check name no one: a request with no text, text over 4,096 characters, or no key named; a key it does not know; a decision that is neither approve nor reject, or one on a request that does not exist or is no longer waiting. The gate's own receipt key is never named. A refused request's key is still the fingerprint the request claimed, signed or not.
How much is logged. Each clock hour:
- each key that setup or an owner's signed change has made active, whether it is still active or revoked since, has its own 20: the first 20 refusals in its name that are not replays (below) are logged. The gate finds these keys in its own log, so keys made active before
gate-4 count too;
- keys never made active (waiting for an owner, or revoked while waiting) share 400;
- everything else shares 600, as every refusal did until now: refusals that name no one, and replays.
Once an allowance is used up, the refusals it covers get the same answer and go unlogged for the rest of the clock hour, even if another allowance has room.
A replay is a request the gate already holds from that key with exactly that text, or an owner change whose id was already applied, whatever its terms. Anyone can copy those from the public log. A replay still names its key and is marked replay, but it counts against the 600, never against a key's own 20 or the 400. For a request, replay says the log holds that key's signature over that very text; for an owner change, only that a change with that id was applied, not that these were its terms. Neither says who sent it.
At most 600 + 400 refusals, plus 20 for each key that setup or an owner has ever made active, are logged in one clock hour: 1,040 on the live gate today, whose two such keys are the owner's passkey, made by setup, and ARBITER's key. Setup has closed, so only an owner's signed change can raise that number.
Newly logged. An owner change signed by a passkey the gate knows, refused because its terms are too old (logged with op null when the change in them is not a valid one), because it was already applied, because the gate refuses the change itself (revoking the last owner, for example), or because its signer stopped being an active owner after its signature was checked. gate-3 logged none of these. No test reaches the last case: nothing else runs at the gate while it checks a signature, and the re-check does not rely on that. Nor does any test send terms too old whose change is not a valid one.
What did not change. Every refusal gets gate-3's answer, word for word, and so does everything the gate accepts. For a key waiting for an owner or revoked, and for owner-change terms too old, the gate checks the signature only after deciding the refusal, and only to say who signed. Only the version the gate reports and the log differ, and with the log what reports on it: the log head at /.well-known/arbiter-gate, and a receipt's place in the log (decision_seq). Refusals are logged as the same four kinds of entry, and only once the call's body has been read, as a JSON object of at most 16,384 characters as JavaScript counts them (UTF-16 code units, so an emoji counts as two; the 25 October correction calls this 16 KiB, but it is not bytes). Still not logged: refused sign-ins, registrations and reads; any setup attempt once setup has closed; owner-change terms that are not this gate's; terms too old that no passkey the gate knows signed; and terms not too old whose change is not a valid one (an unknown kind of change, a malformed field), even when signed.
Of the 25 October correction to G4, then, three things no longer hold: that one allowance of 600 covers every logged refusal; that the only owner changes logged are those whose signature does not verify or is not an owner's; and that an owner change already applied or too old is never logged. The rest of it stands, as does its correction to section 4, with two more pieces of the gate's own bookkeeping: the three allowances' counts, and its list of the keys made active, which it builds from its own log.
What it holds against. For each passkey that setup or an owner made active, the allowance holds against A1 to A5, short of the fingerprint match under Limits: nothing they send uses that passkey's 20, so the first 20 refusals in its name in an hour, replays aside, are logged. None of them can make its signatures, and those it makes go from the person's device to the gate over TLS. ARBITER's key is different. Root on the ARBITER server and a shell in the broker hold it (R4), and it signs whatever ARBITER is made to ask: the broker asks the gate to pay every completed intent of an action paid through the gate, with the account and amount the intent carries. So code in the executor (A4); the agent's tool (A3), which reaches the broker, if it has the id of a completed intent the gate refused; and a company's users or API keys (A2), for intents their company's rules let through, can all make it sign requests the gate refuses. Any of these can spend its 20. Those 20 are logged in its name; that key's later refusals that hour, those of the requests ARBITER sends in its normal work included, are not, unless they are replays. ARBITER uses one key for every company, so its 20 cover them all together.
Limits that remain.
- The log does not keep a refused attempt's signature, so
by is the gate's word, as the refusal itself is.
- Whoever holds a key, can make it sign, or has seen one signature it made that the log does not hold (a signed read in transit, for example) can spend that key's 20. One such signature is enough in every hour, even after the key is revoked. An ARBITER key's signature, or a passkey's over an owner change, works however old; a passkey's over a decision only while that request waits; a sign-in's never. The five minutes a signed read is accepted for reading do not limit this.
- An hour with more than 20 refused requests from ARBITER logs only 20 of them, where
gate-3 logged them all while its 600 had room.
- Anyone can spend the 400 and the 600; refusals under them then go unlogged until the hour ends.
- A passkey's holder can put its own refusals under the 600, marked
replay, by reusing the id of an owner change already applied.
- A key's allowance is found by its 64-bit fingerprint, the same whether the key is a passkey or an ARBITER key. Someone who makes a key of the other kind with the same fingerprint, about 2^64 tries, can register it and spend that key's 20.
- None of this is in the model or the proof: refusals change nothing the model tracks, and the replay of the log against the model (section 4) skips every refusal. Its evidence is the gate's tests.
The numbers now. The gate's tests are 209 checks: 39 added since gate-3, 29 of which fail on gate-3's code (the other ten hold what gate-3 already did). The end-to-end test is still 40 checks. The tests' log is 1146 entries, 1072 of them refusals, which the replay skips, as it skips adding a company (section 4); the model allows each of the 65 steps it takes from the rest. The live log is unchanged by the deploy: entry 28, with the hash in section 8. gate-4 changes none of Gate.tla, GateProof.tla, the replay (trace.sh and the trace.py it runs) or the checker.
27 October 2026: a dress rehearsal with a test gate
What ran. The full dress rehearsal (as on 13 October, section 8), with the gate added. On a disposable copy of production, with the executor, broker and database code production runs and the real AI models, six made-up companies used ARBITER, and four of them paid through a test gate, rehearsal-gate (gate id rehearsal-gate-1, rehearsal-gate.jerrymcclintock1.workers.dev), which reports version gate-4, with its own public log and its own Slack channel. The run attacked the gate as an outsider, as another company, through the AI model, from a shell in ARBITER's executor and as root on ARBITER's server. ARBITER's founder decided two of its payments with a passkey registered from a phone: approved one, rejected the other. 115 checks passed, 0 failed. The test gate's log as the run checked it, 2,144 entries, holds with the checker in section 8 and replays against the model (section 4).
What it does not show. On the test gate, the owner's passkey and every approver's but the phone's are software keys on ARBITER's server, the server the run attacks as root, and an approver granted for a company could have approved root's own request. The attack never uses those keys: it shows what root can do without them, which is root's position against the production gate, whose only owner and approver is a passkey on the founder's phone. The run log sets out this and its other limits.
-
code ecf52ec115 passed, 0 failed
sha256 5d33f43d9f1d8191423897eda5a4e56732b97fee99190b05530914caaba3a88e
-
head 132dfe13a78f93d41a80aa334381ec184ed2d94e7352ad30db88e0b06fb707f5
sha256 34206e434cd77e399a8397e48046436ea062b1e6ad7122825044fd7028e70124
-
sha256 8dc817e674ed1c170d860aaf5e9f4190a95eb131f09628b885f687b9952f3ac4
1 November 2026: two security keys own the gate, and its deployments are watched
What changed. Two security keys (YubiKey 5C NFC), each with its own PIN, were registered and made owners by changes the first owner signed: log entries 30 to 34 (entry 29, a first attempt from one key, was revoked at 33). Then, each signed by the first key: a new passkey on the founder's phone, registered without asking to be an owner (35), was activated as an approver only (36) and allowed to approve for the one company the gate serves, the test company "Boundary proof (test)", up to 50,000.00 (37); and the first owner, the passkey made at setup on 16 October, was revoked (38). The gate's description now reports two owners.
Why. A synced passkey has a copy wherever its account is signed in, and an owner can change everything at the gate: add an owner, a payee, a key or a higher limit (G3, R9). A security key's passkey never leaves the key, and each use needs the key in hand, its PIN and a touch. The phone keeps what it needs from day to day: an approval, which pays only what ARBITER asked, to a listed payee, under the limit (R5 to R8).
How to check it. The checker, as published in section 8, holds on the log's 38 entries and names the owners now: aa5f86cc42992f34 and abefa4c6e7776cd1. Every owner change carries the signer's authenticator data. Its flags byte is 0x05 in entries 36 to 38: the person was present and verified, and the credential cannot be backed up, so it cannot be synced or copied off the key. In every change the first owner signed it is 0x1d: verified, and backed up, a synced passkey. The second key has signed no change yet. All 38 entries replay against the model (section 4). Entry 38 has hash 90daa3be09d216b9a139e5ea8874983328ac3c3a60755fc6b4494090236a50dd: confirm it as in section 8, with after=37.
The deployment watch (R2). Cloudflare sends no notice when a Worker is deployed. Every hour a job on GitHub's machines reads what Cloudflare runs as the gate, with an API token that can only read the gate's Worker, and compares it with what our repository records: the serving deployment must run exactly the recorded version (now 509ac9cc), no newer version may be waiting, and its code must be gate/worker.js as committed at 1e5553a, byte for byte but for the newline that ends the file, which Cloudflare's editor drops (SHA-256 9bdd3eca5c318ae2207904ab4daf9995c51ebc518c1f9b51b4ffa47105ef3ddb). Anything else alerts us, a changed secret included, and so does a watch that stops running. It sees a change after the fact, within the hour; it cannot stop one. (Commit 9b7c4fd.)
What it replaces. In section 6: the owners are the two security keys, not a passkey on the founder's phone, and the only approver is the phone's new passkey (the owners approve nothing). As of 1 November the Cloudflare account has one member, one API token (the watch's, which can only read the gate's Worker), and two-factor sign-in that also takes the two security keys. In section 9, the second owner is done. In R13, the owner's device is now the two keys and their PINs. The 27 October section's "the production gate, whose only owner and approver is a passkey on the founder's phone" describes that day.
What it does not change. The gate's code, ARBITER's server, G1 to G3, the model and the proof. If both keys were lost, no owner change could ever be made again (setup is closed), though the approver could still approve; they are kept apart. Whoever holds the Cloudflare login can still replace the gate's code: the watch makes that seen, not impossible. Root on ARBITER's server holds our repository's deploy key, so it could record a new version for the watch, in plain sight in the repository's history.