Enterprise / Notes / Falsifiable proofs
Engineering note
A proof that cannot fail is worthless.
Every organization has a test that has been green for three years and guards nothing. It passes when the system works and it passes when the system is broken, and nobody notices, because a guard that passes both ways is a false statement everyone trusts. When the product is the guard, that failure mode stops being an embarrassment and becomes fraud.
The specific danger of a verification product
Our proof says a modeled replacement matches recorded reality. There is an obvious way to build that badly: make the comparison lenient, let ambiguity resolve toward agreement, and ship something that says PASS for every customer on every estate. It would demo beautifully. Nobody would catch it for a year — because a PASS is exactly what everyone in the room is hoping for, and confirmation bias does the rest.
So the property we actually have to hold is not "the proof passes on good estates." It is "the proof fails on bad ones, for the right reason." That is a testable property, and we test it directly.
Mutation testing the harness
A mutation test breaks something on purpose and asserts the guard notices. Ours seed one realistic corruption at a time into either the model or the history, then require two things: the verdict flips to DIVERGED, and the specific finding category is populated — because a proof that fails for the wrong reason is only accidentally right. Then the untouched baseline is re-proven, to be sure the harness has not simply become a machine that says DIVERGED.
| Seeded corruption | Real-world analogue | Required finding |
|---|---|---|
| Drop one dependency edge from the graph | A dependency the model missed | missing — jobs history ran that the engine never reached |
| Flip a job's recorded status to FAILURE | A night that went badly | status_mismatch, plus containment_break for what ran downstream |
| Move a start time before its prerequisite ended | A force-start, or a wrong dependency | order_finding, naming both jobs |
| Append a downstream job to a failure night | Somebody released the hold at 3 a.m. | containment_break, naming the job |
| Remove a job's history row entirely | An incomplete export | unexpected — the engine would run what history shows idle |
| Add a job history knows and the model does not | A chain outside the modeled slice | Coverage gap; the day cannot pass |
Beyond the hand-written cases, a generator builds twenty-five random job graphs with matching clean histories — all must PASS — and then the same twenty-five each carrying one seeded violation — all must DIVERGE. It is deterministic from a fixed seed, with no wall-clock anywhere, so a failure reproduces exactly rather than "sometimes on Tuesdays".
All of it runs in continuous integration on every change, alongside a gate that executes the real command-line tool against a deliberately corrupt fixture and fails the build if the exit code is not 2. If our proof ever loses the ability to say no, we find out before you do.
Check our work in about a minute
Do not take the previous section on faith — the entire point is that you should not have to. Run a proof that passes, then lie to it:
# 1. a clean window — expect PASS, exit 0
handeware-prove ./estate/wire_eod.jil --history ./history.csv --out ./proof-clean
# 2. append one lie: a job that "ran" downstream of a failure
cp ./history.csv ./history-lie.csv
echo "WIRE_EOD_GL_POST,2026-03-10,SU,20:00:00,20:04:00" >> ./history-lie.csv
# 3. re-prove — expect DIVERGED, exit 2, naming that job
handeware-prove ./estate/wire_eod.jil --history ./history-lie.csv --out ./proof-lie
echo $?If step three does not diverge and name the job, the tool is broken and you should stop using it — including on our own published artifacts, which are exactly this experiment run in public: the passing proof and the diverging one.
Where this discipline came from
Not from theory. Our engineering rules were each bought with a real failure: a pipeline that reported success because output was piped into another command and the exit code was swallowed; a verification that passed against source while the shipped artifact was stale; guard tests that passed in both directions. The rule that survived is the one that applies here — break the thing it guards and watch it fail, then restore it and watch it pass. Anything less and you have a green checkmark, not a guarantee.
Which is the whole business, really. Anyone can produce a document that says PASS. The question a control function should ask any vendor holding one is simple: show me it saying no.
See both verdicts
The same estate, one appended lie apart. Published together, on purpose.