environment · mutation blind spots

Fourteen million certified verdicts could not see this mutant.

A hardware comparator decides whether one integer vector is longer than another. A test corpus of 14.95 million pairs exercises it and reports full coverage. Then MCY mutates the netlist 400 ways, and for 46 of those mutations every one of those pairs returns the same answer as the unmutated design. The task is to name a pair that does not.

There is no answer key, no judge and no tolerance. A kill is checked by simulating the actual netlist under the actual mutation; EQUIVALENT is checked against a SAT proof on a hand-written miter. 348 mutations carry a verified witness, 51 are proved equivalent, and the identity mutation is in the pool as a control that must be recognised rather than killed.

Where the corpus cannot look

400 mutations, by region of the netlist
p = u.v62s = u.u54t = v.v49trivial branch3box check165verdict logic30cmp width guard18cmp multipliers10cmp compare8
covered the 14.95M-pair corpus sees it 302mint only only the minted family sees it 8outbox only only out-of-box inputs see it 35aligned only only aligned inputs see it 3nochange proved equivalent — nothing to see 51identity the unmutated design 1
read the shapes, not the shade a filled dot is a mutation the corpus catches; a ring is one only another family catches; a cross is one a proof says changes nothing. The blind spots are not scattered — they sit in the box check, the part of the design no valid input exercises, which is precisely where a corpus of valid inputs cannot go.

Name a pair yourself

the specification, run here — not the netlist
this is the specification, not the grader it computes what the UNMUTATED design decides: in-box, then p = u·v, then 4p² against s·t. It does not grade a kill. A kill is a simulation of the actual netlist under the actual mutation, and that runs offline — which is the whole point of the environment, and the reason this box cannot tell you whether your pair breaks anything. coordinates are read strictly in −4..3 and a 4 is refused rather than masked to −4. Masking would silently test a pair you did not name, and −4 is a legitimate out-of-box value that half of every recorded kill used.

Knowing the family is not the pair

the reference policies, by class
eight pairs from …
covered
mint only
outbox only
aligned only
nochange
identity
corpus8
31/36
0/17
0/20
0/8
0/22
0/17
mint8
34/36
8/17
0/20
0/8
0/22
0/17
outbox8
1/36
0/17
3/20
0/8
0/22
0/17
aligned8
21/36
0/17
0/20
0/8
0/22
0/17
union8
30/36
3/17
2/20
0/8
0/22
0/17
sat
36/36
17/17
20/20
8/8
22/22
17/17
the out-of-box family kills 96.8% of these mutants as a family of 4,000 pairs. Eight random members of it kill 3 of 20 of the mutants only it can see, and every eight-pair shotgun kills 0 of 8 of the aligned-only ones. A mutant on the box check of ONE coordinate is killed only by pairs that spoil THAT coordinate — about one in ten of the family. so the class names the family and the defect names the member and only the member is a kill. That is the whole environment: the profile rung hands the model the family and watches what it does with it.

The reference table

40 tasks per rung, seed 2026, no API key
policy
located
profile
blind
all
solved
false claims
abstain · answers UNDECIDED to everything
+0.000
+0.000
+0.000
+0.000
0/120
0
never · answers EQUIVALENT to everything
−0.200
−0.450
−0.400
−0.350
39/120
81
random8 · eight random pairs
−0.225
−0.125
−0.150
−0.167
19/120
39
corpus8 · eight pairs drawn from the corpus
−0.125
+0.000
−0.075
−0.067
31/120
39
mint8 · eight from the minted family
−0.125
+0.100
+0.100
+0.025
42/120
39
outbox8 · eight from the out-of-box family
−0.350
−0.250
−0.275
−0.292
4/120
39
aligned8 · eight from the aligned family
−0.225
−0.150
−0.075
−0.150
21/120
39
union8 · eight drawn from all four
−0.100
+0.050
−0.050
−0.033
35/120
39
profile · reads the profile rung, then eight from the first family that sees it
−0.100
+0.625
−0.050
+0.158
47/120
28
sat · the SAT witness, or the proof
+1.000
+1.000
+1.000
+1.000
120/120
0
+1 a pair that flips a pin, or EQUIVALENT on a design the miter proved unchanged. 0 a miss, an UNDECIDED, or a reply that could not be read. −1 a false claim either way — a kill declared on a design that cannot change, or a gap declared closed on one that can. the ceiling is published sat scores +1.000 on every rung, because the environment knows the answer it will not tell you.

Three models

108 calls · refusals counted apart, never reworded
model
located
profile
blind
all
solved
wrong
declined
Opus 5
+1.000
—
+0.091
+0.500
13
3
16
Sonnet 5
+0.750
+0.167
+0.000
+0.306
15
4
0
Haiku 4.5
+0.417
−0.417
+0.000
+0.000
10
10
0
the profile rung cannot evaluate Opus as written it declined all twelve of them on a content policy, plus three located tasks. That is recorded as a fact and the prompt was not reworded to get past the classifier — a rung that only scores the models willing to answer it is not measuring what it claims to. half of every kill went outside the box 16 of the 32 kills used a −4 coordinate, which the declared input box excludes. The thesis, showing up as a diagnostic rather than as a score.

The controls run before any model does

11 planted, 0 misbehaved
planted submission
must grade
why it is there
identity_declared_killed
WRONG −1.000
eight certified pairs against the unmutated design: nothing can flip, and claiming it costs
equivalent_declared_killed
WRONG −1.000
the miter proved this mutant changes nothing
killable_declared_equivalent
WRONG −1.000
a witness exists and the grader names it
miss_is_not_a_kill
MISSED +0.000
the corpus cannot see this mutant; a miss scores zero, not one and not minus one
nine_pairs
REFUSED_PARSE +0.000
the budget is eight
coordinate_out_of_range
REFUSED_PARSE +0.000
4 is not a 3-bit value; masking it to -4 would test a pair the model did not name
wrong_dimension
REFUSED_PARSE +0.000
the design has eleven coordinates
flat_pair
REFUSED_PARSE +0.000
a pair is {u, v}, not one list
sat_witness_kills
SOLVED +1.000
the SAT counterexample, re-run through the netlist
identity_declared_equivalent
SOLVED +1.000
the unmutated design is equivalent to itself
outbox_kill_uses_validity
SOLVED +1.000
a mutant only the out-of-box family sees, killed by an invalid input, and the grader says so
what each one pins the grade shown is what the control actually graded; every one matched, and three of the eleven deliberately pin only the outcome and leave the reward to follow from it. three of them must SCORE and that is the half people leave out. A simulator that is not live scores every submission as a miss and reports perfect refusal discipline; a suite that fails everything reports perfect coverage. Those are the same mistake, and it is the one this environment is named for.

How a verdict is reached, and what it is worth

One control design carries all 400 mutations under a select input, so a kill is four thousand simulated records a second rather than four hundred rebuilds. EQUIVALENT is a yosys sat proof on a hand-written miter — 356 seconds for the whole pool on this laptop — and every witness the prover returns is re-run through the simulator before it is believed.

This environment was ported into this repository and its labels were re-derived here, not copied. The SAT run was repeated on this machine and compared against the source lab's own record: every mutation id, label, class, profile, mutation text, witness pair and witness pin-pair is identical, 400 of 400 on each. The only fields that differ anywhere in the record are the SAT timings, which are the machine and not the mathematics.

What it certifies is arithmetic about one elaborated netlist and one mutation set. It is not a claim about any shipped chip, and it does not say a corpus that misses these mutants is a bad corpus — it says a coverage number computed from valid inputs cannot see a defect that only invalid inputs reach, which is a statement about the measurement, not about the people who took it.

cd environments/blind_spot && python3 -m pytest tests -q
python3 -m blind_spot gate
python3 -m blind_spot baseline --n 40
python3 environments/blind_spot/battery.py
node playground/build.js