What a Green Run Proves

A model-checking gate came back green, and the sentence that followed was “the model verifies.”

# The bad way: read the verdict, skip the loop that produced it.
make check-alloy   # → green

That gate’s loop excludes the soak roots and the legacy models by construction. Green says the roots it visited hold. It says nothing whatever about the roots it never opened — which is correct behaviour and an incorrect reading waiting to happen. The good way is one clause longer: green over the non-soak roots; the soak roots have their own target and it has not run.

A green run is evidence about the corpus the run visited, through the instrument that visited it. Both halves narrow the claim, and both are usually left implicit.

This page covers the instrument Checks That Cannot Fail does not: a gate, a suite, a script — the machinery that produces a verdict. The rule is the same one. A verdict that cannot come out otherwise is not a verdict.

Each section names how many independent witnesses it rests on, because a rule derived once and a rule derived three times are different kinds of claim, and this page would be a poor place to blur that.

A declaration that does not name its corpus cannot be failed

Two witnesses.

Two scans of one tree can disagree by construction and both be correct, wherever something changed between the representations they read.

One database index had three defensible descriptions: non-unique at creation, recreated UNIQUE under the same name, then renamed. Migration text and the live catalog give different right answers, and a claim that names neither cannot be contradicted by either.

This generalizes past SQL and past regular expressions. Any claim over “the code” where a build step, a generator, or a rename stands between two representations needs to say which representation it read.

State the corpus with the claim. A gate’s corpus is what its loop actually visits — which means its exclusions are part of its verdict. One model-checking gate excludes the soak and legacy roots by construction, so a green run there says nothing whatever about those roots. That is correct behavior and an incorrect reading waiting to happen.

A fixture generated from the artifact under test cannot witness a disagreement

Two witnesses.

Where a suite builds its schema, its fixture, or its expectation from the code’s own declaration, the two are equal by construction. The divergence the suite appears to guard against is unconstructible: control and subject are the same artifact.

The suite still passes, and its green reads as evidence for a property it structurally cannot test.

Derive the fixture from the other side of the boundary — the migration, the deployed schema, the published contract — or state plainly that the suite tests self-consistency rather than agreement.

Prove an instrument can fail before trusting its green

Three witnesses for the criterion; the exit-code shape below is verified twice.

Make the gate red on purpose before believing it green. Break the thing it guards, run it, watch it fail, put the thing back.

A standalone exit code and a wrapper that honors it are two different claims. A command that exits non-zero can still be reported as success when the recipe’s plumbing swallows it — a trailing echo, a || true, a pipeline whose last stage returns zero. This shape is verified twice, in different tools and by different mechanisms. A gate runner’s recipe ended in a bare echo, so the command’s non-zero exit was discarded by the recipe’s last line and the gate reported success. A build wrapper piped its output through tail, so the pipeline’s exit status replaced the build’s.

The positive form is the one to carry: a run without its own result line is not a verdict, whatever it exited. A build can die before emitting BUILD SUCCESSFUL or BUILD FAILED; a suite can die before printing its completion line. Read for the result line first, and treat its absence as “no answer” rather than as the answer the exit code suggests.

Where a gate prints a human-readable verdict alongside its real one, check which one is load-bearing. In the model-checking gate the readable grep is || true and cannot fail the run; the verdict rests entirely on the solver’s exit code. A reader watching the readable output is watching the half that cannot say no.

A shared fixed-name log cannot say which run wrote it

Three witnesses.

A tool that writes to a fixed path, run concurrently, produces a file no reader can attribute. The same defect has now appeared in a slot wrapper, a gate script and a Makefile.

The consequence is subtler than a lost file. In one gate, instance output and the display log are shared fixed paths across seven targets, so two concurrent runs in one tree corrupt each other’s readable verdict while the pass/fail stays correct. The run is right and its record is wrong, which is the harder failure to notice.

Give each run its own output path — a run id, a timestamp, a slot name — before running two of anything concurrently.

An identifier that names two things routes work to the wrong owner

One witness. Stated as a hypothesis rather than as practice.

Four separate sequences in one project numbered things A-nn. A finding reached the wrong stream because of it.

The fix that appears to survive is qualifying the namespace at the point of reference rather than renumbering the records: name the thing rather than its number when the reference crosses a boundary, since a label from another session’s scheme is not a label in yours. That is the proposed remedy, not a second witness.

This has been observed once. It is recorded here because the cost was real and the shape is recognizable, not because one instance establishes a practice.

Write the prediction down before the run

Two registrations and one counter-case.

A prediction recorded after the result is not a prediction. It is an explanation, and explanations fit whatever happened.

Before a long verification, write down what each part should report — which roots should be satisfiable, which counts should hold, what the run should not find. Register it where someone else can read it, then run. The value is not in being right; it is that a written prediction is the only thing a run can contradict.

A model-checking campaign did this before its gate: predictions per root, registered in writing first. The run agreed with most of them and disagreed with two, and the two disagreements were findings about the model rather than adjustments to the expectation — which is exactly the outcome an unwritten expectation cannot produce, because an unwritten one quietly becomes whatever the run reported.

The second registration was smaller and answers the obvious objection, that this only pays on large runs. A rule about when a generated manifest is regenerated at commit time was written down as a prediction before four commits, along with the reason and the observation that would refute it. It held four times. The cost was one sentence per commit.

The counter-case is the important one. That same manifest rule, in an earlier and wrong form, predicted correctly seven times in a row before it failed. Seven confirmations, and the rule was still wrong — because none of the seven was a case that could have come out differently under the correct rule. The discriminating case had already occurred and had not been recognized as one.

So the discipline has a second half: say what would refute the prediction, not only what would confirm it. A run that could not have contradicted you did not test you, and counting how many times it agreed measures nothing. This is the same rule as the rest of this page, turned on the expectation instead of on the instrument.

Sources

From the model-checking campaign on the Orders v2 Phase-III work; the submission is /workbooks/notebooks/domain-ontology/streams/minesweeper/parmandil-submission-2026-09-09.md. The index witness was read in operations at 55969958 and 578b8c9f, each of which carries the rename.

The gate anatomy was read from the manufacturing-ontologies working tree, where the Makefile is uncommitted — it matches no committed revision, so a reader checking it at ae31cc9 will not find the recipe described. Pinning it awaits that file landing. Stated here rather than glossed, because a page arguing that a claim names its corpus cannot leave its own unnamed.