Proofload: A Refusal That Offered an Override That Also Refused
Part 6. A local viewer, error visibility, a gate that refuses underpowered designs before they are paid for, and a research read that overturned the reasoning behind a decision while leaving the decision standing. See Part 5: The Stopping Rule Fired and the Third Arm Never Launched.
Sep 6: A page that renders nothing it did not compute
The viewer serves one pair of runs as a local page, read-only on loopback, with no network requests of any kind. The rule the whole packet hangs on is that the page prints no number it formatted itself. Everything numeric arrives pre-formatted, produced by the same helpers the report uses, because a second formatter is a second thing to drift.
Two of the thirty-four mutants I ran against the shim survived. One moved a block to a place the spec named and no invariant pinned. The other bound a raw socket earlier than the tripwire that watches for sockets. The first got an invariant. The second is now written down as a named non-observable, so nobody reads a green suite as proof that the CLI opens no socket.
Sep 6: Every stored arm reports zero errored rows
The next packet made run-level error counts visible: totals per run, errored rows per cell, and a stated reason for every hole in a grid.
Measuring it produced a sentence worth keeping. Every one of the stored pilot arms tallies zero errored rows, including the arm that died with every single episode crashing on an empty provider balance. That arm had no errored rows because crashing was an outcome, and error visibility never reads an outcome’s name.
Which turned into the repo’s first docs page, one sentence long: an outcome names what happened to the system under test, never what happened to the instrument. The worked example is that arm. Legal outcome, well-formed rows, a trace on every episode, time inside the horizon, every gate green, and the number would have been wrong.
The load-bearing part is why the analysis cannot rescue it. The diff reads a narrow frame and never touches metadata, deliberately, because decoding it is expensive at scale and because a comparison reaching into free-form metadata would mean different things for two runs with different metadata shapes. So the distinction has to live in the outcome label or nothing downstream can see it.
Sep 6: The default test discards the pairing
The pilot’s README recommended the unpaired test on runs created as pairs. That was two defects, and they are separable: a docs bug, fixed in a line, and a question about the CLI default, which is not.
Switching the default when the runs happen to share a salt would silently change the test a user gets between two invocations that differ only in how the runs were created. That is its own trap. So the tool warns instead, under its own warning class, so a CI that wants this as a gate can turn exactly that one into an error without erroring on everything else.
The mutation pass found the thing worth reporting. The mutant that matters, silently switching the method when the runs are pairable, is caught by 23 tests, 20 of them frozen oracles written before anyone thought about this problem. A switched method changes cell counts everywhere, so tests that were aimed at something else catch it for free.
Also found and deliberately not fixed: the headline prints “paired” as a fact about the two runs, immediately after naming the method that discarded it. It reads as though the analysis was paired. Moving it moves frozen rendered bytes in three oracles, so it is an amendment session and not a queue item. A test now pins the current wording, so the conflation is recorded rather than merely noticed.
Sep 6: A gate for underpowered designs, and the message it prints
The pilot’s real lesson was that the worst-case detectable effect had been printed before a dollar was spent and read twice without being acted on. So the pre-flight became a refusal. A design that cannot resolve better than the default threshold is refused before anything is planned or written, with an explicit override for someone who means it.
Two findings contradicted the specification and got pinned rather than worked around. “Strictly decreasing in N” is false, because the function returns the largest possible increase when even that is undetectable, so every tiny design reports the same saturated value. And “before planning” is not observable, since planning writes nothing; what is observable is before anything is written, so that is what the test asserts.
The third is the one I keep telling people about. The override the refusal message names does not work. The message computes a value that would accept the design as it stands, then prints it rounded, and the rounded value refuses again. The packet’s one interaction failing at its one instruction. The invariant now requires that whatever the message offers must itself pass the gate.
The threshold behind the gate is still the weak part, and the spec says so rather than hiding it. Nothing has yet cleared that gate for the right reason.
Sep 6: The read that falsified its own conclusion’s reasoning
A decision made a week earlier set a default for how failures get grouped. It was the weakest-sourced decision on the board, and it rested entirely on a research session whose record no longer exists. Six later decisions cite that record.
So it got re-run first-hand, with every claim tagged as read-from-source, from-memory or inferred, and the job stated as challenging the decision rather than confirming it. Fifteen real systems read at source.
The premise turned out to be false. The thing the decision assumed was rare is common.
The decision survives anyway, for a reason it did not originally give, and it owes two amendments to say so. A survived decision with a falsified rationale is a strange artifact to write down, and it is exactly the kind of thing that gets quietly re-litigated in three weeks if nobody does.