Tagged verification
18 write-ups.
How a Pluralisation Rule Broke a Correct Answer
A planner answered `movies` for a request containing the word `movie`. The generator singularised that to `movy` and its own checker then rejected the result. Two candidates round-trip and the order decides, and the same two words defeat both obvious repairs.
Taking the Language Model Out of a Build Planner
Over 88 requests, with everything downstream held constant, the model's plan rescued zero rows an empty seat lost, under all four ways of scoring the run. The one reading in which it looked resolved was resting on two rows the scorer could not see.
A Ceiling That Was Measuring My Test Harness
The headroom over nine build configurations came out zero, and then zero again. The first zero meant eight of the nine were invisible to the driver; the second, from 1,584 builds through a driver that reaches all nine, means they return the same verdict on all 88 requests.
Pinning What a Function Answers Across Rewrites and Time
A pin on a nondeterministic function fails at random on the next machine, and the blame lands on the pinning tool. Every candidate goes through nondet first; the committed control turns the gate off, changes not one byte of the tree, and asserts the check goes red anyway.
Finding Duplicate Functions by Executing Them, Not Reading Them
Two functions agreed on every rung of the input ladder and were not the same function; one character, ½, turned same into differs with a witness. The guard exists because agreement is cheap: constants, projections and copies agree with everything, and each mistake was made before it was guarded.
A Check With a Zero Denominator Reports Clean
A JUnit file reading tests="50" skipped="50" is a green run of nothing wearing a total, so every parser here returns total and executed separately and the floor applies to executed. Thirteen mutations were applied to the source; the two that survived their first run were worth more than the eleven that were caught.
Breaking CI Guards on Purpose to Prove They Can Fail
A fix I believed in was proved a no-op by the tool auditing itself: mtime invalidation has one-second granularity and the edit cycle is milliseconds, so stale bytecode looks fresh either way. PYTHONDONTWRITEBYTECODE is the guard actually holding; the surviving mutation corrected the README.
An Exit Code Cannot Say Whether Anything Happened
go test on a tree with no test files prints [no test files] and exits 0, measured rather than assumed. didrun wraps a command, demands evidence it did something, and returns four states instead of one number; the committed control asserts that 0 passed satisfying the expected pattern still scores as did-not-run.
Proving the Tree Came Back After Breaking It on Purpose
finally does not run on SIGTERM, and a restore that ran is not a restore that worked. The suite kills real children: a try/finally harness leaves the mutated file on disk, the guarded one comes back byte for byte, and SIGKILL defeats both, so the last check lives one process out.
A Determinism Check Has to Leave the Process
Set iteration order is stable inside one Python interpreter and different in every new one, so the repeat-it-twice check reports deterministic every time. nondet probes in fresh processes instead: 9 of 9 nondeterministic fixtures caught, 0 of 10 deterministic ones falsely flagged.
Ten Packages, One Rule: A Check Must Be Able to Fail
Eight of the ten went up in one day, extracted from a year of measurement work in which the thing lying was usually the instrument, not the code. Each package encodes one way a green check can mean nothing, and each commits a named test that would report its own premise wrong.
What Mutation Testing Frameworks Do When a Timeout Kills Them
I expected a kill to leave all four with a mutated file on disk. Three of them never write a mutant into your tree at all, and the fourth is left dirty by an ordinary SIGTERM, which is a gentler signal than the one I built the suite to test for.
When a Test Suite Rejects a Correct Program
Eleven of twenty-one operations never passed my frozen checks, and I wrote that up twice as a limit of the generator. A wrapper that only re-expressed each program's own stdout repaired 90 of 102 failures, changing no algorithm.
A PDF Exporter With No PDF Library
PDF wants JPEG bitstreams verbatim and zlib-wrapped deflate for everything else, and a browser already emits both. That makes the exporter 336 lines with no dependency, and moves the only place it can quietly break into the cross-reference table.
What a Browser Extension's Test Suite Cannot Reach
130 Node assertions passed while printing could not open a dialog at all, and choosing PDF silently broke the editor handoff. Both bugs sat at a boundary: my code meeting a browser API, and one internal stage meeting another. Pure-function suites are structurally blind to those.
Where Four Backends Stop Agreeing
My language compiles to C, WebAssembly, ARM64 and a bytecode VM, and correctness is defined as all four producing identical output. There are exactly four places where they are allowed not to, and casting an out-of-range float produces a different result in every one of them.
The Fixpoint No Test Suite Can Check
My language has 94 tests that run every program through four backends, compared byte for byte. All 94 run a program the JavaScript compiler built, so none can detect a compiler that disagrees with its own output. Self-hosting found three bugs the suite could not reach.
An App Generator That Verifies Everything Except Its Parser
A natural-language app generator whose verification sweep is exhaustive over everything except the part that reads English. The composer scores 100% on 810 cells built from feature sets; the parser that has to produce those feature sets scores 0.70, and nothing prints that number next to the other one.