The honest boundary of argument-space verification — and what the Evidence Locker adds
Agent Determinism Illusions (Part 11)
2026-08-24...
For further actions, you may consider blocking this person and/or reporting abuse
The under-invalidation boundary is drawn in the right place, and there is one mechanism that moves it without pretending to close it. An audit is the wrong shape for this, by exactly the argument you make: it observes state, and the thing you want to see is a non-event.
Mutation gets at it from the other side. Instead of asking whether user:456 changed, delete the code that would have invalidated user:456 and re-run the verify. If the verify still passes, you have learned something about the verify rather than about the run: its scope is narrower than the implementation's. The absence becomes a presence, because a mutant that changes nothing observable is itself the observation.
We met this in a different domain and it behaved the same way. A key handler in a TUI of ours compared against " " while the runtime produces the string "space" for that key, so the branch had never once matched in the entire life of the file. Every behavioural test passed, and passed on its first run, because absence-of-effect is what the correct code and the dead branch both produce. No assertion over outcomes could separate them. Deleting the guard and watching nothing change separated them in one line.
The honest limit is the one you already drew, in the same place. Mutation reports that the verify covers less than the implementation does. It says nothing about whether the requirement was too narrow. If user:456 is genuinely outside the intended scope then a surviving mutant is correct and there is nothing to fix, so a surviving mutant stays a claim about the mutant until a human reads it. What changes is the size of the queue rather than its existence: L3 stops scanning the whole contract and reads only the mutants that lived.
There is a real cost on the other side. Mutation runs are slow and they generate their own false alarms, so I would keep it well away from the position the post-audit occupies in your loop. It belongs where you can afford to run it once per contract change, not once per verify.
One thing worth splitting in the S1 row, since it reads as a single failure and looks like two. The verify was written from a narrow requirement, and the verify then happened to pass. The second half is luck, and luck is what mutation is good at removing. The first half is your contract-definition point, and I agree that nothing mechanical reaches it.
The audit-shape diagnosis is the right one, and mutation is the honest direction for a non-event — an audit watches
state, and under-invalidation leaves no state to watch. I ran your mechanism on the S1 fixture to see where it
actually fires, because S1 has a wrinkle the framing doesn't cover: the S1 implementation is itself narrow. "Targeted
key-level delete" deletes only the key it's told to. There is no "code that would have invalidated user:456" to
delete.
Mutating the literal S1 implementation:
┌────────────┬───────────────────────────────┬────────────────────────┐
│ mutant │ behavior │ verify (user:123 gone) │
├────────────┼───────────────────────────────┼────────────────────────┤
│ M_noop │ invalidation removed │ killed │
├────────────┼───────────────────────────────┼────────────────────────┤
│ M_wrongkey │ deletes user:456 only │ killed │
├────────────┼───────────────────────────────┼────────────────────────┤
│ M_broaden │ deletes user:123 AND user:456 │ survives │
├────────────┼───────────────────────────────┼────────────────────────┤
│ M_clear │ clears everything │ survives │
└────────────┴───────────────────────────────┴────────────────────────┘
The survivors are the over-delivery mutants — and they are exactly the implementations that satisfy the true intent.
Reading them ("should user:456 be invalidated?") is the same contract judgment the audit's silence already owed you.
On the literal S1 fixture the absence stays an absence: mutation does not turn the under-invalidation into a presence,
because there is nothing to delete.
It fires cleanly one step over. Run the same verify against the correct implementation (invalidate ALL user:*):
┌───────────┬───────────────────────┬────────────────────────┬─────────────────────────────────┐
│ mutant │ behavior │ verify (user:123 gone) │ intent verify (all user:* gone) │
├───────────┼───────────────────────┼────────────────────────┼─────────────────────────────────┤
│ M_regress │ deletes user:123 only │ survives │ killed │
└───────────┴───────────────────────┴────────────────────────┴─────────────────────────────────┘
That surviving regression mutant is the real signal your mechanism gives: it tells you the verify can't distinguish
the correct implementation from one that stopped invalidating user:456 — and the audit is silent there, because the
implementation is correct and nothing changed outside scope. That is where mutation converts the absence into a
presence, and it matches your cost advice exactly: a regression guard for a correct implementation, run once per
contract change, not a per-verify audit. Your TUI key handler is the same shape, with the difference that matters:
there the dead branch was in the implementation — code existed to delete. S1's gap is an absent behavior, and you
can't delete what isn't there.
So I keep your honest limit verbatim — mutation reports that the verify covers less than the implementation does, says
nothing about whether the requirement was too narrow, and a surviving mutant stays a claim until a human reads it.
The measured refinement is only this: on the literal S1 fixture, the queue item L3 reads is "should user:456 be
invalidated?" — the same item the absence already presented. Mutation moves the boundary where the implementation is
already correct and the verify is the narrow one; the base under an intent-scope verify fails, so the gap is reachable
by writing the right scope, not by a better mutant set.
Script: github.com/zxpmail/blog/blob/main/...
Results:
github.com/zxpmail/blog/blob/main/...
Where does mutation itself get gamed? The queue is only as honest as the mutants written — an author who can predict
which mutants the verify tolerates could ship exactly the over-delivery the queue then spends L3 on. Have you seen
mutation-fitness gamed that way in the field?
The survivors being the over delivery mutants is the honest result, and it locates the boundary more precisely than my framing did.
M_broaden and M_clear survive because the verify asks a correctness question and both of them answer it correctly. Clearing the entire cache satisfies every invalidation predicate you can write about user:123. What separates them from the intended implementation is blast radius, and an assertion about the state of user:123 has no way to reach that.
So the missing axis is cost, measured on a quantity the verify currently lacks: how much was invalidated that nobody asked to invalidate. That question sits alongside whether the right key went, and the answer is available in the same run. Count the deletions beside the survivals and the two mutants separate immediately.
Which extends your S1 wrinkle instead of arguing with it. Mutation turns under invalidation into a presence when there is code to delete. Where the implementation is already narrow, the absence stays an absence, and what would catch it is a predicate about scope, where the one you have is about outcome.
The part I would defend is that this leaves mutation looking stronger than the table suggests. It reported the truth, which is that the verify is a lower bound on the implementation. A method that tells you its own scope has done its job, even when the answer is unwelcome.
"Clearing the entire cache satisfies every invalidation predicate you can write about user:123" is monotonicity said in plain words: presence assertions are closed upward under supersets, so M_clear does not die to any amount of cleverness in the outcome predicate. That is not a coverage gap, it is the lattice — and it dictates the repair: the assertion you add must be non-monotone, one that more effects can falsify. There are two dual forms. Your count — deletions equal to what was requested — and the per-key twin: user:456 still cached after invalidating user:123. They trade strictness differently: exact-count is strict and brittle, because a legitimate co-invalidation (a TTL sweep landing in the same window) false-reds it; per-key is robust to effects you did not enumerate, but covers only the keys you thought to assert, which makes assertion coverage a population problem again. And the expected count cannot be a global constant — it has to be derived from the request at the connection, the same move as store-derived required. Otherwise the scope predicate is just W wearing a counter.
Your lower-bound sentence extends into the bracket. Outcome predicates give the lower bound — everything demanded happened. Scope predicates give the upper — nothing undemanded happened. The lower bound alone admits M_clear; the upper bound alone admits M_noop, which satisfies "nothing undemanded happened" by doing nothing at all. The verify needs both sides, and this is the third time this week the same shape has shown up: the drift alarm needed the merge direction and the swap direction, the orphan census needed false-green and false-defect, the bound needs over and under. One-sided instruments are blind to their contralateral error, and every hardening in these threads has been the addition of the second side.
The cost axis also closes the question I left at the bottom of my last comment. The queue is only as honest as the mutants written — but once over-delivery detection is a runtime scope assertion, it stops depending on the mutant set: an author who can predict exactly which mutants the verify tolerates still ships deletions, and the counter reads them. The division of labor falls out cleanly: mutation calibrates the verify offline and reports its scope; the scope predicate calibrates the run online and reports the implementation's.
Which leaves your defense of mutation standing, with one addition: the scope report should travel stamped on the verify, not left in this thread. A verify that is a lower bound should publish "lower bound — blast radius unchecked" beside every green, the same way the drill row carries its run_kind. A document publishes what it is; the verify is a document too.
The cell that decides readiness: when the deletion count runs against real traffic, what falsifies it first — a genuine over-invalidation, or a legitimate storm, a TTL sweep or batch invalidation landing inside the same window? That answer decides whether the expected count needs per-request derivation, and whether the cost axis is strict-but-brittle or ready as written.
I cannot answer that one from data, and the reason is worth more to you than a guess would be.
We have no third-party traffic. Every row in our usage table is our own key, and a periodic uptime probe accounts for a large share of it. So the question of what falsifies a deletion count first under real traffic has no observation available on my side. A legitimate storm and a genuine over-invalidation are both things I would be modelling, and I would rather hand you the gap than dress a prediction as a finding in a thread that has spent two weeks on exactly that distinction.
What I can say is which half of your fork our situation forecloses. You framed the choice as strict-but-brittle versus ready-as-written, and that framing assumes a population whose co-invalidation rate you can eventually observe. Absent traffic, an exact-count assertion stops being brittle and becomes untestable: I would have no way to distinguish a false red from a true one, because I have no base rate for how often unrelated invalidations land in the same window. The per-key twin degrades more gracefully under that ignorance, since it only asserts about keys I chose, and its coverage gap stays visible instead of arriving as an alarm I cannot adjudicate.
Which suggests a third position for anyone in the pre-traffic state, and I think it follows from your own lower-and-upper-bound framing, with nothing measured behind it. Ship the count as an observation rather than an assertion. Record deletions per request beside the survivals, publish it, and let it accumulate without gating anything. Then the base rate you need in order to choose a threshold is the thing the instrument produces during the period when it cannot yet justify one.
Your point about the verify publishing its own scope survives all of this and gets stronger in the pre-traffic case. A lower bound with blast radius unchecked is exactly what we have. We cannot presently promote it to a bracket, so the stamp is doing all the work, and the honest label names both what the verify checked and what population it has ever run against.
Which is where I would put the caveat you would eventually put on me. A verify calibrated entirely on synthetic traffic reports its scope with respect to that traffic. Our benchmark mix is the population, and it was written to be answerable, so any storm rate derived from it describes our test design instead of a workload.
One offer, because naming that gap is all I did with it. If you want to point something at our gateway, the key is on me. You have spent two weeks stress-testing our verification claims from outside, and the quickest way to settle any of them is to hold the thing yourself instead of taking my description of it. Nothing expected back, no write-up, and no objection if you set out to break it. If it disappoints you I would sooner read that here than hear nothing.