git:20260703.bdabb9b to git:20260713.90c0e23

18 added, 26 removed. Audit A to A.

---

name: new-spec

- description: Author a new .fsl spec and take it through the repo's non-vacuity gate before calling it done — fslc check, then verify, then --engine induction, then a hollowness check via fslc mutate kill-rate / --vacuity. Use when creating or substantially changing a spec under specs/ or examples/.

+ description: Author a new or substantially changed .fsl spec and take it through native check, bounded verification, induction where relevant, mutation, and vacuity evidence before completion.

---

- # new-spec — author a spec that actually says something

+ # Author a meaningful FSL spec

- A spec that verifies is worthless if it verifies *vacuously*. This skill is the gate a

- new or changed `.fsl` should pass. Read `skills/fsl/reference.md` before writing syntax —

- FSL is not in training data, so write from the reference, not memory.

+ Read `skills/fsl/reference.md` before writing syntax. Use the working-tree native prefix:

+ ```text

+ cargo run --manifest-path rust/Cargo.toml -p fslc-rust --bin fslc --

+ ```

## Gate

- 1. **Parse + types (fast loop).** `.venv/bin/python -m fslc check <spec>`. Fix errors

- here first; this is the tight iteration signal.

- 2. **Bounded model check.** `… verify <spec> --depth 8` (raise depth as needed). Read the

- JSON: `verified` with a witness, or a shortest counterexample to reason about.

- 3. **Unbounded proof where it applies.** `… verify <spec> --engine induction` for an

- infinite-depth guarantee (supply a `decreases` ranking / `invariant` if induction needs

- it; `sum(x: T of …)` is allowed in a `decreases` measure).

- 4. **Non-vacuity — the step people skip.** A green spec can be hollow (a dead ghost, a

- tautological invariant). `--vacuity` catches some cases but misses dead-ghost

- tautologies, so gate on **mutation kill-rate**: `… mutate <spec>`. A very low kill-rate

- (roughly <10%) means the spec barely constrains anything — strengthen the invariants

- until mutants die.

+ 1. `check <spec>` for syntax and semantic diagnostics.

+ 2. `verify <spec> --depth 8` or a justified bound for bounded evidence.

+ 3. `verify <spec> --engine induction` when the intended claim is unbounded.

+ 4. `mutate <spec>` to measure whether properties constrain behavior.

+ 5. `verify <spec> --vacuity error` where applicable.

+ 6. Run the focused corpus/command test required by the spec's dialect or example family.

- ## Rules

+ Do not hollow out a spec to dodge a counterexample. Confirm source requirements and exceptions before

+ inventing behavior. Keep confirmed assumptions with the spec using established metadata. If FSL is the

+ wrong tool for the behavior, say so rather than forcing a vacuous model.

- - **Never hollow out a spec to dodge a counterexample.** Weakening an invariant to go

- green defeats the purpose. If a counterexample is real, fix the modeled behavior, not

- the property.

- - If a spec lives under `specs/` or `examples/`, changing it will move the corpus snapshot

- (`tests/test_corpus_snapshot.py`). Review the diff; regenerate only if the behavior

- change is intended (`FSLC_SNAPSHOT_UPDATE=1 .venv/bin/python -m pytest tests/test_corpus_snapshot.py -q`).

- - If FSL is the wrong tool for what you're modeling, say so and recommend ordinary tests

- instead of forcing a spec (see the self-check in `skills/fsl/SKILL.md`).

+ Changing a corpus file may affect contract or compatibility artifacts. Use their owning generator only

+ after confirming the semantic change is intentional; never hand-edit a snapshot.