A Summary Is Not a Permission

Take the Ashdown instruction, the invented intake matter that recurs through this book. The intake agent may read the letter and the privileged advice, summarise the advice, and send the public filing. For this chapter I add one restriction: the filing goes out only after a partner confirms. At some point a line in a case-management system lists the advice note in the filing pack. Nobody entitled to decide has decided anything. The agent's memory writer absorbs the line, and the record now says the advice may be sent. A later step reads the record and sends it.

Every part of that chain behaved. The executor did what its record said. The log, faithfully kept, shows a permitted act. The record was wrong, and the system's own memory made it wrong, with no attacker. Tommaso Cerruti, Mika Okamoto and Ansel Kaplan Erol have named this: "endogenous authorization laundering", in which "the system's own memory creates authority absent from the underlying history" (Cerruti et al., 2026). The term and the measurements are theirs. I use warrant-drift for one narrower thing, the case where a summary widens a grant, because I need a name for what a rule can forbid. I claim no novelty beyond that label.

A summary of a grant is evidence about a grant, and an agent's memory should have no vote on whether an act is allowed. Three claims follow, and each could be wrong. First, a summary may only narrow what it summarises. That rule is decidable over typed records, but it works only as a comparison with an authoritative ledger, made at the time of use: no check that sees only the memory can do it. Second, shorter is not narrower. Compaction that drops an action narrows a grant, and compaction that drops a restriction widens it, so the pressure that drives summarisation has no safe direction. Third, and most contestable: the correct stored form of a permission is a pointer. A copy the writer can rewrite is at best a planning hint. If a memory writer that updates incrementally, with neither the ledger nor the full history to read, can match a ledger without giving up legitimate work, the third claim falls.

I build AI systems for law firms, and I gain if buyers ask where an agent's permissions are read from. Nothing here is legal advice.

What the paper measured

Its headline numbers travel badly, so here are the conditions. It is a workshop paper, version 2 dated 24/10/2026.

The setup. Seven models act as memory writers and two as executors. There are three domains, procurement, cybersecurity and finance, with 12, 16 and 8 synthetic cases and 36, 64 and 32 matched pairs of requests, one authorised and one not, differing in one relevant field. A hidden deterministic ledger supplies ground truth. The executor sees the stored memory and the request, and never the history. Executors were admitted only if they made no error under correct memories, so the design attributes failures to the memory. There is no attacker.

The 45.4%. The abstract says writers create false authority for "up to 45.4% of unauthorized requests". That is the finance domain under typed incremental updating, pooled across seven writers and three seeds. Procurement is 25.9%, cybersecurity 10.5%, and all three pooled 23.2%. It is the worst domain.

The 99.0%. This is conditional. Given a typed memory already holding false authority for the request, the executor acted in 386 of 390 trials. After the memory was replaced with an oracle-exact one, it acted in 1 of 390. The 99.0% does not mean 99% of unauthorised requests succeed. The figure to carry is the unauthorised action rate, which under typed incremental memory is 26.6%, 10.5% and 45.9% by domain.

The update strategy. Averaged across domains, typed memory written once from the full history gave 0.8% unauthorised actions. The same representation updated incrementally gave 27.7%. They trace this to semantic misinterpretation, where restatements by people who cannot grant anything are adopted as changes, and failed persistence, where legitimate updates fail to apply and stale permissions remain.

The limits, in their words: "our cases and tools are synthetic, leaving transfer to real deployment uncertain". Their ledgers are closed-world, with "one recognized authority class and unambiguous fields". Nor is the raw history a safe harbour: their diagnostic that reasons directly from the full history gave 33.6% unauthorised actions in cybersecurity and 13.0% in finance, though 0.0% in procurement, with procurement and cybersecurity at one seed. I read the paper as showing a mechanism, not deployed rates, and as showing that a model reading only the memory is the wrong place to fix it. Swapping executors moved unauthorised action rates by under a point.

The rule

The recurring case file has a Grant.narrows, written for delegation. It does not suit summaries, and I can show why. It ignores the holder, and it ignores revocation: case_narrows_ignores_holder and case_narrows_ignores_revocation each exhibit a child that passes it and permits what the parent refuses. That suits delegation, the subject of Who Proves the Agent Is Yours?, where the holder is meant to change. For a summary it is a defect.

So my file adds a restriction list, confirmBefore, and a stricter rule. This block is copied from lean/BuildingInSteel/WarrantDrift.lean and compiles on Lean v4.29.1 with no libraries beyond the case file:

def Warrant.narrows (s w : Warrant) : Bool :=
  decide (s.grant.holder = w.grant.holder) &&
  s.grant.actions.all (w.grant.actions.contains ·) &&
  decide (w.grant.validFrom ≤ s.grant.validFrom) &&
  decide (s.grant.validTo ≤ w.grant.validTo) &&
  revNoLater s.grant.revokedAt w.grant.revokedAt &&
  w.confirmBefore.all (s.confirmBefore.contains ·)

Read the last line against the second. Actions are covariant [the summary's set must sit inside the ledger's]. Restrictions are contravariant [the ledger's set must sit inside the summary's].

narrow_sound is the general result: for every summary and warrant, whatever a narrowing summary permits, the warrant permits. narrow_trans shows that narrowing composes. store_sound lifts it to a memory: for every fixed ledger and any sequence of writes, a store built through the admission check permits only what the ledger permits.

On the Ashdown path, laundering_formed computes the paper's formation event at tick 6: the record permits sending the advice, and the ledger refuses. rule_blocks_laundering shows the rule refuses the record. ashdown_path_blocked runs it end to end: offered a faithful record and then the laundered one, the store refuses to send the advice and still sends the filing on confirmation.

The idea is old, and I am not its author. Norm Hardy's confused deputy, a compiler that "serves two masters and carries some authority from each", is the ancestor of the failure (Hardy, 1988). Macaroons embed caveats that "attenuate and contextually confine" a credential (Birgisson et al., 2014). The nearest statement for memory is Jinghan Xu and colleagues': "summarization may preserve information, but it must not upgrade the authority of the source". Their firewall gates tool calls on platform-held provenance (J. Xu et al., 2026). Zhan and colleagues call a neighbouring failure "authority collapse" (Zhan et al., 2026). Those two works ask how far a source may be trusted. Mine compares the fields of a grant, a different axis: Cerruti and colleagues note that "correctly attributed permissions with incorrect scope or validity remain undetected by origin checks", and J. Xu's limitations list scoped policies as "natural extensions". What I add is small: the scope-and-time version of a known principle, kernel-checked, with its consequences drawn out.

Shorter is not narrower

It is tempting to treat summarisation as lossy and loss as safe: the worst it can do is forget. For an allow-list that is true. drop_action_narrows proves that dropping an action narrows every warrant, and add_restriction_narrows proves the same for adding a restriction.

Now remove the line about the partner. shorter_can_widen computes it on Ashdown: the compacted record is shorter, it fails the rule, and it permits sending the filing with no confirmation, which the ledger refuses. A prohibition is information. Compress it away and the grant grows.

A memory writer holds both kinds of statement in one text and has one instruction, which is to fit. The paper states the two errors side by side: "Forgetting a revocation preserves stale authority; dropping a permission blocks a valid request." The kind of sentence dropped decides the sign, and a summariser working in free text has no field that records the kind.

Where the check has to sit

Three results rule out the cheap locations.

Not at write time alone. write_check_goes_stale takes an exact copy of the research grant. Before the withdrawal it narrows the ledger. After it the same bytes do not, and they permit a read at tick 6 that the ledger refuses. unrevoked_never_narrows_revoked is the general form. No writer erred; the world moved. This is where Yesterday's Permission meets this chapter: a record can become wide without being touched.

Not against the previous record. Incremental writers see the last memory and the new block, so the natural check compares the two. chain_narrows_root proves that this suffices for every chain if every step was checked from the root. local_check_carries_drift shows the cost of one missed step: the record narrows its predecessor, fails against the ledger, and still permits sending the advice. Copied forward, it passes the local check again, because narrow_refl holds for every warrant. The paper reports a neighbouring behaviour in one procurement study at a single seed: observed errors persist in 98% of cases, and self-repair stays near 2%.

Not in the memory or the executor. This block compiles from the same file, and the proof is shown in full:

theorem no_memory_only_check (f : Warrant → Bool) :
    (f laundered = true ∧ laundered.narrows ashdownLedger = false) ∨
    (f laundered = false ∧ laundered.narrows laundered = true) := by
  cases h : f laundered with
  | true => exact Or.inl ⟨rfl, rule_blocks_laundering⟩
  | false => exact Or.inr ⟨rfl, narrow_refl laundered⟩

The proof is two cases, because all the content is in the type: f has no ledger argument. In one world the record was laundered. In the other the same record is the grant. Any function of the record alone gives one answer to both. ledger_access_escapes shows the hypothesis matters: given the ledger, both worlds come out right. This is the small formal cousin of the paper's "Executor-side alignment cannot close this gap; a safeguard has to reach the memory itself". I accept the first half and part company with the second. Their executor has no ledger and they tested no gate that has one, so the second half is their inference, and the opposite one here is mine, equally untested. I read it as reaching any memory-level filter that consults no authoritative source. A filter reading platform-held metadata has a kind of ledger, so J. Xu's firewall is not refuted by this.

A ledger-reading check at retrieval would survive those three as well, so choosing the tool boundary is my judgement: it is the last point before a side effect. The gate reads the current ledger, outside the generator. The Guaranteed Safe AI framework makes the same separation, with a verifier issuing a proof certificate "relative to the world model" (Dalrymple et al., 2024), whose first author launched ARIA's Safeguarded AI programme. Here the ledger plays the world model, and the verifier is a few lines long.

gate_sound proves that a pass implies the ledger permits, for every ledger and record. My first design was still poor. whole_record_gate_overrefuses shows it: a gate demanding the whole record narrow turns one wrong field into a refusal of everything, so the laundered record also blocks the legitimate filing. And rejected_write_keeps_stale shows my admission check has a flaw the paper warned of in its own fallback. An update that records the withdrawal but also launders an action is rejected whole, so the older unrevoked record stays and still says yes.

The design that survives has two jobs in two places. At the tool boundary, ask the ledger about the act. At the write boundary, use the rule to decide what stays in memory, re-run it when the ledger moves, and quarantine what fails. A wide record is harmless to authority once the ledger decides, but it still steers what the agent attempts.

Point, do not copy

Once the ledger decides, what should memory hold? An identifier, and if you like a cached description for planning, marked as such. pointer_follows_revocation computes the benefit: the same pointer record says yes before withdrawal and no after, with no memory write. That is true by construction, which is the point: a revocation needs no memory write. The pointer is not immune. pointer_can_be_swapped shows that changing one identifier to a wider entry for the same agent widens the record with the ledger untouched, so the gate must ask the ledger about the act, and not about the entry the memory names.

Separate evidence points the same way on utility, and not on safety. MasDrift compares two multi-agent defences: one re-anchors each pending call to the original request, and the other carries an attenuated policy down the delegation chain. The chain variant, which is my narrowing rule handed to the agents, eliminates executed unauthorised actions but blocks up to 54.5% of attempted required calls and forfeits up to 36.3 points of completion. The source-anchored one reduces unauthorised actions without eliminating them, blocks at most 3.5% and moves completion by at most 4.5. Their explanation: "Chain entrusts the policy to the same handoffs that lose the constraint" (Z. Xu et al., 2026). That warns against a misreading of my own rule. It is a ceiling to check against the source, not an instruction to the writer, who may narrow far too much.

The price

The paper reports a safety-utility trade-off that any recommendation has to answer. All figures are its own, for typed incremental memory.

The authors say better writers tended to improve both rates, so the trade-off comes from the mitigations and not from model choice: an accurate record serves safety and capability alike. Every defence here pays somewhere, and rebuilding, the best of them, works because it goes back to the raw history. My gate goes further back, to the ledger.

My proposal has a price too, and I have measured none of it. narrowing_can_lose_utility shows the rule is one-sided: a summary that lost the filing permission passes, the gate refuses, and the ledger would have said yes. An act-level check removes that refusal only if the agent still attempts the act, and an agent whose memory lost a permission may never try. Non-progress is a harm of its own, the subject of Never Breaks a Rule, Never Finishes.

Erasure across derived assets

Information relating to an identifiable person is personal data under UK GDPR Article 4(1), and a summary of a summary still is, if it still relates to one.

Compaction's second defect lies here. When two memos merge, authority must go down and provenance must go up. meet_narrows_left and meet_narrows_right prove that the merged warrant narrows both parents, where the second needs the holders to match. compact_keeps_honest proves that a merge taking the union of sources stays honest [every source its text draws on is declared], for every pair of honest memos. A size-bounded writer is inclined to do the reverse on both. The information-flow half has a long lineage, including Dorothy Denning's lattice model (Denning, 1976). The only new part is that one compaction step must do both, in opposite directions, on one record.

honest_erasure_complete proves that for every store of honest memos, erasing by source leaves nothing carrying that source. lossy_survives_erasure is the counterexample: a rollup that kept its text and dropped a parent's source survives the sweep while still carrying the advice. honest_rollup_over_erases shows the other cost: the honest rollup goes whole, taking the letter's content with it, and must be rebuilt. My model takes carries as given. In a real system that is the hard part. Runtime data-flow tracking, as in CaMeL (Debenedetti et al., 2025) and Fides (Costa et al., 2025), is the serious route, and a model rewriting prose is where such labels are hardest to carry.

GateMem is the measurement to read alongside this: across its baselines, retrieval-based and external-memory methods "still leak unauthorized or deleted information" (Ren et al., 2026). The ICO's Tech Futures report, which describes itself as "early thoughts" and which the ICO files under research and reports, records that inaccurate information in an agent's memory "is likely to have a significant effect across multiple decisions", and that complexity "could make it harder to determine the source of personal information" (ICO, Tech Futures: Agentic AI).

Here is how I map the obligations, all from UK GDPR as shown on legislation.gov.uk, with no statement about the EU text. The right-hand column is what no theorem reaches. Ashdown Ltd, being a company, is not a data subject; individuals named in its advice would be. Yesterday's Permission covers Articles 17(1)(b) and 19 on withdrawal.

A memory store run by a vendor is processing by that vendor: Art 28(3)(a) names transfers to a third country as within the instructions, so a transfer analysis must cover the store as well as the model call. And none of this makes a system "compliant". A passing check is machine evidence about a record, and whether the law is satisfied is a legal judgment.

Who can cheat, and what breaks

A rule that moves the decision to a ledger moves the target to the ledger.

• Compromised or careless ledger. Whoever can write it holds all authority. A gate that trusts a wrong ledger is wrong with a proof attached. A bad entry shows up only if ledger writes go to a log the writer cannot alter and someone else reads it, and nothing in this chapter provides that. J. Xu's guarantee likewise assumes intact platform metadata and leaves "social-engineered genuine confirmation" out of scope, and so does mine. Who may enter a grant is the question of Who Gets to Write the Specification?.
• Bypass. The gate binds only the tools routed through it. A general shell reaches what it does not see.
• Wrong record type. The writer may store "the partner said the client is fine with this" as a fact, not a permission. The executor then uses it to fill in arguments the gate permits. The rule does not see persuasion in prose, and permitted acts can combine into something forbidden, as Every Query Was Allowed shows.
• Incentives. A refused action is visible on the day. A false permission is invisible until something goes wrong, and then it may fall on someone else. I expect vendors to tune toward fewer refusals, which is my judgement and not a measurement.

The claim a buyer may repeat is narrow: if every side-effecting tool goes through the gate, each call is correctly typed as an act, confirmations reach the gate from outside the memory, and the ledger is right, no act occurs that the ledger refuses. In the model that is true by definition, since actGate is the ledger's own answer: the certificate certifies the act against the ledger and nothing beyond it. It does not say the agent is safe, that its memory is accurate, or that it will finish.

A corpus you can run

corpus_rule checks the rule's verdict on twelve samples, computed by the kernel. corpus_semantics checks an independent search over principals, actions, ticks 0 to 31 and two confirmation states for an act the record permits and the ledger refuses. Rule and search agree on eleven. On the twelfth, recorded by rule_stricter_than_semantics, the rule refuses a record that permits nothing extra. The check never reads the text column, and bridging text to record is the part I have not solved.

"As granted." is the sample to show a sceptic: two words, and depending on what happened yesterday, either a good record or false authority.

What exists and what does not

Proved generally in lean/BuildingInSteel/WarrantDrift.lean, for every warrant, memo store or chain as stated (no sorry, no declared axioms; #print axioms lists at most propext and Quot.sound): narrow_sound, narrow_refl, narrow_trans, store_sound (fixed ledger), drop_action_narrows, add_restriction_narrows, empty_record_passes, unrevoked_never_narrows_revoked, gate_sound, chain_narrows_root, meet_narrows_left, meet_narrows_right, compact_keeps_honest, honest_erasure_complete. no_memory_only_check is general in f over one fixed record.

Computed on one fixed case, illustrations or counterexamples and not general results: case_narrows_ignores_holder, case_narrows_ignores_revocation, laundering_formed, rule_blocks_laundering, ashdown_path_blocked, shorter_can_widen, write_check_goes_stale, whole_record_gate_overrefuses, rejected_write_keeps_stale, local_check_carries_drift, narrowing_can_lose_utility, ledger_access_escapes, pointer_follows_revocation, pointer_can_be_swapped, lossy_survives_erasure, honest_rollup_over_erases, the corpus results.

Sketched, not proved or measured: the two-job design as a whole; any effect of a gate on EAL-Bench rates; quarantine and re-checking when the ledger moves. Nothing here connects to a running system. The model-to-code gap is the subject of The Proof Passed. The Wrong Thing Ran.

Assumed and trusted: a ledger exists, is right, and is reachable (partitions are in Yesterday's Permission), the typed record reflects whatever the agent will rely on, a tool call reaches the gate correctly named as an Action, and the confirmed list is genuine. The last two are free inputs in my model, and neither is small: if the case-management line in my opening also defines what the filing pack contains, a send of the pack reaches the gate as sendExternally publicFiling and passes with the advice inside.

Not known to me: a published evaluation of a gate reading a ledger of grant scope and dates, on an authorisation-memory benchmark, with both rates. Checking records complements, and does not replace, work on why writers err.

Objections

"Better writers and rebuilding will fix this." The strongest objection, and the paper gives it real support: rebuilding improved both rates, and writer-side compute improved them too. Verdict: it reduces the rate and does not change the architecture. The hardest number is the paper's one-shot typed writer, which never sees the ledger and still reaches 1.5%, 0.6% and 0.3% unauthorised actions by reading the whole history. My claim survives because that history is, in the authors' words, "synthetic, ordered, complete", which real correspondence is not, and because rereading it at every change is a slower read of the source, whose output is still a copy, stale until the next reread. In the single-seed diagnostic above, a rebuild before the last two blocks left it no better. I would give up my third claim on seeing an incremental writer with neither ledger nor full history reach the figures in my first prediction.

"Your ledger does not exist. Grants live in emails." This is the most expensive point in the chapter, and the benchmark's closed-world ledger is a luxury many organisations will not have. Verdict: the absence is the finding. With no authoritative record of a grant, an agent's summary has become the only record. Start with the few acts that cannot be undone. I would change my mind if firms with no explicit record showed false-permission rates no worse than those with one, measured on real histories.

"Authority labels already work." Zhan's AuthMem-Bench reports automatically predicted labels cutting unauthorised actions from 16.9% to 0.0%, with benign success "essentially unchanged", and J. Xu reports no evaluated unauthorised high-risk action passing their gate under intact provenance. Half right. Those are real results, on controlled benchmarks, and they address the origin of a claim. Verdict: use them and do not stop there, since a correctly attributed record can still carry the wrong scope or a stale date, the corpus's "lost revocation" row. If an evaluation showed origin labels catching scope and lifecycle errors at the rate a ledger does, I would drop the distinction.

"This is capability attenuation, and twenty lines of Python would do it." Both true. Verdict: conceded. Ship it in whatever your gate is written in, and test it differentially against this file. The Lean earns its place by proving soundness and catching my own flawed first gate, not in your runtime.

"Then store a signed capability, not a pointer." The sharpest reply to my third claim. A macaroon gives "the inability for adversaries to remove caveats" (Birgisson et al., 2014, full paper), so a writer holding one can narrow it and cannot widen it, and the verifier needs a key and not a ledger. Warrant has no signature field, so no_memory_only_check does not reach this. Verdict: such a token is not a copy in my sense, because no model can rewrite it, and it defeats the laundered, extended-window and lost-restriction rows. Alone it does not defeat "lost revocation". Its authors say macaroons "excel at all four" common revocation strategies, among them very short-lived credentials and "external, authoritative state". Both ask a party holding current state to reissue or answer at use, which is my ledger in another form. I would drop the pointer for a token scheme shown to follow withdrawals as fast as a ledger read.

Goodhart, and what formalising loses

Publish a false-authority rate and expect it to be gamed. empty_record_passes is the limit case: for every warrant, a record permitting nothing passes the rule. A writer that remembers nothing scores perfectly, so any figure must come with the legitimate action rate, on matched pairs, as the paper reports it.

Formalising also removes something real. A partner's "deal with the usual filings" is open texture, which a good human agent reads with judgment. A typed record cannot hold that sentence without widening or narrowing it, and whoever writes the schema decides which. Some refusals will be cases where a person would rightly have got on with it. Who gains? Whoever can afford a ledger, and I sell to them. A small firm may reasonably decide the record costs more than the risk, outside the acts that cannot be recalled.

What to do on Thursday

If you run a firm, ask whoever runs your tools one question:

At the moment this agent sends something out, where is the permission read from, and could the agent's own memory have written it?

If the answer is the prompt, the context or the memory, that is the finding. A real answer may mean building a record you do not have and accepting some refused actions.

If you build agents:

1. Keep grants in a store the memory writer process has no write path to, enforced by operating-system or container permissions, not by a prompt.
2. Route every side-effecting tool call through a small deterministic check against that store.
3. Store pointers in memory; label any cached description as a hint.
4. Make compaction take the union of sources, and carry restriction fields through deterministic code and not through the model. Event-based memory did the like and paid for it above, so measure legitimate actions.
5. Run the published benchmark on your writer, at EAL-Bench, which its authors call open source.

Predictions

1. By 31/12/2027, no published run on EAL-Bench or a declared successor will show incremental typed memory, with no rebuild, and with neither the ledger nor the full history available to writer or gate, reaching at most 2% unauthorised actions and at least 95% legitimate actions in all three domains. Refuted by one such result, which would also refute my third claim.
2. By 30/06/2028, a public incident report, regulator decision or judgment will attribute an unauthorised act by an agent in an organisation to a permission or restriction altered by the agent's own memory or context compaction, with no attacker involved, in an incident occurring after this chapter's date. Refuted if a search at that date of ICO and EDPB decisions, BAILII and the AI Incident Database finds none.
3. By 31/12/2027, no ICO guidance, including the agentic AI guidance its plan lists as in drafting, will state whether erasing a source reaches a summary derived from it in an agent's memory. Refuted by any ICO guidance text giving either answer.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.