Runbook for #387 — deliberately break each line of vera/ and confirm a test flips RED. A surviving mutant is a test gap: either a weak test to strengthen or an equivalent mutant to annotate. This is the safety net under the #421 runtime decomposition and every future change.
A passing suite is necessary, not sufficient. The #680 audit found 8 green-for-the-wrong-reason tests in one 57-test battery; #734 had to mutation-validate its own harness. Mutation testing systematises that check.
Current baseline (soundness core): 80.8% caught, 2,038 survivors. The committed score lives in mutation-summary.csv and the README badge; the per-module chart and the full survivor inventory are attached to the baseline comment on #387.
Evaluated both on vera/obligations/ (Phase 0 spike, 2026-06-22):
| mutmut 3.6 | cosmic-ray 8.4.6 | |
|---|---|---|
| Throughput | ~7–8 mut/s (coverage-guided: runs only the tests covering each mutated line) | ~0.08 mut/s (re-runs the full test command per mutant — #498) |
| Working tree | copies the project to ./mutants/, source untouched |
mutates in place (apply → test → revert) — leaves the tree dirty if interrupted |
| Resume after a hard kill | verdicts persist as plain JSON; mutmut run resumes |
session SQLite; resumable |
The ~90× speed gap (coverage-guided selection) is decisive for a slow Z3/WASM suite, and the copy-based model is safer for multi-day runs. mutmut also sidesteps the stale-.pyc hazard of an in-place bespoke driver.
That hazard is real whenever you mutate by hand instead: when validating a test by breaking the code it targets (see TESTING.md), purge __pycache__ before re-running — a stale .pyc can serve the unmutated bytecode and false-green the mutant (this bit a hand-run oracle test during the v0.0.195 work; the kill was only confirmed RED after the purge).
pip install -e ".[mutation]" # pulls [dev] + mutmut + pytest-timeoutConfig lives in [tool.mutmut] in pyproject.toml. (Avoid setup.cfg — its list values split on newlines, not spaces, so a.py b.py becomes one bogus path. TOML arrays are unambiguous.)
mutmut activates a mutant in-process via an import trampoline. Tests that spawn a subprocess — test_conformance.py, test_cli.py, and test_browser.py all run python -m vera.cli / Node, which imports the un-mutated installed package — therefore cannot kill mutants. The oracle for each module is its in-process unit tests:
| Module | In-process oracle |
|---|---|
verifier.py, smt.py |
test_verifier_*.py, test_obligations.py |
checker/ |
test_checker_*.py |
obligations/ |
test_obligations.py, test_lsp.py |
codegen/, wasm/ |
test_codegen*.py, test_wasm*.py |
Consequence for the baseline: code exercised only via subprocess (much of cli.py) will score low because mutations are invisible there, not because its tests are weak — mark those # pragma: no mutate with that reason, don't chase them as gaps.
The committed config scopes the sweep to the soundness core via only_mutate (verifier / smt / checker / obligations), while source_paths = ["vera/"] keeps the whole compiler in range. To sweep a different module, point only_mutate at it (e.g. only_mutate = ["vera/codegen/*"]), then:
caffeinate -dims mutmut run # macOS: keep awake; copies to ./mutants/, runs, stores verdicts
mutmut results # list survivors + not-checked
mutmut show <mutant-name> # see the exact diff for one mutantmutmut run is safe to interrupt — verified against a hard SIGKILL mid-run: completed verdicts persist (plain JSON, no DB-corruption window) and re-running resumes, re-doing only the unfinished mutants (39s vs ~100s from scratch in the spike). A power-off costs minutes, never the whole run. Only deleting mutants/ forces a full restart (of compute, never of correctness).
🎉 killed (a test caught it — good) · 🙁 survived (gap — triage) · ⏰ timeout (see Z3 note) · 🔇 no tests / not checked (no covering test — often a coverage gap or subprocess-only code) · 🤔 suspicious.
mutmut show <name>— read the mutation.- Classify:
- Weak test → strengthen it (a discriminating assertion or a new killing test). Same discipline as #680/#734: pick inputs where the wrong behaviour flips the assertion.
- Equivalent mutant (semantically identical to the original — e.g.
a < bvsa <= bwhere the boundary is unreachable) →# pragma: no mutateon the line, with a one-line rationale. - Genuine coverage gap → add a test.
- Re-confirm (Z3-flakiness guardrail): re-run the specific mutant ≥2× before trusting a survivor. A mutant that makes a verification barely unsolvable can hit the Z3 timeout →
unknown→ Tier-3 and survive nondeterministically. If a survivor flips between runs, it's timeout-flaky, not a weak test — raise the--timeout/ Z3 timeout rather than "fixing" a test.
Run the sweep locally (CI's 6 h job cap can't hold a multi-day run); the committed config scopes the first pass to the soundness core:
caffeinate -dims mutmut run # hours-to-days; resumable, leave it overnightTurn the verdicts into the durable record with the reporting script:
python scripts/mutation_report.py --label coreIt writes mutation-summary.csv (committed — per-module total / killed / survived / timeout / caught%, a diff-able score history across sweeps), mutation.json (the README shields.io badge), mutation-survivors.csv (the survivor + timeout inventory, gitignored), and mutation-<label>.png (the per-module chart, gitignored — needs matplotlib, which ships in the [mutation] extra; the script skips the PNG with a note if it is absent). The script fails loud rather than emit a number it can't stand behind: an empty corpus, a result line it can't parse (mutmut format drift), a mutmut results status it doesn't model (not checked / suspicious / caught by type check — mutmut results lists every non-killed mutant, and these must not be folded into the derived killed count), a module missing from the mutants/ tree, or a per-module total below its survived+timeout count is a hard error, not a skewed score. Post the headline score + per-module table as a comment on #387, and drag-drop the inventory CSV and the chart into that comment (gh can't upload binaries; GitHub CDN-hosts them). The soundness core (verifier / smt / checker / obligations, all in-process tested) is triaged first; remaining modules become tracked per-module follow-ups under the issue.
The 2026-06 baseline: 10,620 core mutants, 80.8% caught (6,816 killed + 1,766 timeout), 2,038 survivors — verifier.py dominates the survivors (1,132); checker/control.py is the weakest-covered substantive module (60.6%).
Mutation testing runs locally for now — the measure-all baseline is a multi-day job that CI's 6 h per-job cap cannot hold. Two CI pieces are deliberately deferred to a dedicated follow-up PR (workflow files warrant their own focused security review):
- A non-gating on-demand sweep (
workflow_dispatch) for running a bounded per-module sweep in CI when convenient. - The diff-scoped PR gate — mutate only the changed lines of a diff, run in parallel with the existing matrix, block on a survivor. Cheap because it only touches what a PR changed. It will need a matching entry in the branch-protection required-checks list (which is decoupled from the workflow YAML and synced by hand).
Both land once the baseline is stable and the soundness core is clean.