Carr Digital

Analysis · August 15, 2026

The 20% that passed for free

A build guard reported a secret present in a bundle that did not contain it, and it was not flaky. IBM measured this failure at 20% of formulas on first runs, formal methods calls it vacuity, working programmers call it a tautological assertion, and it arrives in five distinct shapes.

Danny B. Carr, Jr.

On 2026-08-14 at 01:04:21 UTC, a build guard I wrote printed Sentry: DSN verified present in main.dart.js. It had grepped the compiled bundle for the secret it was given, and it found it. The string it found was roughly 51 characters long and it was not a DSN.

The guard was not flaky. It did exactly what it was written to do, against a real occurrence of the exact string it was handed. It was answering the wrong question.

That distinction is the whole subject here, and it matters more than it sounds. A flaky check invites a retry. A check that answers the wrong question invites a rewrite, and until somebody notices, it invites nothing at all.

If you operate a check that has never failed, you do not know whether it works. A check that passes because the property holds and a check that cannot fail produce identical output, and nothing in that output separates them.

This has a name. It has a detection algorithm, an industrial measurement, and a date, and all three are older than most of the tooling I run.

Twenty percent, on the first run

Four researchers at IBM’s Haifa Research Laboratory named the problem and built an algorithm to detect it: Ilan Beer, Shoham Ben-David, Cindy Eisner, and Yoav Rodeh. Their paper was received in May 1998 and ran in Formal Methods in System Design in 2001. The word they chose is vacuity, and a formula that passes for a trivial reason is vacuously valid.

Their canonical example is one line: AG(request -> AX ack). Every request is followed by an acknowledgment. It holds in a model that never issues a request. The formula is valid, the tool reports success, and the property you cared about was never exercised.

The paper opens on why this is worth an algorithm:

The ability to generate a counter-example is an important feature of model checking tools, because a counter-example provides information to the user in the case that the formula being checked is found to be non-valid. In this paper, we turn our attention to providing similar feedback to the user in the case that the formula is found to be valid, because valid formulas can hide real problems in the model.

Then the number, which is the part I keep coming back to:

Several years of experience in practical formal verification of hardware at IBM [3] have shown us that during the first formal verification runs of a new hardware design, typically 20% of formulas are found to be trivially valid, and that trivial validity always points to a real problem in either the design or its specification or environment.

One formula in five, on first runs, written by people doing formal verification of hardware for a living. Not people cutting corners. And every one of those trivial passes was covering something real.

Working programmers found the same thing and gave it a different name. Mark Seemann called it a tautological assertion in 2019, and his framing is the shorter one: “It’s surprisingly easy to write a unit test assertion that never fails.”

Formal methods says vacuity. Practitioners say tautological assertion. The two literatures do not read each other, which is most of the reason this keeps arriving as a surprise to whoever it happens to next.

It happened to me five times in six days, and no two of them looked alike. Sorting them turned out to be the useful part, because the diagnostic is different for each.

It asserts a proxy, not the property

Back to the build guard. It was written to close a gap where a compile-time flag was assumed to have reached the compiled output, which is a good instinct and the right rung to climb. Asserting the input is not asserting the artifact, so the guard greps the artifact.

The trouble is that grepping the artifact for a secret proves the secret is in the artifact. It says nothing about the secret being the thing it claims to be, and the value in that repository secret was not a DSN.

I could not read the secret back, because they are write-only by design, so the diagnosis had to come from somewhere else. It came from byte counts. With a real DSN the bundle is 5,352,229 bytes. With the old value it was 5,352,185, and no source changed between the two commits. The DSN is 95 characters and the bundle grew 44. That puts the old value at roughly 51 characters and means it was genuinely compiled in, exactly as the guard reported.

The fix is one rung, and it is cheap: check the shape before you check the presence. If it does not parse as a DSN, fail before building. Validate the input, then assert the artifact.

I have written this shape into an article on this site before without recognizing it. Across 88 measured cells of post-quantum certificate chains against real client stacks, parsing never fails. Every chain parses, in every stack, including the ones that cannot validate or handshake with it. An inventory tool that reports “the certificate parses fine” is asserting a proxy for “something in your fleet can use this,” and the two come apart completely. That tool has a 100% false-pass rate on the question anyone actually cares about. It looks healthy the whole time.

Google’s SRE book has the tidiest phrase for the general case, in chapter 17. Describing a system test that passes while the corresponding configuration test fails, it says the result “is valid hermetically, but not operationally.” The test was correct. It was correct about the wrong world.

The diagnostic. Write down the property you need in one sentence, with no “and” in it. Then read what the check actually tests. If those are different sentences, you are testing a proxy, and the only question left is how far apart they can drift.

It fired once where it needed to stand

On 2026-08-12 I made a repository public. It has a PREPUBLICATION-AUDIT.md, which exists precisely to catch material that belongs nowhere near a public repository. The audit ran. It passed. It was correct.

The next day I added a scope document to docs/upstream/ and pushed. It named a private individual five times, and it was live on a public repository for eighteen minutes.

Nothing in that repository, its workflow, or git checks a file added after the audit. The audit was an event where the risk was a condition. There is a second half to why it was easy to miss: adding a document to an already public repository does not feel like publishing. It is one git push, identical to every other push that evening.

The same shape, wearing different clothes, two days later. A re-run on 2026-08-10 reminted a set of certificate chains, which gives every certificate new keys, which moves ECDSA signature lengths by a byte or two because DER prepends a zero when the high bit of r or s is set. I wrote a document recording that the numbers had moved. That document was correct, on the day, and it is still correct.

Two prose tables that quote those numbers were not updated. They shipped stale into a public release with a DOI on it, and the only thing that caught them four days later was checking a figure by hand before quoting it to a maintainer in a public issue. Recording a change is not propagating it.

The diagnostic. Ask what happens to the file added tomorrow. If the answer is nothing, you have a certificate about the past rather than a gate, and it will keep looking like a gate indefinitely.

It says success it never earned

This is the loud family, and it is loud only in retrospect.

My dashboard’s deploy script printed a green deploy and shipped the previous content. Its runbook lists the notes sync as step one and then says to prefer the script over the manual sequence. One grep settles it:

grep -n 'sync-notes' scripts/deploy.sh     # no match

The script never called it. Read together, the documentation was an instruction to use a script that silently omits its own first step.

A measurement harness printed 10 for the handshake message length in six different cells. Six identical plausible numbers, from a two-stage extraction where the second stage matched the letter a inside the word “Handshake” before it ever reached the hex value. 0xa is 10. That is the loudest possible tell, a constant where the input varied, and I still nearly published it.

Three of four new tests for a style hook passed on the first run. The block above them changes directory, so the fixtures landed one level deeper than the hook was pointed at, the hook exited on a missing file, and every clean-case assertion passed on empty output. The fourth test was the one written to fail. It is the only reason I found out.

And the cheapest one, which costs nothing to internalize and will save an afternoon eventually: rg honors .gitignore by default. Searching a vendored tree that sits under an ignored path returns no matches, cheerfully, and an empty result means “nothing matched” and also means “I never opened a single file.” Nothing in the output tells you which. Use --no-ignore, or reach for grep.

In every one of these, a passing result and a broken result are the same observation.

The diagnostic. Make it fail on purpose. This is not a discovery on my part; deliberately injecting a fault to prove a check can detect one is mutation testing, which has been studied since the 1970s and which Facebook wrote up at industrial scale in 2021. The technique is free. Every clean assertion I now write sits beside one that must fail on the same machinery, in the same run, so that a clean result carries information.

The discriminator that cannot change

The first three are checks asserting the wrong thing. This one asserts exactly the right thing and still cannot fail, because the value it reads is identical on both sides of the change.

I was promoting a release to production. The plan was to merge, then confirm the web deploy by fetching version.json and reading the version back, which is the correct check and the one my own notes tell me to use.

The release was dependency-only. The version string was 1.1.17+120 on both branches, because upgrading a router package changes the bundle without touching a number that only moves when a human edits it. So version.json would have returned 1.1.17/120 before the merge and 1.1.17/120 after it. It would have passed if the build succeeded, passed if the build failed, and passed if the platform never built at all.

The tell is not in the check. It is in the diff. A build hash moves on every change; a semantic version moves only when somebody edits it, which is precisely why the second one is the one that quietly stops discriminating.

Two fixes, and the first is nearly free. Capture the baseline before the change, so one fetch into the scrollback turns a pass into a before and after. 1.1.17/120 then 1.1.18/121 proves a deploy. 1.1.18/121 on its own proves somebody looked at a page. Then make the discriminator move: bump the version deliberately, as its own step, rather than shipping changed code under a number two app stores already publish. That bump was not bookkeeping. It was the thing that made the check capable of failing.

The diagnostic. Before trusting an identifier, ask whether this particular change moves it.

The condition nobody can evaluate

The first four run and report the wrong thing. This one never runs, which is why it is the quietest member of the family.

I deferred a feature behind three re-open triggers, which is the right pattern and I would do it again. Trigger one read: web-only users miss check-ins at a meaningfully higher rate than mobile users. That is the correct property. It is exactly the fact that would justify building the thing.

Nothing in the system collects a per-platform miss rate, and nothing was scheduled to start collecting one. So the trigger sat at “not fired” for a week while its honest state was “unevaluable.” From outside, those two are the same sentence, and one of them means the risk is low.

The enabling cause sat one layer down. A CSV exists to accumulate weekly history, its own header says to run it from cron, and it holds exactly one row, dated 2026-06-21, with no crontab entry behind it. The file existing is what made history look like it was accumulating.

This is not the audit that fired once, and the difference is worth keeping straight. An audit that fired once has stopped standing. An unevaluable trigger stands permanently and does so faithfully. It has no input and no reader, so it resolves to a permanent negative, and a permanent negative reads exactly like “fine.”

Monitoring solved this decades ago and gave it good names. A watchdog alert, also called a dead man’s switch or a heartbeat, is an alerting rule that is always firing. It routes to an external service on a short repeat interval, and that service is configured to expect a notification every few minutes and to raise an alarm when one stops arriving. The design inverts the signal so that silence is the failure. Nobody carried that inversion out of monitoring and into governance, where deferral triggers, release gates, and annual reviews live.

The fix here was to replace a wish with a number the database already holds: count armed switches whose owner has no registered device. It was 0 on 2026-08-15. It goes nonzero the moment the situation the trigger describes actually exists. Same intent, evaluable in seconds.

The diagnostic. Write the query before you write the trigger. If the condition cannot be expressed as something runnable today, against data that exists today, it is a wish. Then run it once and record the value, because a trigger with no recorded baseline is the discriminator problem waiting to happen.

What I changed

Five rules, in the order they have earned their place.

  1. Make it fail on purpose. A detector that has never seen a planted defect is untested, whatever its pass rate says.
  2. Assert the property, not a proxy. Shape before presence, input before artifact. Validate that the thing is what it claims, then that it arrived.
  3. Recurring risk gets a standing gate. If the failure can be reintroduced tomorrow, the check runs tomorrow. A hook, a CI step, a pre-push guard, not a document recording that somebody looked once.
  4. Anything that regenerates evidence touches everything quoting it. Recording a change is not propagating it.
  5. Absence of an error is not a pass. A path that can fail silently gets an explicit success signal, and a missing signal is treated as a failure.

None of this is clever and none of it is new. Rule one has a fifty-year literature, rule five is how monitoring has worked since somebody invented the heartbeat, and the failure itself was named, formalized, and given a detection algorithm in a paper submitted in 1998.

What is new each time is the disguise. My five arrived as a grep that matched, an audit that passed, a deploy that went green, a version string that did not move, and a condition nobody could read. Not one of them looked like the previous one, and every one of them printed something reassuring.

IBM measured 20% on new hardware designs, at a company doing formal verification as a discipline, with a tool built to find it. I have been counting mine by hand for six days. I have no reason to believe my rate is better.

Provenance

Measured here (Verified). All five incidents are mine, from 2026-08-10 through 2026-08-15, with dates and commits recorded at the time rather than reconstructed. The 5,352,229 and 5,352,185 byte counts were read from the built bundles. The 88-cell parsing result and the reminted-chain byte shifts are public with captured output and a DOI, in pqc-cert-matrix (DOI 10.5281/zenodo.21749600) and pqc-chain-selection (DOI 10.5281/zenodo.21911032). The rg behavior reproduces on any tree under an ignored path.

Read in the source, not measured (Reported). Every quotation above was taken from the document itself, downloaded and searched on 2026-08-15, not from a search result or a summary. The vacuity paper was read as the 2001 journal version; the 1997 CAV paper of the same work was not opened, so it is not quoted here. The mutation testing citation is used for the practice and its age, nothing more.

Mine, and labeled as mine. The five-shape taxonomy is my own sorting of my own incidents. The vacuity paper defines an “interesting witness” as a positive trace demonstrating non-trivial satisfaction, which is related to a negative control and is not the same construction, and the paper does not claim otherwise. Carrying the watchdog inversion from monitoring into governance is my framing, not a finding from the cited source. None of this is claimed as new; the literature named the problem decades before I ran into it, and the contribution here is the sorting and the receipts.

If I have something wrong, email the studio and I will correct it here, with a note saying what changed.

Sources