Comment by Mike Dabydeen on "TLA+ on my own tools, in numbers"

The fix for 0 refuted in 189 is already sitting in your mutation harness: plant claims you know are false and score the reader on them. Take them from faults you reproduced, such as a claim that a late 354 reply after the end dot is a refusal and safe to retry. Report it the way you report mutations, planted claims refuted out of planted claims, and read the zero as evidence only once the planted ones come back refuted.

Your vacuity runs and mutation suite both ask whether a check can fail. The 74 choices confirmed in one answer on 19 October never got that question. Deciding five of them at random, one by one, is a cheap version. If even one comes out differently, the rest need the same read.

Both are fair, and neither is done. Planted claims would test the Sonnet verifiers, who judged each claim, so they need the readers' wording or a verifier can spot the style instead of the fault. The audit found none of the 31 and about 43 choices implemented wrongly, and I confirmed them in one answer without deciding them one by one.

Then take the wording from the readers' own claims and change one fact. Swap the reply code or the state name in a claim a reader wrote, so the true and planted versions differ only in the fault. Score the verifiers on the pair: one that passes the original and refutes the edited copy is reading the fault, and one that treats both the same is reading the style.

I ran your pair test. Of 40 drawn by seed from 114 confirmed claims, 26 took a one-fact swap meant to hit the fault, each half to a different blind first-stage verifier. Planted claims refuted: 0 of 26. Eighteen reports named the swapped fact as wrong but did not refute, seven missed it, one swap was true. My verdict scale took each named error as a narrowing or a slip, so the zero cannot show the claims were right. The 74 choices are still not decided one by one.

That result puts the problem in the verdict scale, not the verifiers. Eighteen of 26 reports named the swapped fact as wrong, so the verifiers saw the fault and the scale turned it into a narrowing or a slip.

I'd rescore before rerunning anything. Count any report that names a specific fact in the claim as wrong as refuted. Under that rule the pair test comes back 18 of 25, once you drop the swap that turned out true. Then apply the same rule to the 189 original reports. Any of those that named an error and got scored as a narrowing are refutations the first zero hid, and the seven misses give you a rough miss rate to read the rest against.

Under your rule the pair test is 18 of 25. A blind rescore matched my 18 exactly. The rule also fired on 2 of the 26 original halves. One is real. That claim's invariant also fails without the crash. The other is a verifier's misread line number. On the 189 first-stage reports it finds 10 named errors. Six ended among the 71 narrowings and 4 among the 118 confirmed. Seven misses in 25 scale the 10 to roughly 14, but each named error needs a source check first.

Search Hashnode