Interlock

Proof

Every run behind Interlock’s claims, the results tables, what it costs, and what is real and what is not. Back to the README.

Seven runs, one claim

the run where it ran what happened check it
10 injected refund faults × 6 systems simulated Stripe-grade API today’s retry pays wrong in 9 of 10; idempotency keys in 5; Temporal-style durable execution in 5; the gate in 0 tables below, regenerated by run_all.py
the same faults on real Stripe test mode, every id listed the key pays $40 when support refunds by hand mid-outage; the gate refuses at recovery results/stripe_live.md
real Temporal, workers killed mid-refund Stripe test mode 6/7 outcomes as wanted, 7/7 answers matched Stripe’s own records; plain Temporal 4/7 results/e2e_live.md
a Google ADK agent under an AP2 mandate, SIGKILLed Stripe test mode 5/5 as wanted with the gate as the tool callback; 2/5 with an idempotency key alone results/adk_live.md
a synthetic approval day, 100 requests mix stated as an assumption 65 of 95 cleared with no person, all 65 receipts verify, 0 wrong payouts (rules alone: 10 wrong) results/approval_inbox.md
a real model reading the gate’s refusals 40 cases per system 0 wrong, 0 sent to a person; the ungated model paid wrong 15 times results/repair_live_model.md
the design itself TLC model checker two design flaws found and fixed, each counterexample kept reproducible in spec/broken/ spec/COUNTEREXAMPLES.md

The cost is on the table too: the gate closes a crash in 43s median where a tuned hand-written re-check takes 15s, and that hand-written check ties it on outcomes wherever both ran. Both numbers are ours and published — see What it costs.

Proof, not promises:

“The system must distinguish what an agent proposed, what was authorized, what was executed, and what was durably recorded.” — the Cloud AI track brief, one sentence in, describing a thing that did not exist. Now it does.

The full narrative — the root, the field, what we ruled out, why it’s a business — is in docs/00-the-whole-story.md, as a visual walkthrough at az-said.github.io/Interlock/docs/interlock-explained.html, or as the landing page that replays the crash live: az-said.github.io/Interlock/site/index.html.

The goal: let finance teams cut two thirds of the manual approvals they do on agent actions. Much of what a reviewer checks is mechanical (is the order still eligible, was it already refunded, is this still allowed), and Interlock checks exactly that at the moment of sending. On a synthetic day of 100 refund requests (results/approval_inbox.md, mix stated as an assumption), rules plus Interlock took reviews from 100 to 36 with zero wrong payouts, where rules alone paid out wrong 10 times. On the fuller accounting, 65 of the 95 unique requests (68.4%) cleared with no person, and all 65 receipts verify.

Results

Six experiments, one gate, one journal, different worlds. The simulated cells are produced by python3 experiments/run_all.py in under a second; the live tables list their own reproduce commands and every Stripe id.

1. The refund agent (the brief’s own example)

$100 paid, one $20 partial refund approved. Invariant: exactly $20 refunded, or $0 if the lease was revoked or the order became ineligible first. Three baselines: today’s naive re-run, the conventional “just use idempotency keys” operation, and durable execution the way Temporal, DBOS and Restate recommend (recorded step results replay, a crashed step re-runs with a stable key, Stripe-grade target).

fault naive (today) idempotency key only durable execution (Temporal-style) gate @ tier 1 gate @ tier 2 gate @ tier 3
crash before send $20 ✅ $20 ✅ $20 ✅ $20 ✅ $20 ✅ $0, AMBIGUOUS ⚠️
crash before ack $40 $20 ✅ $20 ✅ $20 ✅ $20 ✅ $20, AMBIGUOUS ⚠️
duplicate submit $40 $20 ✅ $20 ✅ $20 ✅ $20 ✅ $20 ✅
model re-decides $30 on retry $50 $20 ✅ $20, replayed ✅ $20, refused ✅ $20, refused ✅ $20, refused ✅
same request, different amount $50 $20 ✅ $20, replayed ✅ refused ✅ refused ✅ refused ✅
lease revoked mid-flight refunded ❌ refunded refunded refused ✅ refused ✅ refused ✅
order became ineligible refunded ❌ refunded refunded refused ✅ refused ✅ refused ✅
support refunds by hand during the outage $40 $40 $40 $20, refused at recovery ✅ $20, refused at recovery ✅ $20, AMBIGUOUS ⚠️
lease revoked during the outage refunded ❌ refunded refunded refused at recovery ✅ refused at recovery ✅ $0, AMBIGUOUS ⚠️
recovery after the 24h idempotency window $40 $40 $40 $20, found by lookup ✅ $20, found by lookup ✅ $20, AMBIGUOUS ⚠️

Finding 1. Exactly-once is a property of the target, not the client. Achievable when the API dedupes (tier 1) or can be queried (tier 2). When it does neither, the crash cases are undecidable from the client: “sent, ack lost” and “never sent” produce identical observations. The strongest honest guarantee at tier 3 is at-most-once plus a surfaced ambiguity, and the cost is on the table: a refund that never happened stays blocked after a crash-before-send. This is the Two Generals result (1975) written as a per-service contract with a measured price.

Finding 2. Idempotency keys are necessary and not sufficient. The idempotency-only column handles crashes, duplicates, and the $30 re-decision, all at the service. It still refunds under a revoked lease and refunds an ineligible order, because the service can’t see the agent’s authority or premises. The difference between that column and the gate columns is what the runtime adds, measured rather than claimed.

Finding 4 (added after checkpoint 2). Recovery is when the world moves. The last three rows found a bug in our own gate. Until this change, recover() re-sent at tiers 1 and 2 without re-checking premises or lease, so the gate refunded $40 when support refunded the order by hand during the outage, and refunded under a lease revoked during the outage. Tier 1 also trusted the provider’s dedup forever, but Stripe prunes idempotency keys after 24 hours, and a retry after that is a new refund. The fix: a resend is a new dispatch, so I3 and I4 run again first, and after the dedup window tier 1 is treated as a lookup, not a safe retry. The idempotency-only column still fails all three, because a key only matches the same request.

2. Parallel coding agents (the same root, wearing a different hat)

Two agents on one repo. Agent B decides first, agent A lands first. That ordering is what every worktree-based product ships. Invariant: nothing lands that fails at runtime; nothing lands twice; one implementation per symbol.

fault naive (today) gate, file-hash premises gate, symbol premises
A renames the function B calls lands, breaks at runtime refused ✅ refused ✅
A and B both implement format_currency 2 implementations 1, B told A holds it ✅ 1 ✅
A edits the file in a way B doesn’t depend on lands ✅ refused ⚠️ lands ✅
crash after apply, before commit duplicated recovered ✅ recovered ✅
duplicate submit duplicated ignored ✅ ignored ✅
lease revoked lands ❌ refused ✅ refused ✅
A keeps name+arity, inverts meaning lands, breaks refused ✅ lands, breaks

Finding 3. Premise granularity is a dial with a floor. File-hash premises never land a broken change but refuse benign concurrent edits: that’s the naive “did the file change” check every worktree tool could add, and it over-fires. Symbol premises (what the agent actually referenced, not what it opened) land benign edits, catch the rename, and catch duplicated work with zero model calls. Duplicated work is the single most common multi-agent failure mode in the Berkeley MAST study (17% of 1,600 traces). But symbol premises cannot see a change that keeps the signature and inverts the meaning. No mechanically extractable premise catches that row. Catching it requires understanding intent, which is a model-quality question, and the brief is explicit that protocol guarantees and model quality stay separate. That row is the measured boundary.

The thesis behind this half, from the team’s concurrency-control spec: agent transactions need concurrency control, but not the classical kind. Abort-and-retry assumes a cheap, deterministic redo. LLM agents cost 4–15× tokens per attempt and don’t reproduce their plan on re-run. So the gate’s response to a conflict is graded by what it can say mechanically, not “abort everything.”

3. The same faults against real Stripe

Not a simulation: experiments/stripe_live.py makes a $100 test-mode card payment per run, approves one $20 partial refund, and injects the fault against Stripe’s API. Every payment id is listed in results/stripe_live.md so the refunds can be checked in the Stripe test dashboard.

fault naive (today) idempotency key only gate (Stripe key + lookup)
crash before ack $40 $20 ✅ $20 ✅
duplicate submit $40 $20 ✅ $20 ✅
support refunds by hand during the outage $40 $40 $20, refused at recovery ✅

Same result as the simulation, on the real service: the idempotency key handles the crash and the duplicate, and pays twice when a person refunds during the outage.

4. Durable execution on a real Temporal server

Not modeled: experiments/temporal_live.py runs the refund step as a Temporal activity on Temporal’s local dev server, with Temporal’s own retry policy doing every retry. A worker crash is a failed first attempt. Full output in results/temporal_live.md.

fault Temporal, recommended idempotency key Temporal with Interlock as the activity body
crash before ack $20 ✅ $20 ✅
support refunds by hand during the outage $40 $20, refused at recovery ✅
permission revoked during the outage refunded refused at recovery ✅
order became ineligible before the step ran refunded refused ✅

Temporal does exactly what it promises: the crashed step is retried and, with a stable key, lands once. When the facts behind the decision changed before the retry, it runs the same step again. Put the gate inside the activity and the same retry is refused. Interlock is not a Temporal replacement; it is the activity body. interlock.temporal.gated() is that body, and experiment 4 uses it.

The longer end-to-end run — a real model deciding, real Stripe, real Temporal, workers killed mid-step, seven support cases — is in results/e2e_live.md: with the gate as the activity body, 6/7 outcomes as wanted and 7/7 final answers matched Stripe’s own records, at a median 43 seconds from crash to close. Plain Temporal with the recommended key got 4/7.

5. A Google ADK agent under an AP2 mandate, live

Not our harness alone: experiments/adk_live.py runs a Google ADK agent holding an AP2 payment mandate, kills the process with SIGKILL mid-refund, and restarts it against Stripe test mode. An AP2 mandate says what the agent may spend; the gate’s Guard callback is what makes that hold across a crash — a journaled intent before the POST, the mandate re-verified and the premises re-checked at dispatch and again on recovery. With the Guard, 5/5 runs left Stripe exactly as wanted. An idempotency key alone got 2/5. Full table and reproduce command in results/adk_live.md.

6. How many approvals still need a person

experiments/approval_inbox.py runs one synthetic day of 100 refund requests three ways. The mix is an assumption, not measured data (60 routine, 15 over the $50 limit, 5 flagged customers, 5 ineligible orders, 5 duplicate deliveries, 5 crashes mid-send, 5 refunded by hand before the agent’s send, and, of the over-limit requests, 3 refunded in full and 2 refunded a third by hand between approval and send). Change it and re-run.

system reviews a person did orders refunded the wrong amount
everyone approves 100 10
rules only (routine requests send with an idempotency key) 25 10
rules + Interlock (interlock/approvals.py) 36 0

Rules take routine work off people, but without the gate they pay out wrong whenever the facts changed between the decision, or the approval, and the send. With the gate, a person’s approval is the authority the refund runs under, and the facts they saw are its premises: a stale, expired, or unauthorized approval is refused when the refund is actually sent, and comes back to the queue saying what changed. Of the 11 extra reviews, 10 are people closing or repairing refunds the gate stopped, not re-deciding them, and 1 is a person deciding the new, smaller amount of an accepted repair.

What it costs, measured against ourselves

The gate is slower on recovery: 43s median crash-to-close on the Temporal harness against 15s for a tuned hand-written re-check, and 46s against 10s on the ADK harness. The claim-TTL wait is the price of never resending while another worker might still be mid-send. And a careful hand-written check — an idempotency key, a lookup, a premise re-read, 6 to 10 lines per tool — ties the gate on outcomes everywhere both ran. Both numbers are ours and published: docs/11-weakness-audit.md, docs/11-quality-plan.md, and the eight live-service scenario harnesses in docs/10-scenarios.md.

What the gate adds over that hand check: no per-tool code, one journal and one receipt format across every tool, AMBIGUOUS instead of a guess where the API can’t answer, and a refusal a model actually acts on. In the live-model run, the gate’s refusals were read and correctly repaired in all 10 refused cases; the hand check’s message left the customer short in 4 of its 6 hand-refund cases.

Why this and not the obvious things

“Just use idempotency keys.” That’s the second column in table 1, and it’s the right answer whenever the target supports it. It refunds the ineligible order anyway. Keys live at the service; authority and premises live at the agent. Both are needed.

“Just log more.” A log records what the logger saw. The thing you need to know happened on a machine you don’t control, and it can only tell you by sending a message, which is subject to the same loss. Perfect client-side logging of the crash above reads request bytes written and then nothing. Logging is observation. What’s missing is attribution: which decision, under whose authority, produced which effect, once. Enterprises report having the first without the second.

“Temporal / Pydantic AI already does this.” Durable execution wraps every model and tool call as a checkpointed step and resumes from the last completed one. That solves resume and freezes model outputs. It checkpoints the step’s result, which means a tool step that dies after the effect and before the result is saved re-runs the tool. Whether that duplicates the effect is the tool’s problem. Their docs say as much: if the process crashes mid-request, the agent has no idea what already happened. Interlock is the body of that step. It journals intent before the call, checks premises and lease at dispatch, and recovers by the tool’s tier. Complementary, and the cleanest place to ship it. Table 1’s third column measures the difference instead of arguing it: durable execution used the way Temporal recommends, against a Stripe-grade target, ties the gate on every crash, duplicate, and re-decision row, and fails all five rows where the world changed after the decision. Experiment 4 repeats the key rows on a real Temporal server, with the same result.

“Keep writes single-threaded” (Cognition). Sufficient for coherence, not necessary. It’s the rule a database would impose with no concurrency control, and databases abandoned it for throughput. The benign-edit row is a concurrent write landing safely.

“CaMeL solves prompt injection with capabilities.” Yes, and it was the closest prior work until this summer. CaMeL controls whether untrusted data can influence control flow. It has no model of crashes, retries, duplicate delivery, or revocation. It answers “was this action allowed?” Interlock answers “did this allowed action happen, once, under authority that was live when it fired?”

“Didn’t a paper just do this?” Three did, in pieces, between June and September 2026. ATR (Huawei) re-checks typed premises but excludes crashes and non-idempotent APIs. Cordon (Tsinghua, EuroSys 27) stages effects and parks an unproven dispatch in an audit state, which is our tier 3 from the security side. “Engineering Reliable Commit Gates for Agentic AI” (WashU) benchmarks verifiers and shows after-check races need atomic guards. None re-checks premises on the recovery path or states a guarantee per target, and none ships adapters for real services. Three groups converging on this layer in three months is the best evidence the layer is real. Details in docs/03-landscape.md.

Full landscape, with the tools attacking parallel-agent conflicts today, in docs/03-landscape.md.

What’s real, what’s not

Real. The journal, the gate, the targets, every experiment and every number above. python3 experiments/run_all.py regenerates the simulated results/ from scratch in under a second; each live table carries its own reproduce command.

Tested. python3 -m unittest discover -s tests — 465 tests in 43 files, 412 passed and 53 skipped on the last full run (the skips are the live-service suites, which need keys), 0 failed; CI on Python 3.9, 3.12 and 3.13 on every push, failing if results/ drifts from the code. The suite asserts every row above, where each baseline fails as well as where the gate holds; runs 2,000 randomized interleavings of tier, crash point, events before the decision and during the outage, late recovery, and duplicate delivery; races eight workers on one journal (JSONL and SQLite) to prove one dispatch and one recovery; tampers with receipts; runs the approval inbox through stale, expired, and unauthorized approvals; runs the three-line integration through a simulated restart; and kills the MCP proxy mid-call against a real subprocess server. Building and hardening the gate found real bugs in our own code at every stage — 15 before the escalation build, 30 more across three adversarial hardening rounds, 6 in the merge review — and each fix has a test in tests/ that failed before it. The worst was critical: a recovery running while a send was still being applied could send it a second time; sends now hold a claim that recovery waits out. The full inventory is tests/README.md.

Model-checked. The recovery design is a TLA+ model in spec/, checked with TLC for the stated constants — a model check, not a proof of the Python or the SQL. It found two design flaws before any test did, both fixed in the code, and every counterexample is kept reproducible by the configs in spec/broken/ (spec/COUNTEREXAMPLES.md).

Simulated. The payments API and the repo in tables 1 and 2 are local. Faults are injected, not observed. This is by design: the brief asks for targeted failures at meaningful boundaries, not random process kills.

Real, against live services. interlock/targets/stripe_api.py is a Stripe refunds target (test-mode keys only, standard library only); experiments 3, 4 and 5 run against real Stripe, a real Temporal server, and a real Google ADK agent, and the eight scenario harnesses in scenarios/ cover payouts, disputes, billing credits, calendar, email, GCP resources, GitHub merges and a shared spending cap.

Not built yet. A real GitHub merge target in the gate itself. Premise extraction beyond file hashes and function arity. A notary that both sides write to, so tier 3 services can be lifted to tier 2 without changing their API.

Out of scope, on purpose. Whether the agent’s decision was right. A faithfully executed bad refund is still a bad refund. Interlock controls effects, not judgment.

Next test

Swap LocalRepo for a real gh pr merge target and measure how often the gate must return AMBIGUOUS when the merge API response is dropped, versus when GitHub’s merge-commit lookup is used as the tier-2 query. The ratio is the availability cost of running without a cooperating target.

References

The ones the results lean on. The full list with notes is in docs/05-reading.md.

Interlock — Battle of the Coasts 2026, Cloud AI track, Boston. MIT licensed. Fork it, break it, tell us which row is wrong.