ESS plugin: teach a catalogue of specification-hardening techniques beyond mutation

[b10x-bot]

Proposal

Teach the ESS plugin a catalogue of specification-hardening techniques. Each one runs after a suite is green and asks a question the suite cannot. Today ess:testing-conformance covers one of them: mutation, as "break the behaviour and watch a named scenario go red" (SKILL.md:22-41). An agent asked "how do I harden this spec?" has nothing else to reach for, and has to invent the rest each time.

Evidence from one adopter: a spec with 3 domains, 7 entities and 31 commands, and a JavaScript implementation. The generated suite had 121 scenarios, all passing. Each technique below was applied in turn, and each one was shown to fail against a planted defect before it counted.

technique	question it answers	what it found for that adopter
1. Mutation audit	Would the suite notice if a declared rule broke?	8 of 35 single-rule breaks passed every scenario; 6 were declared behaviour. Root causes in beyond10x/ess#111
2. Random command sequences checked against a reference model interpreted from ess specify compile IR	Does the implementation agree with the spec along paths nobody wrote?	4 of 4 engine defects that the 127-scenario suite passed: a view capped at 5 rows, a refusal that still writes, an identity reused, a state not re-enterable. Also 3 invariants that held only through undeclared defaults (beyond10x/ess#112)
3. Replay of the real caller (the application's own command stream, checked against the same model)	Does the code that uses the implementation send only what the spec accepts?	0 disagreements over 25,980 commands; 25 refusal outcomes the caller never triggers
4. Determinism (same seed twice → same command stream; source scan for clock and randomness)	Is the implementation deterministic where the spec assumes it?	Passed; a planted Math.random() diverged at command 235
5. Metamorphic relations between paired runs (e.g. "a pause changes nothing but the pause commands")	Do promises that span two runs hold?	1 real defect: an action allowed while paused that the design forbids
6. Exhaustive guard analysis over each when: guard's complete boundary domain, with an optional z3 cross-check	Are guards dead, overlapping, gap-leaving, or weak enough to admit an invariant break?	11 guards, 374 combinations, 0 findings
7. Spec diff in the gate (ess verify diff against the last release tag)	Is a change breaking, and was that acknowledged?	20 changes since the tag, all additive. ess names changes but does not classify them as breaking, so the adopter wrote the classification
8. Design review by an agent: design document vs mapping vs spec, every finding citing both sides	What does the design say that the spec omits or contradicts?	26 findings, the most of any technique, e.g. "one entry per player" and "the count always goes up" were not declared at all

Formal model checking (TLA+ or Alloy export) was considered and not applied. On a spec this size, random sequences reached every declared outcome, 59 of 59.

What the plugin could carry

1. A skill (ess:hardening, or a section of ess:testing-conformance) that:
   • lists the eight techniques with what each catches;
   • gives an order: cheapest first, and the design review early because it found the most;
   • carries the rule that makes each one count: a check nobody has seen fail is not evidence, so plant a defect first;
   • carries what each technique needs from the IR: lifecycles, guards, sets, payloads, views, invariants, actors.
2. The model interpreter as a reusable reference. Techniques 2, 3 and 6 all rest on it: about 150 lines over the IR. Proposal: mutation audit and a model-based sequence runner generated from the IR ess#114 has a draft explore.ts for the TypeScript target. Until that ships, the skill could point at it as the pattern.
3. The ess:conformance agent offers the catalogue when it finishes a coverage task on a green suite, not only mutation.
4. A design-review brief for an agent (technique 8): the four classifications (missing / contradicts / stale mapping / spec-only, plus unclear), the rule that every finding cites both the design line and the spec file:line, and "quote a vague statement and mark it unclear rather than inventing a meaning".
5. Spec-diff classification guidance until ess classifies changes itself. Treat as additive: added items, variants, transitions, grants, accepts and publishes, and wording. Treat everything else, and anything marked narrowed, as breaking. Acknowledgement is a committed file keyed to the release tag.

Related

• Synthesized suite misses declared behaviour: transition state never asserted, updates repeat setup values, one source per transition, no guard boundaries ess#111: generator gaps found by technique 1
• validate is green where synthesize refuses an authored scenario's actor, and where an invariant reads a field no create sets ess#112: validate gaps found by technique 2
• Proposal: mutation audit and a model-based sequence runner generated from the IR ess#114: mutation and sequence runner as ess features, with the draft
• ESS skills: init ignores an existing specification, the refusal recorder is Go only, init plans without --host #32: ESS skill fixes