Investigate mutation testing: SAFE proves executed, not asserted

[omsherikar]

Problem

SAFE proves a changed statement executed. It does not prove any test would fail if that statement's behaviour changed. A line inside a test that never asserts on the result counts as covered and earns SAFE.

This is the largest remaining false-SAFE surface, and unlike the others it is not a bug in a rule — it is the limit of what line coverage can tell us.

Evidence this is real, not theoretical

From this project's own hardening history, recorded in docs/verification/verdicts.mdx: Jinja2's truncate filter guards its early return with if len(s) <= length + leeway. Change <= to < and behaviour genuinely changes at the boundary. All 911 tests still pass, the changed line is covered, and the verdict is SAFE.

That verdict is correct about what it claims and is still not proof. Boundary conditions are exactly where suites are thin.

Why it matters now

Every other false SAFE closed in #110 and #109 was about which tests ran. This one is about whether the tests that ran would have noticed. It is a strictly larger hole than any of them, and it is the honest ceiling on the product's central claim.

What this issue is

An investigation, not an implementation. Mutation testing is the only technique that answers "would a test have failed?", and nobody has made it cheap enough for a per-commit gate. Before any code, this needs a decision on whether a version of it is affordable and honest enough to feed a verdict.

Questions to answer with numbers, not intuition:

1. Cost. What does mutating only the changed statements (not the whole file, not the repo) cost in wall-clock on a real repo? The changed-statement set is already computed in src/verify/coverage-attribution.ts, so the mutation surface is naturally bounded in a way general mutation testing is not.
2. Sampling honesty. If we mutate a sample rather than every changed statement, what may the verdict claim? A sampled pass is not a proof, so it likely cannot earn SAFE on its own — it may only downgrade. Is a rule of "surviving mutant → cannot be SAFE" both affordable and sound?
3. Which mutations. Boundary operators (<= → <), arithmetic, boolean negation, return-value replacement. Which classes catch real regressions per unit of runtime?
4. Verdict shape. Does this become a fourth gate, an input to fusion, or an advisory field? A surviving mutant is evidence of a weak test, which is a different claim from "this change is unsafe".
5. Timeout and flake interaction. Mutants that hang are common. The tests gate already has flaky-retry logic; mutation runs would need their own budget.

Acceptance criteria

1. An ADR recording the decision, with measured numbers for question 1 on at least one real repository, not an estimate.
2. An explicit answer to question 2, since it decides whether this can ever strengthen SAFE or only ever weaken it.
3. If the answer is "not affordable", the ADR says so plainly and docs/verification/verdicts.mdx keeps stating the limitation rather than implying it is solved. Closing this as wontfix with a recorded reason is a legitimate outcome.
4. If affordable, a follow-up implementation issue with a red-first fixture: a change that passes the suite, is fully covered, and is caught by a mutant.

Non-goals

• General-purpose mutation testing of the whole repository. The bounded surface is the changed statements.
• Replacing coverage. This would be additive evidence, not a substitute.
• Shipping anything in the 0.4.x line. This is a research spike.

Verdict integrity

The verdict at risk is SAFE, permanently and by construction. Nothing in this issue makes a verdict worse; the risk is the opposite — that a cheap, unsound version of this makes SAFE look stronger than it is. Any rule that lets a sampled mutation pass strengthen a verdict must be rejected.