specodelic

specodelic (spk) is a specification format and toolchain for AI agents: specs are plain markdown with YAML frontmatter (the Intent layer) and three fixed tables — Constraints, Model, Properties — under a closed schema. The linter never reads prose, so prose is free; everything the toolchain reasons about lives in the structured rows.

The repo dogfoods itself: every corpus file in openspec/specs/ is a spec written in the format it describes.

Hit jargon? The glossary defines every term a cold read needs, from EARS to the guarantee ladder.

Is this for you? The format presumes a spec-first workflow — the spec is the design artifact and the implementation is agent-authored, regenerable, machine-checked code. If humans hand-maintain the code and nothing consumes the structured rows, the layers are pure tax, not leverage. The full when-not-to-use statement (assumption, honest one-line test, and the cases where an ordinary design doc wins) is in USAGE.md.

New to the format? Read the worked example — one reservation/order spec built layer by layer, with every lint finding and counterexample the author hit on the way.

Before trusting a green checkmark, read verification boundaries — the guarantee ladder from lint-clean to matches-oracle, and what each rung does not assure.

Thinking about a design rather than code? Specs as the design substrate is the canvas for that — and which command when? routes any task to the right verb. Questions a cold read asks are answered in the FAQ.

The four layers

The pipeline

spk walks a spec file through stages, each with its own command:

1. spk lint — the gate: every rule, every file.
2. spk compile — Constraints → TOML, Properties → proptest scaffolding, Model → TLA+ module (all three artifacts, byte-stable).
3. spk model-check — the compiled model interpreted as a pc-automaton by the embedded stateright backend.
4. spk verify — executes the emitted proptest scaffolding.

Plus tooling around the corpus: spk graph (reference graph with fan-in/out and dangling detection), spk rename / spk merge / spk refactor / spk orchestrate, spk doctor (workspace diagnosis), spk explain (the embedded format guide for agents), spk new (scaffold), spk init and spk feedback.

Domain packs extend the format without a format revision: a kind: profile manifest declares typed sections, fiber kinds, and reference fields for a domain (no config file — lint discovers packs by corpus scan). Six packs ship in-repo — the five standard packs (data.lineage, numeric.predicates, empirical.registry, quant.finance, svc.contracts — still draft) plus the bioimage D6 pilot (bioimage.data, the first cross-pack ## Requires); see the packs spec and the using packs guide.

For agents

No repo access needed: spk explain serves the distilled format guide from inside the binary — ten topics (format, ears, kinds, references, lifecycle, lint-rules, dual-format, packs, graph-views, conform), and every lint finding carries its own rule_id and one-line semantics. See llms.txt at the site root for a machine summary.

Ecosystem

specodelic is part of the charly-vibes tool ecosystem — the ecosystem map shows how spk relates to the sibling tools (wai, beads, openspec, genesis-vibes, and the checkers). For the two relationships that touch this repo daily — the OpenSpec dual-format protocol and the ah/espectacular correspondence companion — see tool relationships.

Install

cargo install specodelic

Then spk --version --json (reports the embedded format_revision), spk new my.first_spec, and spk lint my.first_spec.md.

Documentation provenance

Rendered docs are generated artifacts; the repository sources are authoritative — edit the repo sources, not the rendered output.

Release Status

Generated artifact (from Cargo.toml + git ref). Do not hand-edit — the repo source files remain authoritative.

• Version: v0.11.0
• Built from: main @ d4d9c47

Installation & Quick Start

Install

# macOS (Homebrew)
brew tap charly-vibes/charly
brew install specodelic

# Linux / macOS (binary download — all five release targets, see checksums.txt)
# Grab the archive matching your platform from:
# https://github.com/charly-vibes/specodelic/releases/latest
#   specodelic_{VERSION}_linux_{amd64|arm64}.tar.gz · specodelic_{VERSION}_darwin_{amd64|arm64}.tar.gz
tar xz specodelic_*_linux_amd64.tar.gz && sudo mv specodelic spk /usr/local/bin/

# Windows (Scoop)
scoop bucket add charly https://github.com/charly-vibes/scoop-charly.git
scoop install specodelic

# Any platform (Cargo)
cargo install specodelic

(Rust stable toolchain; published on crates.io.) Installs two binaries: specodelic and its alias spk.

Quick start

All output below was captured verbatim from specodelic 0.11.0. On a TTY the tool prints human-readable text (shown here); when stdout is piped it emits a JSON envelope instead.

# Scaffold a spec — the template teaches its own tables
spk new order.cancel --file order.cancel.md

created order.cancel.md
→ Run: specodelic lint order.cancel.md

(--file picks the target path; without it the scaffold lands in the openspec tree at openspec/specs/<cap>/spec.md, which must already exist.)

# Lint it — findings carry their own rule id + semantics
spk lint order.cancel.md

lint: 1 file(s) linted, 0 finding(s), 0 advisory warning(s)
→ Run: specodelic graph

What a finding looks like. A typical first edit — replacing the file-qualified wiki-link in the traces_to column with bare text — is a real mistake, and lint reports it:

spk lint order.cancel.md

lint: 1 file(s) linted, 1 finding(s), 0 advisory warning(s)
  order.cancel [linter.single_root_reachable] 4 row(s) unreachable from any intent row — an orphaned island (traces_to/derives_from/guard/from-to/emits): order.cancel.c1, order.cancel.initial, order.cancel.p1, order.cancel.t1
→ Run: fix the reported invariants — each rule's semantics: spk explain lint-rules

That is linter.single_root_reachable hard-failing: every row must reach its file’s own intent row through own-file typed links, and bare text is not a wiki-link — so c1 loses its reachability path and drags the state, transition, and property hanging off it down as one orphaned island.

# Derive the reference graph (fan-in/out, dangling links)
spk graph order.cancel.md

graph: 1 file(s), 5 node(s), 5 edge(s), 0 dangling, 0 typing violation(s), 0 supersedes cycle(s), 0 external boundary(ies)
→ Run: specodelic lint

# Compile to artifacts: TOML + proptest scaffolding + TLA+ module
spk compile order.cancel.md --out-dir specodelic/

compile: 1 compiled, 0 failed
  order.cancel.md [order.cancel] → specodelic/order.cancel.toml, specodelic/order.cancel_props.rs, specodelic/order.cancel.tla
→ Run: specodelic verify (consumes the *_props.rs artifacts)

# Model-check the compiled module (embedded stateright backend)
spk model-check order.cancel.md

model-check: 1 checked, 0 failed
  order.cancel.md [order.cancel]: exploration_only (1 states explored) → specodelic/order.cancel.check.json
    claims: 0 evaluated, 1 unchecked, 0 blocking
      unchecked: c1
→ Run: specodelic verify (consumes the *.check.json reports)

In an existing workspace

spk doctor        # diagnose the workspace (self-hosting vs consumer mode)
spk init          # write the SPECODELIC managed block into AGENTS.md
spk explain       # the embedded format guide — ten topics, no repo access needed
spk feedback      # send feedback about the tool

Self-hosting

This repo’s own corpus (openspec/specs/ — the single tree, specodelic-jf1) is linted by the tool itself:

just lint-specs   # spk lint openspec/specs
just ci           # fmt-check + clippy + tests + release build + openspec gates

Command Reference

Exit codes (uniform across verbs): 0 = a clean run; 1 = the stage produced findings or a tool-level failure; 2 = invocation error — nothing was processed (path not found, no spec files matched, unreadable input). clap argument-parse failures also exit 2. The JSON envelope’s envelope_kind is "error" and ok is false whenever the run is not a clean run — findings and failures never ride a success-shaped envelope (openspec/specs/errors/spec.md envelope_error_kind + exit_code_mapping).

All commands emit through the genesis envelope: JSON for pipes, human-readable for TTYs (--human / --format json to override). Failures carry a remediation hint. Hit jargon? The glossary defines every term a cold read needs.

spk lint <files|dirs>

Use when: you want the gate — before committing, in CI, or wired as the pre-commit hook (spk hooks install). It is the first stage every other verb assumes (spk explain lifecycle).

The gate. Runs every rule in the catalog over spec files (recursively; files without frontmatter are skipped with a warning). Each finding carries rule_id (linter.<name>) and rule_semantics.

• Spec: linter rules (one file per rule family)

When nothing was found and the repo carries an openspec/ tree (consumer repos keep their corpus under openspec/changes/*/specs/), the failure hint names it — spk lint openspec (gh#2.2).

Ingestion is hostile-input hardened (specodelic-suz): only regular files under a 2 MiB cap are ever read — a FIFO, device file, or oversized file named *.md is labeled, named, and skipped (never blocking or unbounded-memory); when nothing else was linted, the labeled notes ride the failure envelope. A parse error (malformed frontmatter) fails the stage (exit 1) even when the rest of the batch linted clean — a corrupted spec is never a silent pass (specodelic-in9: the pre-commit gate must not let it commit); the error names the offending file and the file was NOT linted.

Domain packs

A workspace extends the format with domain packs: kind: profile spec files whose six manifest tables (Sections, Kinds, References, Checkers, Floors, Requires) declare typed sections, fiber kinds, reference fields, checkers, and floors. Lint discovers packs by corpus scan (no config file), activates them when a file’s vocabulary matches, and reports:

• linter.pack_shape findings — a malformed pack manifest is a labeled failure
• pack-activation notes (warnings channel, exit 0) and orphan_vocabulary labeled failures — pack vocabulary used with no pack discovered or declared is never silent: a uses edge naming an absent pack, or a pack-qualified token in a kind/field position whose namespace has no discovered pack, names the candidate pack and both remediations
• lifecycle/revision-skew advisories (draft packs activate advisory-first; a pack pinned to an older base format_revision is named)

The five in-repo standard packs live in packs/ (data.lineage, numeric.predicates, empirical.registry, quant.finance, svc.contracts — the last still draft); a consuming file opts in by using the pack’s vocabulary, or explicitly via a uses reference to the pack’s frontmatter id.

• Spec: packs · Guide: using packs

A *.checklist.md file in the linted tree declares an external checklist (openspec/specs/linter-external_completeness/spec.md — mp1 row 10’s manifest format): a flat ## Items list plus a ## Mapping table (item/status/mapped_ids/rationale). The five linter.external_completeness rules then check every item is explicitly covered (mapped ids resolve to real constraint/property rows) or waived (with a stated rationale). This pass is optional and never gates a lifecycle stage — no checklist declared, nothing checked; spk compile’s precondition gate deliberately does not run it.

spk graph <files|dirs>

Use when: you need to see who references what — dangling references, fan-in/fan-out, typing violations, supersedes cycles — before making rename, merge, or refactor decisions (the advisors build on it).

Derives the reference graph from every typed reference field: nodes, edges (including a Transition’s from/to state edges), fan-in/fan-out per row, dangling references, typing violations (the Reference Typing table — forbidden edges are reported, never recorded), and supersedes cycles. The rename/merge/refactor advisors build on it.

Text projections (--format edges|dot|mermaid): edges writes the raw six-column TSV edge list (source_id, source_kind, field, target_id, target_kind, annotation — every recorded edge one row, every typing violation one annotation row); dot and mermaid write byte-stable Graphviz/Mermaid text projections (visual grammar: solid = state machine, dashed = guards, bold = emits, dotted = traceability, red dashed = dangling/violations). Rendering stays external — pipe into dot -Tsvg or paste into a mermaid renderer; there is no --render. The projections are the one documented exception to the envelope: raw text straight to stdout, so awk/jq pipelines consume it without an envelope parser. --view wiring (requires --format, composes with all three) selects the wiring view: constraints.satisfies edges project to file level (consumer file → the producer’s published contract), self-loops are dropped, and the remaining cross-file instances aggregate per distinct pair; a corpus with no remaining edges emits a labeled no_wiring element, never a silently clean diagram. Derived diagrams of this repo’s own corpus (wiring, states, trace, schema) live in graph views; spk explain graph-views carries the same taxonomy and one-pipe recipes for your own corpora. The DOT projection renders externally — including through gently, the family’s native Graph::Easy port (spk graph <corpus> --format dot | gently --as ascii); rendering stays a pipe, never a built-in flag.

• Spec: graph

Same discovery hint as lint: with an openspec/ tree present, the zero-files failure suggests spk graph openspec.

Exit codes (both modes): 0 clean, 1 findings (typing violations — the annotation rows still ride along in projections), 2 invocation error (no spec files on an existing path is clean-empty, but a nonexistent or unreadable path is an error — a typo’d path is not a clean empty corpus).

spk new <id>

Use when: you are starting a fresh spec and want the four-layer skeleton plus the per-layer guidance comments instead of a blank file.

Scaffolds a spec file from the template — per-layer HTML-comment guidance (valid kinds, what a guard may cite, law-case requirements), rendered from the same constants the linter enforces.

spk migrate <file> [--dry-run]

Use when: you have an existing openspec delta to wrap (plain form) or — with --rekey — a 0.6.0-era dual-format file still carrying id: spec that must be re-keyed to its real parent-dir-derived id for the 0.6.0 → 0.7.0 corpus migration (spk lint <tree> finds them).

Wraps an existing openspec delta file in place into the Revision 19 pair: the plain delta stays byte-untouched and the generated sibling layer.md sidecar carries the specodelic layer — frontmatter (the parent-directory-derived id with a .layer suffix plus an EARS scaffold statement) and wired scaffold layers (scaffold_* placeholder rows — constraint, one-state model, deriving property). Existing sidecar pieces pass through verbatim; only missing pieces are inserted. A file that already carries frontmatter is refused, never rewritten — re-running is safe. The scaffold lints clean as written; keep it green while you replace the placeholders. Files not named spec.md get a naming-law warning (openspec requires the delta filename spec.md). --dry-run prints the resulting content without writing. --rekey instead rewrites an id: spec dual-format file (0.6.0-era) to its Revision 18 real id — derived from the parent directory — re-keying every [[spec.*]] ref; a file already carrying its real id is an idempotent no-op, and a plain delta or undeducible id is refused without rewriting. This is the sanctioned 0.6.0 → 0.7.0 corpus migration path: spk lint <tree> finds the files, spk migrate <file> --rekey per file.

spk compile <files> --out-dir <dir>

Use when: a spec is lint-clean and you want its executable artifacts — the Constraints TOML, proptest scaffolding, and TLA+ module that model-check and verify consume.

Compiles a lint-clean spec into three artifacts: <stem>.toml (Constraints), <stem>_props.rs (proptest scaffolding), <stem>.tla (TLA+ module). Total or labeled failure — never a silent partial result.

Property and invariant fragments opt in per cell with a **lang:** marker whose tag is drawn from the closed set {rust, py, ts}; a tag outside the set (e.g. **go:**) is a labeled extraction failure naming the tag and the closed set, never silence. **rust:** is the only executable tag — a **py:** or **ts:** fragment gates compile with a labeled failure naming its emitter follow-up (add-py-fragment-emission / add-ts-fragment-emission), never a silent fall-through to Rust emission.

The tag shape is lowercase-initial ([a-z][a-z0-9_-]* before :**): ordinary bold prose (**Note:**) stays prose, but a lowercase bold label in fragment position (**note:**) is tag-shaped and therefore a labeled extraction failure naming the tag and the closed set — keep prose labels capitalized, or move them out of fragment position.

Two binding layers, never cross-wired:

1. Artifact scaffolds (specodelic). compile emits the fragment verbatim into the artifact and records it in metadata comments and the .check.json/manifest staleness keys. Those comments are staleness records, not contracts (CORR-001’s correction).
2. Contract bindings (espectacular). ah binds existing tests to deployed scenarios via contract-TOML entries ([[tests.cargo]], [[tests.pytest]], [[tests.shell]] flags). Binding is not compilation — the layers have different wall-clock, caching, and toolchain stories (design D3 of the language-neutral binding change).

The claim path between them is kernel.binding: an invariant-kind Constraint may carry a kernel.binding column, and compile extracts the cell as an opaque string into the Constraints TOML artifact — verbatim, never parsed, validated, or interpreted (design D4 of add-min-expr-kernel: no registry; the name is namespaced against pack binding columns). An external checker claims a constraint through contract-TOML flags — binding its own tests to the deployed scenarios — while specodelic never learns the checker’s language: the bridge carries the claim, it never absorbs the checker.

The boundary between the tools is tracing vs semantics: espectacular’s property-untraced finding is bookkeeping and may grow similar tracing findings, but ah must never grow semantic findings — a hypothetical property-uncompiled would enforce compile.md’s semantics from ah, crossing the sibling-tool boundary (read-only over openspec/, never enforcing against the specs/ corpus).

• Spec: compile

spk model-check <files>

Use when: you want bounded evidence that the compiled model’s required claims hold (spk explain lifecycle: model_check requires a complete Model section). Read the outcome honestly — claim_aggregate_governs (openspec/specs/model_check/spec.md) fixes the priority:

• no_counterexample — clean: a nonempty required set all verified over a completed bounded exploration (the native backend earns it when the corpus carries executable claims; it is not TLC-only).
• counterexample_found — a required claim was refuted; exit 1, the finding names the claim id.
• timed_out — the depth/state/time bound expired before the exploration completed; exit 0, but not clean.
• exploration_only — the exploration completed but required claims were unknown, unsupported, or missing — including a prose-only corpus whose required set is empty; exit 0, but not clean.

Only no_counterexample satisfies spk verify’s model gate.

Runs the compiled model through a model-check backend within a stated bound (--max-depth, --max-states, --timeout-secs). Two backends:

• stateright (default) — embedded BFS exploration over the compiled model, executing the claims opted into evaluation: **rust:** predicate fragments compiled into the module run inside the exploration, and **kernel:** claims evaluate over the kernel grammar. Prose guards are never interpreted.
• tlc (opt-in, --backend tlc --tlc-jar <tla2tools.jar>) — the TLA+ TLC reference engine as a JVM subprocess over the compiled module, -depth as the stated bound (--max-states has no TLC equivalent and is a labeled error). The JVM binary comes from PATH or SPK_TLC_JAVA; a missing binary or jar is a missing_checker error, never a verdict.

Claim gates (model_check.md’s required_claims_classified + claim_aggregate_governs): a run partitions each parsed file’s invariant-kind Constraints into a required set — those opted into evaluation (**rust:** fragment, **kernel:**, or citation) — and an explicitly unchecked set of prose-only invariants: prose wording, a constraint’s name, or a deriving Property never implies evaluation, and advisory/effect/extension-point rows are never required. The outcome is governed by the required claims’ statuses with fixed priority: any refuted required claim is counterexample_found naming it; absent refutation, an exhausted time/state/depth budget is timed_out; otherwise any unknown, unsupported, or missing required claim is exploration_only with reasons — and so is an empty required set (a prose-only corpus has nothing required, so a completed run stays exploration_only). Only a nonempty required set all verified over a completed bounded exploration reports no_counterexample — the native backend earns it when the corpus carries executable claims; it is not TLC-only. A refuted kernel claim (counterexample_found — CHANGELOG #116’s failing aggregate outcome) is findings: exit 1 with an error-kind envelope (ok:false), the payload intact.

Evidence: the run report persists as <stem>.check.json (claim_schema_version 1) with the consumed module’s SHA-256, the backend engine + version, canonical claim records (id, evaluator kind, status, reason where not verified), expected_claim_ids / unchecked_claim_ids, and a scope_sha256 digest of the parsed structured content and the consumed compiled artifacts. The digest binds structured content, not filesystem paths: reordering CLI inputs or editing prose alone preserves it, while two inputs differing in invariant content never share one. Verify (and orchestrate’s verify stage) recompute the digest and the required claim set from the current inputs and reject stale, foreign, or malformed reports with a rerun hint naming the model-check command — a stored report is never rewritten to manufacture evidence. A command’s parsed inputs must claim unique intent ids: two files with the same id fail duplicate_corpus_identity with a rename hint before compilation, evaluation, or report writes (Revision 18: dual-format files carry real ids and compose like any corpus — the former id: spec isolated-scope rule retired with id: spec itself). A **kernel:** constraint cell that breaks the closed grammar is a labeled kernel_grammar failure before any run — the same validation compile applies — so a stale compile can never silently demote a malformed kernel claim to unchecked and report clean. The honest non-failure outcomes keep exit 0 — timed_out (the bound expired) and exploration_only (a completed exploration over a corpus with no executable claims) are real terminal outcomes, not failures (model_check.md); spk verify’s model gate is what rejects them as not-clean.

• Spec: model_check

spk verify <files>

Use when: you want the conjunction — executed proptest properties and a current clean model verdict (no_counterexample). Choose verify over re-running model-check when a current .check.json exists and you want the full gate without re-exploring the model — verify never re-compiles and never re-runs the model checker; choose model-check when you need fresh bounded exploration evidence itself. Neither is a substitute for the application’s own test suite (spk explain lifecycle).

Executes the emitted proptest scaffolding and rejects stale clean results via the .check.json hash.

Both gates must hold — verified is the conjunction, never a single green stage:

• Properties gate — the *_props.rs artifact is staleness-checked against the current spec by block-metadata fingerprint (ids, cases, generators, predicates — hand-translated predicate bodies keep the fingerprint, spec edits change it), then really executed: the artifact is staged into a scratch cargo crate and run via cargo test, so an un-translated todo_predicate! fails honestly (properties_failed), never skipped. Failing blocks report proptest’s shrunk minimal input.
• Model gate — the <stem>.check.json run report must be current (its artifact_sha256 matches the on-disk <stem>.tla; a missing module fails closed as stale), its scope_sha256 digest and required claim set must match the current inputs (verify recomputes them — stale, foreign, or malformed reports fail with a rerun hint, never rewritten), and its outcome must be no_counterexample — earned only when every required claim verified over a completed bounded exploration (exploration_only and timed_out are explicitly not clean).

--timeout-secs <N> (default 600; 0 = unbounded) bounds the whole cargo run on a wall-clock clock: a hanging (likely pathological) predicate is killed and reported as a labeled properties_timed_out block — never a silent hang, and never indistinguishable from a test failure (no block verdicts exist after a kill, so the bound is raised and the run repeated, not misread as a failing property).

.data.status is verified exactly under the conjunction, else the first blocking stage (missing_properties_artifact, stale_properties_artifact, properties_failed, properties_timed_out, properties_uncompilable, runner_unavailable, missing_model_run, stale_model_run, model_not_clean). Verify never re-compiles and never re-runs the model checker. A blocked verify is findings, never a success-shaped envelope: exit 1 with ok:false / envelope_kind:"error", the payload (and .data.status) intact.

Scope note: verify’s stored scope digest binds the run’s structured inputs (contributing files, claim records, artifact SHA-256), not result statuses — a hand-forged check.json with invented verified statuses does not yield a clean model gate: verify recomputes the scope and the required claim set from the current inputs, and any digest, record-shape, or artifact mismatch is rejected with a rerun hint (openspec/specs/verify/spec.md evidence_scope_bound; the persisted report is never rewritten).

The properties gate’s scratch crate lives under the system temp dir (specodelic-verify/), with a shared target/ dir so proptest compiles once per machine. A retention policy keeps it bounded: orphaned per-invocation crate dirs (from killed runs) are pruned after 24 hours, and if the shared target/ dir exceeds 4 GiB it is dropped whole — the next verify pays one cold proptest rebuild. Set SPECODELIC_VERIFY_SCRATCH to relocate the scratch base (e.g. off a size-capped tmpfs).

• Spec: verify

spk conform <file> --oracle scenarios.jsonl [--closed-world]

Use when: you have evidence from outside the spec — traces recorded from a legacy system, a curated case set, or a reference implementation — and you want each trace classified against what the spec declares and can actually execute. Every other verb evaluates the spec’s own claims; conform is the one verb that checks the spec against reality. It is strictly read-only (help text states it): it never advances the lifecycle, is never an orchestrate stage, and writes nothing.

Each JSONL trace record (one per line, carrying id, an optional setup state, and a trace of actions with observations) receives exactly one verdict from a closed set — never collapsed to pass/fail:

• permitted — a declared, executable claim covers the trace and it agrees
• forbidden — the trace violates a declared executable claim (in any invocation mode), or — only under --closed-world — nothing declared covers it
• underspecified — no declared Model element or claim covers the trace (open-world default: a spec gap, never a prohibition)
• unknown — a covering claim exists but is prose-only (prose is never silently checked)
• unsupported — the covering claim’s evaluator kind is not executable in this run

The run report carries a conform-local report_schema_version, per-trace records sorted by scenario id (no timestamps — reruns over identical inputs are byte-identical), a scope_sha256 binding the parsed spec and the consumed corpus bytes, and a fixed evidence_scope field in both the JSON envelope and the --human view — “agreement on the supplied corpus; not a proof of behavioral equality”. That scope is data, not a disclaimer: a finite trace corpus agreeing with the spec never proves the spec describes the system.

Exit codes: 0 = no forbidden/unsupported verdict; 1 = any such verdict; 2 = invocation error or gate refusal (stale artifacts, lint-dirty file, malformed corpus) with zero verdict records emitted. unknown and underspecified surface as counts but never fail the run — they are spec-gap findings, not refutations.

• Book: conform — external oracle evidence (spec page lands with the corpus archive; see book: verification boundaries)

spk parse <file>

Use when: a downstream tool or script needs one file’s structured IR as JSON — syntax-only, it succeeds even where lint would fail (chain spk lint yourself).

Emits the parsed Spec IR for one file as a JSON envelope (specodelic-9rv): data carries the full structured layer — intent, constraints rows, states, transitions, properties rows (cells as keyed maps, not generated text), and structured links. Parse is syntax-only: it succeeds on files that fail spk lint and embeds no lint status — chain spk lint yourself (the envelope’s hint names it). Exactly one file per invocation (no globbing — consumers loop); unparseable or missing input is a labeled error envelope with a remediation hint and a non-zero exit.

spk doctor

Use when: onboarding a repo or after a format-revision bump — it classifies the workspace and warns (never fails) on corpus revision lag.

Classifies the workspace (self_hosting vs consumer), checks the local corpus’s Revision N against the binary’s embedded format_revision — warns, never fails, on lag. A corpus discovery check names where the specs live (specs/, an openspec/ tree with a file count, or the discovery rule).

spk explain [topic]

Use when: you are offline or want the canonical wording — the embedded format guide, no repository access required. Nine topics: format, ears, kinds, references, lifecycle, lint-rules, dual-format, packs, graph-views.

spk init, spk feedback

Use when: provisioning an agent-facing repo (init writes the SPECODELIC managed block) or filing an upstream issue (feedback).

spk init writes/refreshes the SPECODELIC managed block in the repo’s AGENTS.md (rule catalog + format revision). spk feedback opens a prefilled feedback channel for the tool.

spk hooks install, spk hooks uninstall

Use when: you want the dual-format lint gate (spk lint openspec) to run on every commit — marker-guarded and additive in the lefthook chain, never a commit trap.

spk hooks install wires the dual-format gate (spk lint openspec) into the repo’s pre-commit chain as a marker-guarded managed block in lefthook.yml — purely additive (beads’ core.hooksPath → lefthook chain keeps flowing), idempotent, indentation inferred from the stage’s own children. Install runs the gate once and reports the outcome (data.outcome, data.gate_dry_run); a failing gate is a warning with the failure summary and an escape hint (spk hooks uninstall), never a commit trap. Requires a lefthook config (never created from scratch) and an openspec/ tree; husky and prek repos get a labeled refusal with a manual-wiring hint. spk hooks uninstall strips only the managed block.

spk archive-companion <CHANGE_ID>

Use when: archiving an openspec change whose deltas carry the dual-format layer in sibling layer.md sidecars — the stock openspec archive regenerates deployed specs and strips the layer (spk explain dual-format has the wrap recipe).

spk archive-companion archives an openspec change while preserving its dual-format layer (specodelic-fzo, GH#7; reworked for Revision 19, add-delta-layer-sidecar): the companion invokes openspec archive with default spec application — plain deltas are openspec’s native merge — then re-attaches the layer to each regenerated deployed spec from the change’s archived layer.md sidecar. Fail-closed: a delta without a restorable sidecar is refused BEFORE the destructive archive, with the spk migrate wrap path as the hint, and the assembled deployed spec is shape-asserted (no delta headers, frontmatter + the three tables) before anything lands — the tool never deploys a stripped spec. Re-running on an already-archived change skips the openspec invocation and re-attaches to identical deployed bytes; a change with no spec deltas succeeds with an empty restored list; --dry-run resolves the plan without invoking openspec or writing anything. just archive-change delegates to this command.

spk rename <old_id> <new_id> [files|dirs]

Use when: an id changes and every referencing [[link]] (plus checklist mapped_ids and the filename itself) must follow — computed and verified in memory before any byte is written, so a failed rename leaves the repo byte-identical.

The atomic rename (openspec/specs/rename/spec.md): updates the defining row (an Intent frontmatter id or a table row’s qualified id) and every referencing [[link]] — including child refs like [[old_id.child]] — as one transaction. Declared checklists reach into the same law: every *.checklist.md’s mapped_ids cells are rewritten too (bare and [[…]] spellings alike), and the verify gate re-runs the external-completeness resolution over the post-rename corpus, so a missed cell is a labeled rejection, not a silent dangle. A file whose Intent id is renamed also gets its filename renamed per the - ⇔ . naming law. Everything is computed and verified in memory (re-parse + zero dangling) before any byte is written, so a failed rename leaves the repo byte-identical: collisions, unknown ids, and verify-gate rejections are labeled failures with remediation hints.

• Spec: rename

Merge check

Use when: two branch tips both touched spec ids and you want what a textually clean merge cannot see — id collisions, dangling renames, intersecting blast radii — checked before joining the trees.

spk merge --branch <incoming-tree> [--base <ancestor-tree>] [current-tree] checks what a textually clean 3-way merge cannot see (merge), over the two branch tips’ spec trees:

• id collisions — an id minted on both branches (absent from the ancestor, or divergently edited on both) is flagged as a collision.
• dangling renames — a rename on one branch plus a fresh reference to the old name on the other is flagged for replay (spk rename does the rewriting after the trees are joined).
• blast radii — each branch’s touched ids get a fan-in/fan-out closure computed from that branch’s own graph artifact; intersecting radii require human review (needs_review) even when the file diffs don’t overlap.
• relint gate — the union tree must re-lint clean with zero dangling references before the merge reports merged.

Exit 0 = merged, 1 = findings (verdict needs_review or failed), 2 = invalid invocation (missing --branch, empty incoming tree).

• Spec: merge

spk orchestrate <files|dirs> [--out-dir <dir>] [--backend tlc --tlc-jar <jar>]

Use when: you want the whole pipeline — parse → lint → compile → model_check → verify — in the fixed stage order with each gate enforced, halting at the first failing stage, in one invocation.

Drives the full pipeline — parse → lint → compile → model_check → verify — in the order orchestrate fixes, gating each stage transition exactly as specodelic specifies and halting at the first stage that fails:

• Lint stage — the six Checker Ownership checkers run in dependency order: frontmatter first, then referential_integrity → graph_shape → model_shape (branch A), ears_syntax (branch B), schema_shape (branch C). A failed checker’s dependents are skipped (never invoked, never reported as failed) while independent branches still run and report. linter.external_completeness runs when a checklist is declared and never gates.
• Compile stage — advances past the coverage checker’s verdict only (compile_gate_matches_coverage), never a looser or stricter check.
• Model_check stage — passes only when every file’s outcome is no_counterexample; exploration_only and timed_out are honestly not clean, so a corpus whose required claims never all verify halts here — a prose-only corpus (empty required set) always reports exploration_only, while corpora with executable claims can pass on the native backend (use --backend tlc --tlc-jar for the TLC reference engine over TLA+ modules).
• Verify stage — the conjunction of both gates (see spk verify).

.data.stages lists every stage with a status (passed / failed / skipped) and the failed stage’s exact findings; every skip carries its reason. Rename is never part of a run. Re-running against an unchanged repo is byte-identical.

• Spec: orchestrate

Refactor advisor

Use when: you are planning a tidy-first split — advisory findings (high unrelated fan-in, changeset subset ownership) that never gate a run.

spk refactor [paths] [--high-fan-in N] [--changeset id1,id2] is the tidy-first split advisor (refactor): it flags nodes whose incoming cross-file dependents share no namespace segment below the root (nearest common ancestor = root — decision of record 2026-09-30), and — with --changeset — nodes whose owned rows the changeset touches only as a strict subset without depending on the rest. Every count comes from spk graph’s derived edges, never an independent markdown walk. The high-fan-in threshold is per-invocation configuration (threshold_is_per_repo_setting; default 3). Findings are advisory: exit 0 whether or not anything is flagged.

• Spec: refactor

Which command when? — routing a task to the pipeline

The full reference is commands.md; this page answers the earlier question — I have X, what do I run? — including which verbs gate on which, and which findings are advisory.

The spine first

The pipeline verbs form a gated chain — each stage refuses to run on a file the earlier stages have not blessed:

parse → lint → compile → model-check → verify
              (gates on lint)  (consumes      (gates on
                               artifacts)     model-check)

spk compile only runs on a file that passed lint and coverage (openspec/specs/compile/spec.md, precondition_satisfied); spk verify never re-compiles — it consumes the artifacts a prior compile wrote to the same out-dir, so a stale compile is a rerun, never an acceptance; spk orchestrate applies the same stage discipline across a whole corpus run. spk conform stands outside this chain: it consumes and classifies, but never gates a lifecycle transition.

Routing table

Two honest maturity notes

• spk model-check is bounded, and honest about it: exhaustive runs report exploration_only, never a fabricated clean; a backend that cannot execute Rust fragments reports exploration_only, never a fabricated pass (model_check).
• spk refactor advises — it never edits. Its findings are exit-0 regardless (refactor).

More boundaries: verification boundaries — what a green check actually buys you.

Glossary

The jargon this book (and the openspec/specs/ corpus) uses, defined for a cold read. Definitions are one to three sentences; where a deeper explanation exists, the entry links to it instead of restating.

The format and its files

• spec / specodelic file — one markdown file: YAML frontmatter plus fixed tables under a closed schema. Every corpus file in openspec/specs/ is a spec written in the format it describes — see the core format.
• frontmatter — the YAML block at the top of a spec file carrying the file-level identity: id, kind, and statement. Checked shape-first by linter.frontmatter.
• Intent — the file-level layer: a real id, a kind, and one EARS statement saying what the spec promises.
• four layers — the fixed structure of every spec: frontmatter (Intent), Constraints, Model, Properties. The linter never reads prose — everything the toolchain reasons about lives in these structured rows. See architecture.
• EARS — Easy Approach to Requirements Syntax: five fixed sentence patterns (Ubiquitous, Event-Driven, State-Driven, Unwanted-Behavior, Optional-Feature) with an imperative SHALL. A spec’s statement must match exactly one pattern; conformance is shape-only grammar checking. spk explain ears has the pattern table.
• kind — the type tag on a spec file (kind: intent, kind: profile) or a table row (invariant, effect, advisory, extension_point, deriving, …), drawn from closed sets: a value outside the set is a labeled finding, never silently accepted. See kinds.
• Constraints — the table of the spec’s claims (invariants, effects, advisories, extension points), with [[wiki-linked]] traces. Compiles to TOML.
• Model — the behavior table: states plus guarded transitions — a state machine. Compiles to a TLA+ module and is explored by spk model-check.
• Properties — the table of deriving properties, each with a generator + predicate. Compiles to proptest scaffolding and is executed by spk verify.
• corpus — the set of spec files a command operates on, usually a whole tree (openspec/specs/ here; consumer repos pass any dir). Lint discovers packs by scanning it; spk graph derives edges over it.
• lifecycle — the ordered stage gates a spec moves through — parse → lint → compile → model_check → verify — each stage gated on the previous one’s clean run. spk explain lifecycle states the gates; spk orchestrate drives the whole run.
• dogfooding — the repo eating its own dog food: every file in specs/ is a spec in the format specodelic defines, so the tool validates itself with every lint run (see self-hosting round, below).
• naming law — a spec file’s frontmatter id equals its filename stem with - ⇔ .: linter-graph_shape.md ⇔ id: linter.graph_shape.
• format_revision / Revision N — the format’s version stamp. Each corpus file states the current Revision N in its revision history, and the binary embeds format_revision (reported by spk --version --json); spk doctor warns when a corpus lags the binary, never fails.
• wiki-linked reference — a [[id]] link in a table cell pointing at another row or file. Typed reference fields are checked by spk graph and linter.referential_integrity.
• link kinds — the typed reference fields that connect rows: traces_to/derives_from trace provenance (derives_from is the coverage edge — a Property derives from its Constraint), emits/ observes are a typed effect protocol between files (an observation is not a dependency), satisfies consumes a published extension_point contract, supersedes replaces an older row. The authority is specodelic.md’s Reference Typing table.
• pack (domain pack) — a kind: profile spec file whose manifest tables declare typed sections, fiber kinds, and reference fields for a domain. Discovered by corpus scan (no config file); a consuming file opts in explicitly via a uses reference to the pack’s id. See packs.
• fiber kind — a kind declared by a pack. While the pack is active, the base closed kind set widens to base ∪ active-pack-fiber; the same token without an active pack fires a labeled finding.
• external checklist — a *.checklist.md file declaring items that must each be explicitly covered (mapped to real constraint/property rows) or waived with a rationale; checked by linter.external_completeness, which never gates a lifecycle stage.
• dual-format — one markdown file that parses as both a specodelic spec and an OpenSpec delta: the specodelic half (frontmatter + Constraints/Model/Properties) plus the openspec half (## ADDED Requirements mirrored verbatim in ## Requirements). One file, two parsers, requirement text authored once. spk explain dual-format carries the protocol and the migration recipe.

The toolchain and its output

• spk — the CLI binary; the crate is named specodelic.
• finding — one labeled rule violation a checker reports, carrying a rule_id (linter.<name>) and one-line semantics. Findings fail a stage (exit 1) and never ride a success-shaped envelope.
• envelope — the output wrapper every command emits through: JSON (ok, envelope_kind, data) for pipes, human-readable for TTYs. Failures carry a remediation hint. See errors.
• artifact — a compiled output on disk: <stem>.toml (Constraints), <stem>_props.rs (proptest scaffolding), <stem>.tla (TLA+ module), and <stem>.check.json (the model-check run report).
• scaffold — placeholder rows or sections that a template or spk migrate inserts so a file lints clean immediately, to be replaced with real content while staying green.
• staleness — compiled artifacts carry digests or fingerprints of the spec they were compiled from. spk verify recomputes them and rejects stale, foreign, or malformed reports with a rerun hint — a stored report is never rewritten to manufacture evidence.
• scope_sha256 — the digest in the <stem>.check.json run report binding the run’s structured content and consumed compiled artifacts. Prose edits and input reordering preserve it; any invariant-content change breaks it — so a report can never be reused as evidence for different inputs. See model_check.

Verification and checking

• lint-clean — the file passes the join of the gating linter checkers (exit 0 from spk lint). Rung 1 of the ladder; format-valid, not verified.
• guarantee ladder — the five rungs of what a green checkmark actually assures, from lint-clean to matches-oracle (and the better-design rung a counterexample puts you on). A file’s honest status is the highest rung it has evidence for. See verification boundaries.
• coverage — every Constraint row must have at least one Property deriving from it (p.derives_from == c), checked by linter.coverage. Uncovered constraints are invisible to the rest of the pipeline.
• proptest — Rust’s property-based-testing library: a generator produces many random inputs and a predicate asserts a property over each. The Properties table compiles to proptest scaffolding; spk verify executes it and reports the shrunk minimal failing input.
• TLA+ — a formal specification language for concurrent and stateful systems. The Model table compiles to a TLA+ module (.tla).
• stateright — the embedded Rust model-checking backend (the default): breadth-first exhaustive exploration of the compiled model within stated bounds (--max-depth, --max-states, --timeout-secs).
• TLC — the TLA+ reference model checker, opt-in as a JVM subprocess (--backend tlc --tlc-jar <tla2tools.jar>); a missing binary or jar is a missing_checker error, never a verdict.
• pc-automaton — how the compiled Model is interpreted for checking: a program-counter automaton whose state is an index into the Model’s states and whose actions are the transitions, explored by stateright with exactly the semantics the committed .tla emission commits to.
• kernel — the opt-in **kernel:** marker placing an expression cell in a closed atomic grammar (equality, comparisons, bounded ∀/∃, reference atomics like resolves/unique/acyclic) that evaluates three-valued (verified / counterexample / unknown) during model checks. A cell outside the grammar is a labeled failure, never prose silently ignored. See compile.
• kernel.binding — an opaque string (test node id, filter, or shell payload) on an invariant row, surfaced verbatim in compiled artifacts so external checkers (like ah) can bind their tests to spec claims; the toolchain never parses or interprets it.
• claim partition — the split a model-check run makes of each file’s invariant-kind Constraints into a required set (those opted into evaluation: a Rust fragment, a kernel claim, or a citation) and an explicitly unchecked set (prose-only). The run’s outcome is governed by the required set only — prose wording never implies evaluation. See model_check.
• model-check outcomes — the four terminal states of spk model-check: no_counterexample (every required claim verified over a completed bounded exploration), counterexample_found (a required claim was refuted), timed_out (the bound expired), and exploration_only (completed exploration over a corpus with no executable claims). The last two are honest non-failures — spk verify’s model gate is what rejects them as not clean.
• counterexample — a concrete input sequence a model checker found that violates a claim. The ladder’s better-design rung treats it as the design lesson, not a tool failure; the worked example shows the precedent.
• oracle — the executable ground truth a spec’s claims are measured against. Here that is the compiled property blocks and required invariant claims that spk verify executes; rung 4 of the ladder, matches-oracle, means exactly that they ran and passed.
• SUT — System Under Test: in classic property-based testing, the implementation the properties run against. In specodelic the checked “system” is the spec’s own compiled model and claims, so a verified verdict attests about the specification, never about a deployed implementation — see verification boundaries.
• advisory — a Constraint kind that records intent without enforcing: advisory rows can never gate a transition (by typing, not convention) and are never required in a model-check run — but their findings are still labeled, never silent.
• fan-in / fan-out — per-row counts of incoming and outgoing references in the derived graph. High fan-in flags a row too many others depend on — a spk refactor candidate.
• dangling reference — a [[id]] link pointing at nothing that exists. Detected by spk graph and linter.referential_integrity; a post-merge corpus with zero dangling references is the relint gate.

Ecosystem and workflow

• self-hosting round — the specs/ corpus is specodelic’s own specification, written in the format it defines, so the tool lints and verifies its own documentation the way it would a user’s spec. The round keeps that corpus lint-clean as the format grows, making the tool’s own spec the first consumer of every new rule. See status.
• ah / espectacular — the companion CLI enforcing spec↔test correspondence via scenario-contract TOMLs; read-only over openspec/ — it never enforces against the specs/ corpus.

FAQ — the questions a cold read asks

These are the questions three independent cold reads of this project (two external AI models in 2026-10, plus a third whose export is still pending) actually asked while onboarding. Every answer either states an editorial judgment or links to the authoritative page — answers never restate machine-generated truth (spk explain topics, lint-rule semantics, corpus-derived views), because a hand-copied restatement becomes an unconsulted claim the first time the format revises.

For the design-oriented questions (“why do the layers impose these constraints at all?”), see specs as the design substrate. For “which command when?”, see the decision guide.

Basics

What is specodelic in one sentence?

A specification format and CLI toolchain for AI agents: specs are plain markdown with a closed four-layer schema, checked by a linter that never reads your prose. The introduction and the glossary expand every term in that sentence.

Is this a documentation format or a testing tool?

Neither, exactly — it is a format with a checking pipeline. The structured tables are linted, compiled, model-checked, and verified; the prose stays free for humans. What a green check attests — and what it does not — is the subject of verification boundaries.

Should I use this for my hand-maintained codebase?

Probably not. The format presumes spec-first, agent-authored, regenerable code — its value comes from something mechanical consuming the structured rows (compiled properties, the TLA+ model, the contract gate). Under hand-maintained code the coverage/anchoring discipline is pure tax: every third-party evaluation of the format reached this verdict independently. The positioning section of USAGE.md states the assumption, the honest one-line test (“will anything mechanical consume the structured rows?”), and the cases where an ordinary design doc wins.

Why can’t I write prose and have the linter check it?

Deliberately not. The linter never parses prose, so prose is free to argue, motivate, and explain. Anything the toolchain reasons about must live in a structured row — a prose-only invariant stays explicitly unchecked and is never counted as verified (verification boundaries, rung 4), and spk conform reports prose-covered traces as unknown rather than silently passing them (conform).

Why is the schema closed? Why can’t I add a fifth table?

A closed schema is what makes every other guarantee stateable: row kinds are closed sets, every [[wiki-link]] is typed, and format evolution is additive-only through numbered revisions — the theory behind this is in theory.md, the mechanism in specodelic.md. Domain-specific structure goes through domain packs, which extend the format without a format revision.

Checks and guarantees

What does a green check actually mean?

It depends on which rung of the guarantee ladder you are standing on: lint-clean, well-modeled, checked-within-bounds, matches-oracle, better-design. Each rung presupposes the ones below it, and each is honest about what it does not assure.

Is my spec “done”?

A file’s honest status is the highest rung it has evidence for, never a single undifferentiated PASS. Lint-clean means format-valid; verified means the compiled property blocks executed and every opted-in invariant claim checked — and still not application correctness. Walk the ladder in verification boundaries.

model-check returned a counterexample — is the tool broken?

Usually the opposite: a refuted claim names the violated invariant, and the counterexample is often the design lesson rather than a tool failure. The worked example records the precedent — the checker found a two-step trace to a state the author swore was unreachable, and the over-claiming row turned out to be the bug.

What can the checkers NOT find?

Known limitations are stated up front, each backed by a runnable command — for example, coverage cannot detect a missing constraint. See verification boundaries — known limitations.

Workflows

Which command should I run when?

The decision guide routes “what do I have, what do I want” to the right verb — including the honest maturity notes on advisory verbs like spk refactor.

I have an existing system or oracle but no specodelic implementation — how do I check specs against it?

spk conform is the one verb that brings evidence from outside the spec: it classifies traces recorded from a legacy system, a curated case set, or a reference implementation against what the spec declares. The verdict taxonomy (permitted / forbidden / underspecified / unknown / unsupported) and the open- vs closed-world choice are in conform.

How do I get large numbers of scenarios out of a spec?

Two complementary verbs: spk model-check explores the compiled model’s reachable state space within a bound (model_check), and spk verify executes the compiled property blocks whose generators produce concrete cases (verify). For scenarios coming from outside the spec, use conform instead.

Can one spec be implemented in different languages or paradigms?

The layers are implementation-neutral by construction — the pattern of “several interchangeable implementations of one contract” is documented in USAGE.md §2.3. One honesty note: **rust:** predicate fragments are compiled and executed natively by model-check/verify; **py:** and **ts:** fragments are illustrative and are not executable (known limitations).

Format mechanics

A lint finding says linter.<something> — what does it mean?

Every finding carries its own rule id and one-line semantics string. spk explain lint-rules prints the catalog from the same table the linter emits from, and each rule has a page under Lint Rules in this book — start at the linter overview.

How do I safely rename an id, or merge two diverged branches?

spk rename rewrites the defining row, every referencing [[link]], and checklist mapped_ids as one in-memory-verified transaction (rename); spk merge --branch checks id collisions, dangling renames, and intersecting blast radii before you join the trees (merge).

Where are the docs agents read without repo access?

spk explain serves the distilled format guide from inside the binary — nine topics (format, ears, kinds, references, lifecycle, lint-rules, dual-format, packs, graph-views) — and llms.txt at the site root is the machine summary (For agents).

Ecosystem

How does specodelic relate to OpenSpec?

OpenSpec changes are the engineering-truth workflow; specodelic specs share the same grammar via the dual-format protocol, and ah/ espectacular enforces spec↔test correspondence read-only. The full division of ownership is in tool relationships.

Can I extend the format for my domain?

Through a domain pack: a kind: profile manifest declaring typed sections, fiber kinds, and reference fields — discovered by corpus scan, no config file. The using packs guide walks the whole loop. Six packs ship in-repo — five standard packs (data.lineage, numeric.predicates, empirical.registry, quant.finance, svc.contracts — the last still draft) plus the first cross-pack ## Requires pilot (bioimage.data).

Specs as the design substrate — a canvas for thinking about the system

The four layers are not documentation sections that later get implemented. They are the place where the system is designed: the contract you reason over while inventing, refining, and validating a design. An implementation — in Rust, Python, whatever paradigm — is a later, optional rendering of a model that already lives in the spec, and it is the rendering that must keep proving itself, never the other way around.

Provenance. This page is distilled from three independent cold-reads of the project by external AI models (2026-10, against v0.7.0); the questions their humans asked seeded the FAQ, and the answers were re-grounded against the current corpus before being written down here. Where this page and the format disagree, the format wins — spk explain format is the machine truth these paragraphs compress, and architecture holds for the lint pipeline’s pass structure.

The shift: the spec is the artifact

Most design docs describe a system that lives somewhere else — in a codebase, in someone’s head, in a slide deck. A specodelic corpus makes the design itself the load-bearing artifact:

• It is lintable — the closed schema means every design decision is in a place the toolchain can see.
• It is connected — the [[wiki-link]]s are typed foreign keys, so claims trace upward to the promise they serve and downward to the behavior that verifies them (architecture).
• It is checkable — the pipeline can challenge the design, not just its spelling (the design loop).

Each layer is a question you must answer

The format’s constraints are not arbitrary gatekeeping — each layer forces one design question to have an explicit, wired answer. If you skip the question, lint tells you where.

Intent — what do we promise? One EARS-patterned sentence in the frontmatter. If a feature cannot be stated in one sentence, the feature is not understood yet; the EARS patterns (kinds and statement, EARS) force the promise to be about a system response with defined conditions, not a vague ambition.

Constraints — what must always hold, and what may be observed? Invariants and effects, each a table row tracing to the Intent it serves. This is where you discover whether your invariants are actually invariant, and which observable outcomes are contractual rather than incidental (specodelic.md).

Model — what can happen? A state machine: states, guarded transitions. The guards must cite the Constraints — the checker demands the wiring — so “the model says so” always decomposes into “these named claims say so”. Writing the Model is where you find out that your constraints were silent about the failure paths (linter.model_shape).

Properties — what would convince us? Every constraint needs a deriving property with a generator and a predicate (coverage, linter.coverage). A claim with no way to challenge it is a wish, not a design decision.

The design loop

spk new → spk lint → spk compile → spk model-check → spk verify is usually presented as a CI pipeline. It works equally well as a thinking loop, run while designing:

1. Draft the layers — the scaffold from spk new teaches its own tables (quick start).
2. Lint early and often; every finding is self-describing, so each failed pass is one concrete design question (“this transition has no guard — what claim says when it may fire?”).
3. Compile and model-check to let the machine explore what you wrote; a counterexample_found verdict is the highest-value design moment, not a failure — see the better-design rung and the worked example, where the checker caught the author over-claiming a rejection state.
4. Verify what can execute; record what cannot, honestly (verification boundaries).

The loop converges on a corpus where every claim is wired, guarded, and either checked or explicitly unchecked — a design that can be handed to an implementer, human or agent, with an honest account of what has and has not been challenged.

Where the canvas ends

The format can force accountable design, not good design. A wrong but internally coherent model lints clean (that is rung 2 of the guarantee ladder, not a defect); the checkers can only challenge what you wrote, and a missing constraint is the blind spot they cannot see past (known limitations). The honest status of any corpus is the highest rung it has evidence for — this page is the canvas, the ladder is the audit.

Design conversations — the specodelic-design skill

The one-line summary: run design conversations that end in a lint-clean Specodelic spec (a four-layer markdown format — Intent, Constraints, Model, Properties).

The specodelic-design skill is a guided conversation procedure — Listen → Intent → Constraints → Model → Properties → Assemble — that ends in a spec the toolchain accepts. It ships inside the spk binary as a managed skill pack: the protocol prose, a format reference rendered from the same tables spk explain serves, and the book’s worked example embedded verbatim.

The procedure’s single authoring surface is the tracked source skill-packs/specodelic-design/SKILL.md — this page deliberately does not duplicate it. The worked example is reservation-order, the same file the binary embeds, so the skill and the book can never disagree.

Install it into your agent’s skill directory:

$ spk skill install            # default: ~/.claude/skills
$ spk skill install --dir ~/.config/agents/skills   # any target

Every installed file carries a managed marker; spk doctor reports a stale install (older binary) with the regenerate command, and a missing one only as an optional hint.

For the thinking behind the four layers the conversation builds, see the design canvas; for the questions a cold read asks, see the FAQ.

specodelic — the core format

id: specodelic kind: intent statement: “THE specodelic SHALL represent a feature’s intent, constraints, state model, and properties as one parseable markdown file conforming to a fixed schema.”

Specodelic

A feature’s specification is a markdown file with YAML frontmatter, a fixed set of tables, and wiki-link references between them. This file describes that format’s own constraints, lifecycle, and properties — it is a spec written in the format, about the tool that checks it (see USAGE.md §0 for the project/format/tool/subject terminology).

Purpose

A feature’s specification is a markdown file with YAML frontmatter, a fixed set of tables, and wiki-link references between them. This file describes that format’s own constraints, lifecycle, and properties — it is a spec written in the format, about the tool that checks it (see USAGE.md §0 for the project/format/tool/subject terminology).

Constraints

The four rows carrying the **kernel:** marker are this file’s executable slice — the min-expr kernel’s closed atomic grammar (add-min-expr-kernel), each backed by its own coverage property row. The remaining data-dependent cells stay informal by recorded decision, not by omission, and no new advisory class was invented to force them in: unique_id (an id is not a schema morphism — uniqueness has no acset-backed atomic), guard_required (¬(t.guard == ⊥) would conflate prose-guard presence with absence), every_state_used (needs ∨, outside the closed grammar), acyclic_traces (the union-graph DAG is not expressible in the closed grammar — per-morphism acyclicity is a strict weakening), and the kind-set/typing cells (outside the closed grammar). A cell migrates only when a Revision widens the closed grammar to carry it — a migration that would need a new advisory class is a migration bug, not a corpus fact.

Reference Typing

Which kind a reference field may point at — every reference field here is a typed foreign key. ref_kind_compatible is this table read as a constraint.

Model

States

• draft
• parsed
• linted
• compiled
• model_checked
• verified

Transitions

Checker Ownership

linted is not one flat conjunction — it is the join point of eight independently-specified checker files, each its own instance of this same format (a spec-of-a-linter-check, verifying a spec). This table replaces the constraint-by-constraint guard with a reference to where each constraint is actually enforced, and the partial order those checkers run in.

Two further checker files exist but sit outside this table on purpose (they are instances of the same format, just never gating): linter-observability.md — advisory findings on the warnings channel, exit 0 by its own advisory_severity invariant — and linter-external_completeness.md — runs only when a repo declares an external checklist, and its outcome never gates per orchestrate.md’s external_completeness_never_gating. Their absence from the table is a membership statement: linted is the join over the eight rows above only.

linted is an all-must-pass dependency gate over this diagram: lint fires only when every terminal node reports passed, not when constraints are checked in some fixed sequence; the two branches after linter-frontmatter.md (referential→graph→model, and ears-syntax / schema-shape) run independently of each other.

Properties

Notes

This file is itself a document instance of its own schema (Intent, Constraint, State, Transition, Property). Running this file through its own lint transition should produce zero findings — if it doesn’t, the format and its own description of itself disagree, the same way a self-hosting compiler that fails to compile its own source has a bootstrapping bug rather than an ordinary bug.

One thing the format cannot check about itself: whether no_boolean_columns is itself satisfiable without a boolean-shaped escape hatch somewhere in the tooling (e.g. a linter’s own pass/fail result). That’s outside 𝒦 — a property of the compiler, not of any instance it compiles — flagged as Needs Human Review rather than silently assumed.

Revision 2

Decomposing the linter into linter-frontmatter.md, linter-referential_integrity.md, linter-graph_shape.md, and linter-model_shape.md surfaced four gaps in Revision 1’s constraint list, now resolved and folded in above:

• id_matches_file — resolved as a structural rule, not left open: a file’s declared id must equal its filename with hyphens read as namespace dots (linter-frontmatter.md ⇒ linter.frontmatter). Applies uniformly to every spec file, since every file’s frontmatter kind is intent regardless of whether it sits at the top of the feature tree or describes one narrow checker.
• ref_kind_compatible — resolved by writing out 𝒦’s morphism typing explicitly (see Reference Typing table) instead of leaving it as an unstated assumption a checker would have had to invent.
• single_root_reachable — resolved as reachability from the file’s own declared intent specifically, not any intent in the repo, since the looser version would silently accept a cross-feature reference filed under the wrong id.
• every_state_used / every_transition_valid — folded in as prerequisites for model_present to mean anything downstream, since a dangling to field would otherwise reach the TLA+ generator undetected.

The lint transition’s guard was also restructured: the flat seven-clause conjunction from Revision 1 was itself an instance of the God-transition pathology modularity-diagnostician flags in code, just written in a guard field instead of a function body. It’s replaced with a reference to the Checker Ownership table, so linted is now legible as a limit over an explicit dependency diagram rather than an opaque AND of everything at once — the fix is the same move as extracting a God Object into cohesive collaborators, applied to a guard expression instead of a class.

Since this revision, linter-ears_syntax.md, linter-schema_shape.md, and linter-coverage.md were all written; none surfaced further gaps in the constraint list above (see each file’s own Notes section).

Revision 3

A Rule-of-5 review (rule-of-5-universal) of the full corpus found one CRITICAL correctness bug in Revision 2’s id_matches_file constraint, plus documentation drift left over from before the last three checker files existed. Both fixed here:

• id_matches_file was not invertible. The original rule (“hyphens read as namespace dots”) assumed a filename’s hyphens could be unambiguously mapped back to dots, but hyphens were also standing in for underscores within a segment (linter-graph-shape.md for id linter.graph_shape). dots_to_dashes⁻¹ doesn’t exist as a function when the forward map isn’t injective. Fixed by reserving - exclusively for the namespace dot and preserving _ literally in filenames; five files were renamed to match: linter-referential_integrity.md, linter-graph_shape.md, linter-model_shape.md, linter-ears_syntax.md, linter-schema_shape.md. Without this fix, the linter as specified would have rejected five of its own seven checker files — a bootstrapping failure the format’s own Notes explicitly claims should never happen.

Revision 4

Writing kinds.md — the standalone definition of 𝒦’s five objects, STATUS.md §4’s P0 item — surfaced one gap: nothing in Revision 3’s list required a Constraint row’s or Property row’s own kind column to come from a closed set. frontmatter_valid only ever checked the file-level kind == "intent"; a Property row with kind: "made_up" had no constraint anywhere rejecting it. Added constraint_kind_closed (kind ∈ {invariant}) and property_kind_closed (kind ∈ {unit, law}), each tracing to the corresponding row-shape constraint now specified in kinds.md. Enforcement landed the same session: linter-schema_shape.md now owns both (see its updated Checker Ownership row above).

• Stale “not yet written” notes removed from the Checker Ownership table and this section, left over from before linter-schema_shape.md and linter-coverage.md existed.

Revision 5

Checking this format against ten features a real polyglot tool ecosystem needed (non-gating quality signals, confidence-scored checks, scenario supersession, cross-language adapter contracts, self-reported-vs-verified claims, versioned shared dependencies, an ad hoc “needs human review” escape hatch, feedback/regression loops, priority-ordered fallback installs, and multi-target compilation) found that seven of the ten were already representable with the mechanisms above and needed no schema change — writing them down for the record, so the next reviewer doesn’t re-open them:

• Non-gating quality signals and “needs human review” as structure, not prose turned out to be the same gap, and it closes by finally exercising kind_field_extensible on Constraint.kind the way it was already exercised on Property.kind: adding advisory above. An advisory Constraint carries no obligation on any transition, for free, once guard’s Reference Typing row is narrowed to kind == invariant (see below) — non-gating by typing, not by the checker remembering to ignore it.
• Confidence-scored / statistical properties need no new mechanism: a Property’s predicate is already an unparsed boolean-valued expression (prose_untouched only forbids the parser reading rationale prose, not expr/predicate fields). A threshold like precision(check(corpus)) ≥ 0.95 is an ordinary unit Property with a fixed-corpus generator; the scoring algorithm behind the threshold is the feature’s own concern, not the format’s.
• Feedback/regression loops and priority-ordered fallback steps need no new mechanism either: States/Transitions is an open table, not a closed enum, so revise: verified → draft or a guard expressing “try A, else B, else C” via mutually-exclusive guard clauses both fit the existing Model section without touching 𝒦.
• Cross-language adapter/plugin contracts don’t need a sixth object in 𝒦 — they need their own file, the same way compile.md, model_check.md, and verify.md already got their own files instead of growing specodelic.md’s Model section.
• Self-reported-vs-verified claims and versioned shared dependencies both turned out to be downstream of the one real structural gap below, once supersession makes a row’s provenance and lineage traceable instead of overwritten.

One gap needed an actual addition, generalized rather than special-cased:

• supersedes. append_only_variants already guarantees a superseded row is never deleted — but nothing let a newer row declare what it replaces, so retirement had to be said in prose or not at all. Rather than add a bespoke “supersession” concept, supersedes is specified as one more row in the Reference Typing table — structurally identical to traces_to/derives_from, just self-typed (Constraint→ Constraint, Property→Property). Its cycle-freedom is checked as its own supersedes_acyclic invariant rather than folded into acyclic_traces, for the same reason Revision 2 broke the lint guard into independent checkers instead of one larger conjunction: lineage and intent-tracing are different graphs answering different questions, and merging them would recreate the God-invariant shape Revision 2 removed. Whether a row is “current” is never stored — it’s computed (superseded(x) ⟺ ∃ y. y.supersedes ∋ x) — so no boolean column is needed and no_boolean_columns covers it with no changes of its own.
• reference_field_extensible. Adding supersedes exposed that the Reference Typing table itself had no stated growth path, unlike the kind columns (kind_field_extensible, in kinds.md). The same append-only-by-Revision discipline now applies to the table as a whole, not just to the value sets inside it — the general rule this codifies is that a Revision’s job is to widen 𝒦’s typing, in either dimension, never to leave a second unwritten one beside the first.

Enforcement cost was uneven, and it’s worth recording why: linter- referential_integrity.md’s ref_kind_compatible needed zero code changes for either supersedes or the narrowed guard row, because it was already written to read allowed_targets(field) from this table rather than hardcoding it per field — the Reference Typing table is its only input. linter-schema_shape.md and linter-graph_shape.md were not so lucky: reference_field_extensible and supersedes_acyclic needed genuinely new local checks (an append-only-table diff, and a second small DAG check kept independent of acyclic rather than unioned into it — see each file’s own Notes), which are now implemented in both files rather than left pending.

Self-correction: reference_field_extensible’s first draft in this Revision forbade retyping an existing reference field at all — which its own paragraph above immediately violates, by narrowing guard from any Constraint to kind == invariant only. The rule above is the corrected version: a narrowing is permitted in the same Revision that introduces the kind-split it depends on, and only when it invalidates nothing that was previously valid (true here, since no advisory Constraint — and therefore no guard pointing at one — could have existed before this Revision introduced the kind itself).

Revision 6

Checked this format against a second, unrelated domain — a pure-Python, lazy, pipe-composed data library whose operations are grounded in category theory (an adjoint triple, a closed expression grammar, Moore-machine reducers). Unlike Revision 5, most of what looked missing here turned out to already be one Revision-5 pattern applied a second time, or an existing mechanism nobody had pointed at yet. Following this file’s and AGENTS.md’s own instruction to fold gaps back the same session rather than let them accumulate, both are done here, and the general workflow is now written up on its own in USAGE.md — read that file before writing a domain spec (one describing a piece of software, not this repo’s own linter), since everything below assumes its vocabulary (sealed enumeration, staged lifecycle, conformance-by-limit).

Simplified, not extended — three rules become one. kind_field_extensible (kinds.md), reference_field_extensible (Revision 5, above), and the old narrow wording of append_only_variants were the same rule discovered three times: an id-set governed by 𝒦 only grows, and only under a new Revision heading. append_only_variants above now states that once, for all three cases (variant-table ids, a kind column’s value-set, and the Reference Typing table’s field set); reference_field_extensible is retired as a separate row, and kinds.md’s kind_field_extensible is reworded to cite this constraint rather than restate its logic (see that file’s own Revision). This is the same move Revision 2 made collapsing a flat lint guard into the Checker Ownership table: one stated rule with several instances, not several hand-maintained copies that can drift out of sync with each other — which they had (Revision 5’s version of this rule already didn’t match kind_field_extensible’s wording word-for-word, despite saying the same thing).

One real addition: emits, giving State an output. A Moore machine is states, transitions, and an output function of state — the third part had nowhere to live, since kinds.md’s state_row_shape fixed State to exactly {id}. Rather than add a sixth 𝒦 object, this reuses exactly the move Revision 5 validated on guard: kind-split Constraint again ({invariant, advisory, effect} — one more kind_field_extensible-governed widening, now expressed via append_only_variants), then add one row to Reference Typing: emits | State | Constraint, kind == effect only. The new kind lives on Constraint, not on State or Transition, because a State’s output is a claim about a value, the same shape every other Constraint already makes — it needs no new row shape, only a new place a State may point at one. emits is optional: a state with no declared output is an ordinary automaton state, not a Moore state, and both are valid. linter-referential_integrity.md’s ref_kind_compatible needed zero code changes for this either, for the same reason Revision 5 noted for supersedes — except its wording needed a fix genuinely found this session: it named traces_to/derives_from/guard explicitly, which was already stale (it didn’t mention supersedes, added last Revision) and would have gone stale again with emits. Reworded there to read the Reference Typing table generically, matching what the check already does in practice.

Confirmed representable with no schema change, written up in USAGE.md as patterns rather than repeated here: a spec author’s own closed, exhaustively-matched enumeration (a “sealed AST”) is a Constraints-table id-set under the same generalized append_only_variants rule — it belongs there, not in Model/States, because it’s a closed value shape, not a lifecycle; a build-then-execute staging (laziness) is two ordinary guarded states, the same shape compile.md’s extracting → emitting already uses; conformance across multiple interchangeable implementations is the Checker Ownership pattern read backwards — N files each owning a slice of one shared Intent, joined as a limit — already fully built and running on this repo, just not yet named as a reusable pattern anywhere; and law_requires_cases’s two required cases were already a stated floor, now said explicitly in its own row above, so an adjunction or functor law needing unit/counit/naturality/triangle-identity cases adds them to its own property rather than waiting on a schema change.

Deliberately left alone: expr/generator/predicate remain unparsed strings. Revision 5 already noted this in passing for confidence thresholds; it’s restated here as a considered boundary, not an oversight — turning categorical laws into something a checker executes rather than a human reads is a different tool (a theorem prover), not a wider lint schema, and is out of scope for the same reason no_prose_field_parsed’s audit-vs-generator mismatch is flagged Needs Human Review rather than forced into a shape it doesn’t fit.

Revision 7

Checked this format against a third kind of gap: Julia-style multiple dispatch and, more sharply, Clojure-style protocols/multimethods, where a consumer extends a generic function or interface for their own type from a file the original author never edits and may never read — the expression-problem pattern, and the concrete mechanism behind the Open/ Closed Principle (closed for modification, open for extension). Every existing pattern in USAGE.md §2 assumes one file eventually enumerates its whole id-set (append_only_variants grows a set inside the file that owns it); an open-world conformer breaks that assumption structurally, not by omission — the same honest boundedness model_check.md already admits for unbounded recursive structures, here across files instead of depth.

Scope deliberately narrowed before specifying anything: an earlier draft of this Revision added a two-way implements edge and a single_root_reachable carve-out so the origin file could enumerate its own conformers. Discarded — verifying unknown, not-yet-written code was never a goal this format’s own boundedness rules could honestly support, and every previous Revision that tried to overreach past what’s checkable (no_prose_field_parsed’s parser-audit case, the categorical-law theorem-proving boundary) ended up walked back to a narrower, honest claim. The kept scope: this format publishes a contract an extension must satisfy, typed and lint-checkable as a well-formed statement; it never claims to verify who or what actually implements it. That’s a communication artifact, not an enforcement one — the same distinction no_boolean_columns’s Notes already draws between what 𝒦 can check about itself and what it can’t.

One new Constraint kind, one new one-directional reference field, both minimal:

• extension_point — constraint_kind_closed widens from {invariant, advisory, effect} to {invariant, advisory, effect, extension_point}, one more kind_field_extensible-governed widening (kinds.md gets the matching Revision). An extension_point row’s expr states the method signature(s) and behavioral expectation a conformer must provide — e.g. ∀ T conforming: symmetry(T)::SymmetryTag, canonical_order(T)::Vector{Int} — the same field every other Constraint kind already has, just aimed outward at code the origin file’s author doesn’t write.
• satisfies — one new row in the Reference Typing table: a Constraint on any file may point satisfies at an extension_point Constraint on any other file, declaring “this row is my conformance to that published contract.” Structurally identical to traces_to (a typed, outbound, one-directional pointer), deliberately not bidirectional like supersedes — the origin file gets no inbound edge and no obligation to know its conformers exist, by construction rather than by convention.

Two things this addition needs nothing new for, checked explicitly so the next reviewer doesn’t re-open them (AGENTS.md #3a):

• guard already excludes extension_point from gating. guard’s Reference Typing row already reads Constraint, kind == invariant only — advisory, effect, and now extension_point are all excluded by the same existing typing fact, not by a new “cannot gate” invariant. Exactly the advisory_cannot_gate precedent AGENTS.md #3a calls out: check the type system before adding a restatement.
• single_root_reachable needs no carve-out. A Constraint row carrying satisfies is still an ordinary row of its own file’s Constraints table, with its own ordinary traces_to pointing at that file’s own Intent — satisfies is an extra outbound pointer sitting beside traces_to on the same row, exactly the way guard and emits already coexist with it without affecting reachability. No forest, no second root, no change to the existing invariant at all — this is the concrete payoff of narrowing scope before specifying: the two-way implements draft would have needed a carve-out; the one-way satisfies doesn’t.
• linter-referential_integrity.md needs zero code changes, the same claim Revision 5 made for supersedes and Revision 6 made for emits, for the same reason: ref_kind_compatible already reads allowed_targets(field) generically from the Reference Typing table rather than naming fields by hand (Revision 6 fixed the one place its wording still hadn’t caught up to that). A fourth typed field is not a fourth special case there.

What this deliberately still doesn’t do: there is no way to ask “do all current and future conformers satisfy this contract” as a single checkable fact, and there won’t be one — that question is unbounded across files and time the same way an arbitrarily-nested expression tree is unbounded across depth (USAGE.md §4), and forcing a false sense of completeness onto it would be a worse outcome than leaving it explicitly unclaimed. What is checkable, per conformer, is entirely ordinary: ref_kind_compatible confirms a consumer’s satisfies row resolves to a real extension_point row of the right kind; whether that consumer’s own expr is actually faithful to the contract it names is the same kind of human/test-suite judgment call every other invariant row already relies on — satisfies adds traceability of intent to conform, not proof of conformance.

Note on an existing, narrower use of “Open/Closed” in this repo: STATUS.md §2 already lists “Switch/case rigidity (OCP violation)” as solved by append-only variant tables — that’s OCP within one file’s own governed id-set (a new case is an insert, not an edit to an existing match). This Revision’s extension_point/satisfies is OCP in the other, harder sense — extension by a party who never touches the origin file at all. Both are real and both now have a home; they shouldn’t be read as the same mechanism solving the same problem twice, which is exactly the kind of same-token-different-guarantee confusion AGENTS.md #6 already tracks (CLAR-001 through CLAR-003) — flagged here rather than silently left for a future reviewer to notice on their own.

Revision 8

The model-checking story became backend-pluggable, and Alloy left the corpus language. no_counterexample’s expr named “TLC/Alloy” — a tool coupling that model_check.md had already outgrown: its contract (bounded exploration, minimal counterexample, invariant named by id) is engine-neutral, so naming engines in the core invariant list pinned an implementation detail into the format itself.

• no_counterexample now says “the selected model-check backend”, and model_check.md’s Notes specify the backends: stateright (default, an embedded Rust model-checking crate — BFS exploration gives counterexample_is_minimal by construction; target_max_depth/timeout give the stated bound and timed_out) and TLC (opt-in, JVM subprocess, the reference engine for the .tla module).
• Alloy was dropped everywhere (compile.md, STATUS.md, USAGE.md, linter-model_shape.md): with a native default and a reference TLA+ engine it had no remaining role, and a SAT-based engine returns an instance, not a minimal trace — which would fight counterexample_is_minimal rather than satisfy it.
• model_check.backend_identified is new: a run report names the engine and version that produced it, so reports from different backends are attributable and comparable.

No variant table changed — this Revision rewords one constraint’s expr and adds one constraint to a non-core file, so append_only_variants is satisfied trivially. The .tla module remains an unconditional compile artifact regardless of backend (see compile.md’s Notes).

Revision 9

Declared outputs became observable claims. Revision 7 added extension_point/satisfies (a published contract and its outbound consumers) and Revision 6 added emits (a state’s Moore-machine output) — but nothing distinguished an effect that something must observe from one nobody watches: a spec could declare outputs that nothing observes and lint clean.

• The Reference Typing table gains observes: Constraint, any file → Constraint, kind == effect only — mirroring the satisfies precedent end to end (one optional column, one typed row, ref_kind_compatible needs zero special cases). A row carrying observes keeps its own ordinary traces_to, so single_root_reachable needs no carve-out.
• observes joins no acyclic edge set: linter-graph_shape.md’s acyclic union is closed and unchanged — an observation claim is not a dependency, so mutual cross-file observation is well-formed.
• Checking “every effect is observed” is linter-observability.md’s contract: advisory severity (warnings channel, exit 0), never gating a lifecycle transition in this Revision; gating is decided after dogfooding produces real friction evidence.
• kinds.md Revision 5 states the general rule this row relies on: optional typed reference columns may appear beside traces_to (satisfies, observes), superseding the “exactly four fields” reading of constraint_row_shape (HITL ticket specodelic-mp1 row 9, resolved by that Revision).

No variant table changed — one new Reference Typing row, grown under this heading per append_only_variants.

Revision 10

Two long-standing “Needs Human Review” questions were decided of record (HITL ticket specodelic-mp1 rows 7 and 8, user-approved 2026-09-30, advised by typed Jev evaluations, jev-1.13.0):

• Guard typing — hybrid (row 7). A transition guard may be prose, but when its gating condition corresponds to a declared constraint, the guard must cite it. The Reference Typing table’s guard row carries the rule; the target typing is unchanged (Constraint, kind == invariant only). This is the only policy consistent with both halves of the format’s own philosophy: guard is a typed foreign key (machine-readable edges exist where constraints exist), yet prose_untouched and the model-check reality (prose guards are uninterpreted — invariants_checked: []) mean banning prose outright buys nothing. The bridge pattern is precedented in the corpus: the hooks capability spec’s guards were bridged by appending typed citations to their prose. Banning prose would churn ~48 corpus rows into invented one-off constraint rows; leaving prose uncited strands half the corpus outside the typed graph.
• Reachability — tiered own-file intent (row 8). single_root_reachable is reworded: a row reaches the file’s OWN intent through own-file primary linkage (traces_to/derives_from chains resolved within the file); cross-file typed edges (guard citations of foreign constraints, satisfies, observes) are outbound leaves, never reachability paths — exactly the wording the table already gives satisfies/observes (“not a second reachability edge”). Enforcement is tiered: rows whose only connection is cross-file are advisory-flagged first; hard enforcement flips after corpus reconciliation (specodelic-cxq) anchors them. The strict own-file reading the old expr implied would fail ~150 of 375 corpus rows, much of it legitimate cross-file structure; the looser some-intent reading the shipped checker implemented silently accepts a cross-feature reference filed under the wrong id. Tiering keeps the wrong-file catch without a churn cliff.

No variant table changed — two existing rows reworded under this heading per append_only_variants; the guard field’s target set is narrowed not at all and the kind sets are untouched.

Revision 11

derives_from gains the same-kind law edge (Reference Typing row reworded; specodelic-cxq corpus reconciliation, 2026-09-30). A Property row whose own kind is law may point derives_from at a Constraint or at the same-kind Property — the top-level law it restates — because the checker files’ *_naturality laws instantiate exactly this file’s rename_naturality law, and banning that edge forced the corpus into either illegal targets or prose-only linkage. Well-formedness of the same-kind edge is not a new invariant: acyclic_traces already includes derives_from in its edge set, so a derivational cycle among laws is a lint finding, and coverage’s no_orphan_property still requires every derives_from target to resolve. A unit Property deriving from a Property remains a violation.

No variant table changed — one existing Reference Typing row reworded under this heading per append_only_variants; the target set WIDENS only for law sources, so nothing valid at Revision 10 is invalidated.

Revision 12

guard’s target set widens to admit a State (Reference Typing row reworded; specodelic-tik reconciliation of the shipped checker, 2026-09-30). Revision 10’s prose said “the target typing is unchanged (Constraint, kind == invariant only)”, but the reconciliation commit that shipped the hybrid guard policy (specodelic-cxq) also encoded the “has reached state X” pattern in graph.rs’s typing_violation and in the independent reference oracle: a transition guard may cite a State — the pattern graph.md’s own extract transition ([[specodelic.parsed]]), refactor.md’s analyze, and orchestrate.md’s start_lint all use. The table text never followed the checker; this Revision makes the table the authority again. A State citation records progress, it gates nothing — but it is a legal typed citation, and advisory Constraints still can never gate a transition, by typing, not by convention. The stale side-effects are reconciled in the same stroke: graph.md’s wrongly_typed_edge_rejected fixture/note (which contradicted graph.md’s own Model extract), USAGE.md’s §2.6 typing remark, and the embedded guide’s REFERENCE_TYPING row.

One existing Reference Typing row reworded and one deriving Property added under this heading per append_only_variants; the target set WIDENS only, so nothing valid at Revision 11 is invalidated — a unit Property (state_guard_citation_accepted) now pins the acceptance beside the existing rejection rows.

Revision 13

Law-row named cases become machine-checkable (specodelic-9qw, 2026-10-01). The law_requires_cases row is reworded: the cases a law requires are enumerated as **name:** case labels in the property’s own predicate — the form compile’s required_law_cases has parsed since the compile functor shipped — instead of free prose whose mention of a case name the linter could not tell apart from a declaration. The identity and associativity floor stands, unchanged, as a minimum; extra named cases (commutativity, idempotence, naturality, unit/counit, triangle identity, …) remain first-class — each becomes its own checkable declaration and its own proptest block. The floor is now lint-enforced (linter.law_cases, executing linter-coverage.md‘s every_law_has_cases) ahead of compile’s precondition gate, so required_law_cases’ unlabeled fallback survives only as defense-in-depth for input that skipped the gate.

One Constraint row reworded under this heading per append_only_variants; the case set WIDENS only (labels beyond the floor stay legal), so nothing valid at Revision 12 is invalidated — a law predicate whose cases lived only in prose now fails lint instead of silently passing.

Revision 14

The extension mechanism becomes first-class: domain packs (specodelic-dcx, add-domain-pack-mechanism, 2026-10-02). Independent vendors converged on the same extension moves — optional sections, per-kind case-label floors, new outbound reference fields — but nothing in the format named an extension, so pack vocabulary collided in the global closed kind sets. A pack is now a declared, discoverable, versioned artifact in the corpus itself; its full contract is [[packs]].

• frontmatter_valid reworded — the frontmatter-kind closed set grows once, narrowly: kind ∈ {intent, profile}. profile marks a pack file; every other rule for profile files is pack-fiber-relative (pack-shape checking, not base-set growth). Nothing valid at Revision 13 is invalidated — a pure widening.
• Reference Typing grows by uses — Constraint, any file → Intent of a kind: profile file, set-valued, outbound leaf. This is the one new generating morphism the mechanism requires; satisfies is NOT overloaded (conforming to a published extension_point contract and enabling a vocabulary fiber are different relations).
• Base closed sets freeze by policy — constraint_kind_closed, property_kind_closed, and the Reference Typing field set stop growing except by true format Revisions like this one; pack vocabulary is per-pack (namespaced, fiber-relative — the Grothendieck construction one level up), never global.
• Checker Ownership stays closed: the pack manifest’s structural rule (pack_shape, owned by [[packs]]) sits outside the eight-row gating table on the linter-observability precedent — it is conditional on pack discovery and advisory-first by its own contract, and a workspace with no kind: profile files lints byte-identically to Revision 13.

One Constraint row reworded and one Reference Typing row added under this heading per append_only_variants; every widening, no narrowing — the profile kind is opt-in per file and uses is optional per row.

Revision 15

Executable predicate fragments (specodelic-rjb, 2026-10-03 — the specodelic-mp1 row 7 option-C decision of record). The verified gate was unreachable by construction: every compiled predicate was a todo_predicate! placeholder that panics at execution, and the native model-check backend executed zero invariant predicates, so verify could never honestly report verified for any file. The way out is opt-in verbatim Rust:

• **The **rust:** marker.** A Property's predicatecell or an invariant-kind Constraint'sexprcell may carry exactly one**rust:marker; the cell text after it is the fragment — a Rust boolean expression emitted verbatim (compile.md'spredicate_fragment_opt_in, invariant_fragment_opt_in). Property fragments bind the block's generated values v0…(one per named generator, each aString`); invariant fragments bind the current state’s id. A cell without the marker compiles and checks exactly as before — pure widening.
• Verbatim, not interpreted. The fragment is user Rust, compiled by the Rust compiler, never re-parsed into a mini-language. Property fragments land in the proptest! artifact (verify’s existing scratch crate executes them); invariant fragments execute through a dependency-free scratch-crate BFS run whose engine attribution is native-bfs (model_check.md’s executable_invariants_execute) — exploration_only remains the honest outcome wherever no fragment is executable, and TLC, which cannot execute Rust, never claims clean.
• Rejections are labeled, never silent. A fragment on a law-kind Property (each case needs its own body), a non-invariant Constraint, or a Transition guard (the program-counter model has no data binding a guard could constrain — deferred of record) fails extraction with a label naming the rule (compile.md’s fragment_law_rejected, fragment_guard_rejected).
• Hygiene is defense-in-depth, not a sandbox (compile.md’s fragment_hygiene): fragments run on the invoking user’s machine with the invoking user’s privileges, exactly like every other compiled artifact; the banned-token list (unsafe, extern, include!, std::fs, std::process, std::net, std::env, asm!, Command) rejects the escape hatches a table cell should never legitimately need. A panicking fragment is a violation, never a pass (model_check.md’s invariant_totality).

No row of this file’s own tables changes in this Revision — the growth lives entirely in compile.md, model_check.md, and verify.md (fragments_reach_verified pins the now-reachable verdict). The only reworded rows sit in those files; nothing valid at Revision 14 is invalidated, and the proptest scaffolding’s element type simplifies from the GenVal wrapper to plain String in the same stroke.

Revision 16 — 2026-10-04

Closed language-tag fragments (specodelic-lf3, 2026-10-04 — design of record in openspec/changes/add-language-neutral-property-binding). Revision 15’s opt-in made predicate cells executable but Rust-bound: the **rust:** marker names the one supported language, and a cell wanting executable Python or TypeScript fragments has no honest form. This Revision widens the marker to a closed tag set — the format grammar grows once, per-language emission machinery stays out (it lives with espectacular’s contract binding and per-language emitters, none built here):

• The tag set is closed — {rust, py, ts}, the same closed-set discipline as property_kind_closed (the grammar owns the enumeration, a cell cannot carry a tag it doesn’t declare). The fragment-position rule and the non-empty-fragment requirement carry over verbatim per tag (compile.md’s fragment_language_closed, widening predicate_fragment_opt_in/invariant_fragment_opt_in’s grammar); **rust:** remains the fully specified case, byte-identical semantics.
• Unknown tags fail labeled, never silent — **go:** in fragment position is a labeled extraction failure naming the unknown tag and the closed set (sd1’s discipline: no silently ignored markers anywhere in the grammar; compile.md’s unknown_tag_rejected).
• Rust widening is pure — every cell that extracted under Revision 15’s grammar extracts byte-identical after it (compile.md’s rust_back_compat); a cell without any marker compiles exactly as before. Nothing valid at Revision 15 is invalidated.
• No emitter, no artifact — a **py:** or **ts:** fragment fails compile labeled, with a remediation hint naming the per-language emitter follow-up (compile.md’s no_emitter_labeled_failure). Executable emission for those languages is deferred of record to the per-language follow-ups (add-py-fragment-emission, add-ts-fragment-emission) — an accepted-tag-without-emitter would silently fall through to Rust, which is the vacuous outcome this Revision exists to prevent.
• Mention is not extraction — a **rust:**/**py:**/**ts:** occurrence anywhere other than fragment position (mid-span, in the defining rows of compile.md’s own table, or in prose between spans) is a mention of the mechanism and never extracts (compile.md’s mention_not_extraction, carrying sd1’s rule into the widened grammar).

No row of this file’s own tables changes in this Revision — the growth lives entirely in compile.md, mirroring Revision 15’s shape. Nothing valid at Revision 15 is invalidated, and the proptest/verify machinery is untouched.

Revision 17 — 2026-10-08

The min-expr kernel (add-min-expr-kernel, 2026-10-08). The data-dependent cells — the equational and bounded-quantified ones — had no defined semantics: the linter and model-check verify structure, but “resolves is unique” or “every reachable row satisfies a bound” was prose only. This Revision defines a decidable bounded fragment of the internal language of Set^𝒦 — the kernel — and makes it first-class format vocabulary:

• One opt-in marker, closed grammar. An expr cell opts in per cell with the kernel: marker in fragment position, under the same fragment-position rule as the executable-fragment markers; the expression is parsed against the closed atomic set — equality, comparisons, bounded ∀/∃ over the finite instances I(k), ∧/¬, and the reference-typed atomics resolves/unique/acyclic/reachable — and a non-member atomic fails labeled naming the atomic and the closed set (compile.md’s kernel_expr_opt_in). A cell without the marker compiles exactly as before — pure widening, nothing valid at Revision 16 is invalidated.
• Three-valued, never coerced. Evaluation over the finite instances reports exactly one of verified, counterexample, unknown; unknown is honest (the claim could not be discharged), propagates under Kleene rules, and never coerces to pass or to counterexample.
• Semantics never outrun proven machinery. Each v0 atomic names its grounding — acyclic/reachable on graph traversal, unique/resolves on acset traversal, equality, comparisons, and bounded quantifiers on model_check bounded evaluation — and an atomic without a grounding entry cannot ship. The widening law: a new atomic (pack predicates included) registers only if it is decidable over finite instances; a predicate failing the gate stays pack-side, checked by contract-TOML runners rather than by the kernel.
• Guard citations evaluate. A guard citation ([[a]] ∧ [[b]], ¬) is upgraded from inert annotation to a kernel-evaluated claim with the same three-valued honesty — an undischargable citation reports unknown, never pass. Executable guard fragments remain rejected of record: fragment_guard_rejected’s deferral condition (a data-carrying state space) is not met, and this Revision does not claim it.
• kernel.binding, the opaque bridge. An invariant-kind Constraint may carry a kernel.binding cell, extracted and surfaced verbatim and never interpreted by the toolchain; external checkers claim constraints through contract-TOML flags binding, and no registry is built (compile.md’s kernel_binding_opaque).

The grammar growth lives in compile.md (kernel_expr_opt_in, kernel_binding_opaque), mirroring Revision 16’s shape. This file’s own Constraints table carries the migrated kernel rows — total_refs, coverage, every_transition_valid, and supersedes_acyclic opt in with the kernel: marker; their per-file migration (USAGE.md examples, then this file’s invariants) was gated lint-clean and command-verified before this Revision’s heading, and this Revision declares the grammar those cells use. Nothing valid at Revision 16 is invalidated.

Revision 18 — 2026-10-08

Single-tree spec authoring: the id law derives spec.md from its parent directory (update-id-derivation-spec-md, specodelic-mcy, 2026-10-08). The old law — frontmatter.id == replace(stem(path), "-", ".") — forced every file named spec.md (the openspec-mandated filename, delta or deployed capability spec) to declare id: spec, and id: spec files resolved as self-contained (refs within the file only, total_refs/total_refs’s scoped index, and the command scope law’s isolated_scope_required arm). That structurally locked a two-tree architecture: a real-id corpus for the typed graph plus a deployed dual-format tree produced by per-repo hand-rolled deploy transforms. This Revision retires the distinction with one rule:

• The id law — expected_id_from_path(path): a file named spec.md derives its expected id from its PARENT DIRECTORY name (openspec/specs/ge-cli/spec.md → id: ge.cli); any other file derives from its own stem; - maps to the namespace dot, _ is literal; a bare spec.md with no parent directory falls back to the stem. A real-id corpus file dropped as openspec/specs/<cap>/spec.md yields exactly one finding — a mismatched id_matches_file.
• id: spec retires. dual_format_valid no longer polices the id (the naming law is the only id gate a dual-format file answers to), total_refs resolves every file corpus-wide (the self-containment scoping and its bare-local arm are gone — real-id files are distinguished by their own ids, so the false-resolution CORR-001 guarded against needed the id: spec collision to exist), and the command scope law reduces to duplicate_corpus_identity (model_check.md’s isolated-scope rule retired with its subject). Real-id dual-format files compose like any corpus; a same-id pair (transitionally: an active change’s delta and its deployed spec) is refused by the identity law on command paths.
• Scaffolds teach the single tree. spk new targets openspec/specs/<id>/spec.md by default; spk migrate generates the real derived id in the frontmatter it scaffolds. New users cannot produce the two-tree distinction.

Pure widening plus one narrowing of dead machinery: nothing valid at Revision 17 is invalidated — a file that satisfied the old law still satisfies the new one (stem files were already stem-derived; spec.md files under capability directories now satisfy the law with their real ids, which the old law rejected — but no corpus content at Revision 17 depended on that rejection being the only legal reading). The rename tool’s filename law (rename.md’s new_id_matches_filename) inherits expected_id_from_path verbatim.

Revision 19 — 2026-10-24

Change deltas go plain; the layer rides beside (add-delta-layer-sidecar, specodelic-s8fg Stage 2). Stage 1 (2026-10-19) made deployed capability specs 1.x-strict-valid by stripping delta sections at deploy; the remaining 1.x rejections were the dual-format change deltas themselves — the byte-identical ## Requirements mirror and the layer tables in the same file. This Revision retires the dual-format delta class with one rule:

• Plain deltas + sidecar. A change delta under openspec/changes/<id>/specs/<cap>/ is a plain openspec file — ## ADDED/MODIFIED/REMOVED Requirements (plus ## Purpose), no frontmatter, no layer tables, no mirror; openspec validate is its gate. The specodelic layer (frontmatter + Constraints/Model/Properties) is carried by a sibling layer.md sidecar — a real, corpus-linted specodelic file whose traces_to citations resolve corpus-wide.
• The id law gains the sidecar arm. expected_id_from_path: a file named layer.md derives its expected id from its PARENT DIRECTORY name plus a .layer suffix (specs/cap-a/layer.md → id: cap.a.layer) — the sibling of the spec.md rule, keeping sidecars per-capability unique and co-archived with their delta. id: spec’s retirement logic (Revision 18) is untouched.
• The mirror retires by construction. requirement_drift and dual_format_valid’s delta-pairing arm police the pairing of a delta section with a same-file ## Requirements mirror — a shape plain deltas can no longer produce without failing openspec validation. Both retire; the dual-format capability spec class (deployed openspec/specs/<cap>/spec.md) keeps every other rule unchanged. migrate’s mirror generation retires with it — the wrap path now scaffolds the sidecar.

The retirement narrows exactly the shape the corpus already stopped authoring: spec-integration’s intent of record (Revision 18 era) already declared “change deltas stay plain openspec files”, and no deployed capability spec is invalidated — the capability-spec class keeps every rule it had. archive-companion’s deploy re-assembly (openspec applies, the companion re-attaches the layer from the archived sidecar) is tool semantics, recorded in archive-companion.md — not a format law.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: referential_integrity

• WHEN arbitrary_spec_file()
• THEN ∀ ref ∈ file: lookup(ref) ≠ None
• VERIFIES [[specodelic.referential_integrity]]

Scenario: acyclicity

• WHEN arbitrary_spec_repo()
• THEN is_dag(traces_to_graph(repo))
• VERIFIES [[specodelic.acyclicity]]

Scenario: rename_naturality

• WHEN arbitrary_spec_repo(), arbitrary_id_rename()
• THEN identity: rename(I, a, a) == I associativity: rename(rename(I,a,b), b,c) == rename(I,a,c) naturality: compile(rename(I)) == rename(compile(I))
• VERIFIES [[specodelic.rename_naturality]]

Scenario: filename_convention

• WHEN (id, mismatched_filename) pairs
• THEN check(id, filename) == failed
• VERIFIES [[specodelic.filename_convention]]

Scenario: typing_enforced

• WHEN guard_field_pointing_at_a_property_row()
• THEN check(file) == failed
• VERIFIES [[specodelic.typing_enforced]]

Scenario: own_intent_reachable

• WHEN spec_repo_with(disconnected_constraint_cluster: true)
• THEN check(repo) == failed
• VERIFIES [[specodelic.own_intent_reachable]]

Scenario: model_well_formed

• WHEN spec_file_with(transition.to_not_in_states: true)
• THEN check(file) == failed
• VERIFIES [[specodelic.model_well_formed]]

Scenario: advisory_cannot_gate

• WHEN guard_field_pointing_at_an_advisory_constraint()
• THEN check(file) == failed
• VERIFIES [[specodelic.advisory_cannot_gate]]

Scenario: state_guard_citation_accepted

• WHEN transition_guard_citing_a_declared_state()
• THEN check(file) == passed — the “has reached state X” guard pattern (Revision 12); a State target gates nothing, it records progress — but it is a legal typed citation
• VERIFIES [[specodelic.state_guard_citation_accepted]]

Scenario: supersedes_cross_kind_rejected

• WHEN constraint_row_with(supersedes: a_property_row_id)
• THEN check(file) == failed
• VERIFIES [[specodelic.supersedes_cross_kind_rejected]]

Scenario: constraint_derives_from_rejected

• WHEN constraint_row_with(derives_from: a_constraint_row_id)
• THEN check(file) == failed — the Appears-on column is normative, not descriptive: derives_from appears on Property rows only (decided of record 2026-10-01, specodelic-huf; a constraint is derived FROM by properties, it does not derive), and ref_kind_compatible reads the column source-side the same way it already reads supersedes’ same-kind rule
• VERIFIES [[specodelic.constraint_derives_from_rejected]]

Scenario: supersedes_cycle_rejected

• WHEN spec_repo_with(supersedes_cycle: length ≥ 2)
• THEN check(repo) == failed
• VERIFIES [[specodelic.supersedes_cycle_rejected]]

Scenario: no_stored_superseded_flag

• WHEN schema_with(explicit is_superseded: bool column)
• THEN check(schema) == rejected — supersession status is derived (superseded(x) ⟺ ∃ y. y.supersedes ∋ x), never stored
• VERIFIES [[specodelic.no_stored_superseded_flag]]

Scenario: emits_cannot_target_non_effect

• WHEN emits_field_pointing_at_an_invariant_constraint()
• THEN check(file) == failed — same shape as advisory_cannot_gate, mirrored onto the other direction of the kind-split
• VERIFIES [[specodelic.emits_cannot_target_non_effect]]

Scenario: satisfies_wrong_kind_rejected

• WHEN satisfies_field_pointing_at_an_invariant_constraint()
• THEN check(file) == failed — same shape as advisory_cannot_gate and emits_cannot_target_non_effect, mirrored onto the third kind-typed reference field
• VERIFIES [[specodelic.satisfies_wrong_kind_rejected]]

Scenario: extension_point_needs_no_reachability_carveout

• WHEN constraint_row_with(satisfies: an_extension_point_in_another_file, traces_to: own_file_intent)
• THEN check(row) == passed — satisfies adds no reachability obligation; the row is reachable the ordinary way, through its own traces_to
• VERIFIES [[specodelic.extension_point_needs_no_reachability_carveout]]

Scenario: frontmatter_missing_field_rejected

• WHEN frontmatter_missing(one of id, kind, statement)
• THEN check(file) == failed
• VERIFIES [[specodelic.frontmatter_missing_field_rejected]]

Scenario: guardless_transition_rejected

• WHEN transition_row_with(empty guard cell)
• THEN check(file) == failed
• VERIFIES [[specodelic.guardless_transition_rejected]]

Scenario: non_ears_statement_rejected

• WHEN statement_outside_the_five_ears_patterns("the system should maybe work")
• THEN check(file) == failed
• VERIFIES [[specodelic.non_ears_statement_rejected]]

Scenario: multi_intent_join_rejected

• WHEN row_id_joined_to_two_intents_via_and()
• THEN check(file) == failed
• VERIFIES [[specodelic.multi_intent_join_rejected]]

Scenario: coverage_gap_flagged

• WHEN spec_file_with(constraint_with_no_deriving_property: true)
• THEN lint(file) reports rule == failed
• VERIFIES [[specodelic.coverage_gap_flagged]]

Scenario: law_missing_case_rejected

• WHEN law_property_missing("associativity")
• THEN check(file) == failed
• VERIFIES [[specodelic.law_missing_case_rejected]]

Scenario: orphan_state_rejected

• WHEN state_appearing_in_no_transition()
• THEN check(file) == failed
• VERIFIES [[specodelic.orphan_state_rejected]]

Scenario: missing_model_section_rejected

• WHEN spec_file_without_states_or_transitions()
• THEN check(file) == failed
• VERIFIES [[specodelic.missing_model_section_rejected]]

Scenario: invariant_violation_blocks_verify

• WHEN model_with_a_violated_invariant()
• THEN check(model_check) == failed
• VERIFIES [[specodelic.invariant_violation_blocks_verify]]

Scenario: failing_proptest_blocks_verify

• WHEN compiled_proptest_block_that_fails()
• THEN check(verify) == failed
• VERIFIES [[specodelic.failing_proptest_blocks_verify]]

Scenario: prose_does_not_affect_lint

• WHEN two_specs_identical_except_rationale_prose()
• THEN lint(a) == lint(b) — differing prose never changes a lint result
• VERIFIES [[specodelic.prose_does_not_affect_lint]]

Scenario: silently_shrunk_id_set_rejected

• WHEN (r, r') where a 𝒦-governed id-set member was removed with no Revision heading
• THEN check(revisions) == failed
• VERIFIES [[specodelic.silently_shrunk_id_set_rejected]]

Scenario: constraint_kind_out_of_set_rejected

• WHEN constraint_row_with(kind: "made_up")
• THEN check(file) == failed
• VERIFIES [[specodelic.constraint_kind_out_of_set_rejected]]

Scenario: property_kind_out_of_set_rejected

• WHEN property_row_with(kind: "audit")
• THEN check(file) == failed
• VERIFIES [[specodelic.property_kind_out_of_set_rejected]]

kinds — closed kind value sets

id: kinds kind: intent statement: “THE kinds spec SHALL define the field set, sub-kind values, and shape-validity rule for each of the five schema objects (Intent, Constraint, State, Transition, Property) that every specodelic file instantiates.”

Kinds

The five objects of 𝒦 — Intent, Constraint, State, Transition, Property — are referenced constantly throughout this repo but have never been specified as subjects in their own right (STATUS.md §4, P0). This file is that specification: for each kind, its exact field set and which values its own internal kind column (where it has one) may take. Every later checker — linter.frontmatter through linter.coverage — assumes a row has already been correctly bucketed into one of these five before it runs its own check; this file is what makes that bucketing itself a checkable fact instead of an unstated assumption.

Purpose

The five objects of 𝒦 — Intent, Constraint, State, Transition, Property — are referenced constantly throughout this repo but have never been specified as subjects in their own right (STATUS.md §4, P0). This file is that specification: for each kind, its exact field set and which values its own internal kind column (where it has one) may take. Every later checker — linter.frontmatter through linter.coverage — assumes a row has already been correctly bucketed into one of these five before it runs its own check; this file is what makes that bucketing itself a checkable fact instead of an unstated assumption.

Constraints

| id | kind | expr | traces_to | satisfies | |————————|———–|——————————————————————————————————————————————————|–––––––––––| | kind_enum_closed | invariant | the five kinds are exactly {Intent, Constraint, State, Transition, Property}, one per top-level section of a spec file (frontmatter, Constraints table, Model/States, Model/Transitions, Properties table) | [[kinds]] | | | intent_row_shape | invariant | an Intent row is the file's frontmatter block; its fields are exactly {id, kind, statement}, with kind == "intent", plus optionally-declared frontmatter keys (currently checked_against_core, per AGENTS.md's convention — see Revision 7) | [[kinds]] | | | constraint_row_shape | invariant | a Constraint row is one row of the Constraints table; its base fields are exactly {id, kind, expr, traces_to}, optionally followed by typed reference columns — each such column must be declared in specodelic.md's Reference Typing table (currently satisfies, observes) and carries no meaning beyond that typing; kind ∈ {invariant, advisory, effect, extension_point}, extended per-file by the active packs' declared kinds (openspec/specs/packs/spec.md fiber kinds — never narrower, see linter-schema_shape Notes) | [[kinds]] | | | state_row_shape | invariant | a State row is one bullet under Model/States; its fields are exactly {id, emits?} and it has no kind column of its own — states are named variants, never a typed column; emitsis optional and, when present, must resolve to a Constraint with kind == "effect" (seespecodelic.md's Reference Typing table) — a state with no emits is a bare automaton state, not a Moore state, and both are well-formed | [[kinds]] | | | transition_row_shape | invariant | a Transition row is one row of the Model/Transitions table; its fields are exactly {id, from, to, guard}, with no kind column of its own | [[kinds]] | | | property_row_shape | invariant | a Property row is one row of the Properties table; its fields are exactly {id, kind, derives_from, generator, predicate}, with kind ∈ {unit, law}, extended per-file by the active packs' declared kinds (openspec/specs/packs/spec.md fiber kinds — never narrower, see linter-schema_shape Notes) | [[kinds]] | | | kind_field_extensible | invariant | a Constraint or Property row's own kind value-set is one instance of [[specodelic.append_only_variants]] — it grows only under a new Revision heading in this file, never silently | [[kinds]] | | | kind_assignment_failure | effect | kinds.kind_assignment_failure(detail) | [[kinds]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | shape_check_failure | effect | kinds.shape_check_failure(detail) | [[kinds]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] |

Model

States

• unclassified
• kind_assigned
• shape_checked
• passed
• kind_failed (emits: [[kinds.kind_assignment_failure]])
• shape_failed (emits: [[kinds.shape_check_failure]])

Transitions

Properties

Notes

Fiber-kind extension of the base subkind sets (2026-10-03, beads specodelic-ung): a domain pack’s ## Kinds rows declare pack-qualified fiber kinds (e.g. empirical.statistic), and a base Constraint/Property row’s kind column accepts them when the pack is active for the file — the closed-set walkers’ effective set is base ∪ active-pack-fiber, never narrower (the base sets above do not grow; kind_field_extensible‘s append-only discipline is untouched — the extension is per-fiber, governed by openspec/specs/packs/spec.md, and dissolves when the pack is not active, firing the labeled finding instead of passing silently). The empirical-registry pack is the first consumer: its kind targets the base Properties table’s kind column directly (the sibling packs’ kinds live in pack-added sections, which is why they never needed this).

Two different things are called “kind” in this repo, and they must not be conflated. 𝒦’s five objects (Intent, Constraint, State, Transition, Property) are what this file calls kinds — which section of a spec file a row lives in. Separately, two of those kinds carry their own kind column as one of their fields: a Constraint row’s kind (currently only invariant) and a Property row’s kind (unit or law). These are sub-classifications within an already-assigned 𝒦-kind, not alternate values of it — a Property row with kind: "law" is still a Property in 𝒦’s sense, never a sixth object. Flagging this as CLAR-002 (same shape as STATUS.md’s open CLAR-001, the coverage/linter.coverage collision): worth an explicit rename in a future revision (e.g. subkind for the column, reserving kind for the 𝒦-level classification alone) rather than leaving two meanings on one word. Not resolved here, since renaming a live column is exactly the kind of change that should go through rename_naturality, not be done by hand.

property_row_shape’s kind ∈ {unit, law} is the authoritative home for the enum linter-schema_shape.md’s EXCL-001 wants a third member added to (kind = "audit", for claims like no_prose_field_parsed that are about the parser’s implementation rather than about spec-file content). When EXCL-001 is actioned, this file’s property_row_shape constraint is what gets a new Revision, and property_row_bad_subkind_rejected’s generator would need to change from a rejection case to an acceptance case for kind: "audit" specifically.

A gap surfaced writing this file, folded into specodelic.md as Revision 4 (same session, per AGENTS.md): nothing before this file required a Constraint row’s kind or a Property row’s kind to come from a closed set at all — frontmatter_valid only ever checked the file-level kind == "intent". A Property row with kind: "made_up" had no constraint anywhere rejecting it. constraint_row_shape and property_row_shape above close that, and specodelic.md now carries matching top-level invariants (constraint_kind_closed, property_kind_closed) tracing back to this file. Follow-up closed the same session: linter-schema_shape.md now owns and enforces both — see its kind_ok transition and the two ..._kind_invalid_rejected properties.

Revision 2

constraint_row_shape’s kind set widens from {invariant} to {invariant, advisory} — kind_field_extensible exercised exactly as it was designed to be, one Revision heading per widening, nothing silent. An advisory Constraint is still fully a row of the Constraints table (same four fields, same table); the only place its meaning differs is outside this file entirely, in specodelic.md’s Reference Typing table, which now types guard’s target as Constraint, kind == invariant — this file owns row shape, not what other rows may reference a row, so that cross-row rule correctly lives there and not here. property_kind_closed is untouched: EXCL-001’s pending audit value is a separate, still-open question and this Revision takes no position on it.

Revision 3

Two changes, both from specodelic.md Revision 6, folded in here the same session per AGENTS.md:

• constraint_row_shape’s kind set widens again, from {invariant, advisory} to {invariant, advisory, effect}. Same pattern as Revision 2 — one more kind_field_extensible-governed widening, row shape itself untouched (still {id, kind, expr, traces_to}). What an effect-kind Constraint means to other rows is again a cross-row fact that lives in specodelic.md’s Reference Typing table, not here: only emits may target one, the same way only guard may target an invariant one.

• state_row_shape gains an optional field, emits. This is a row-shape change, unlike the two kind widenings above — State’s field set moves from {id} to {id, emits?}, which is why it’s stated as its own bullet rather than folded into the kind_field_extensible framing. emits gives a State the output half of a Moore machine (states, transitions, and a function from state to output — only the first two had anywhere to live before this). Making it optional rather than required means a plain automaton state and a Moore state are both well-formed State rows; nothing about existing specs (none of which use emits) becomes invalid by this widening, so variant_set_grows_only- style backward compatibility holds automatically. See USAGE.md for the worked pattern (a reducer’s three phases, each with its own emits).

• kind_field_extensible’s wording was also corrected, independent of either change above: it used to restate, in its own words, the same “grows only via Revision” rule specodelic.md’s append_only_variants already stated for variant tables — the two had drifted slightly out of sync (compare Revision 5’s wording of append_only_variants against this file’s kind_field_extensible at the time). specodelic.md Revision 6 generalized append_only_variants to cover kind value-sets and the Reference Typing table too; this file’s row now just cites that one rule instead of keeping a second copy of the logic.

Revision 4

constraint_row_shape’s kind set widens a third time, from {invariant, advisory, effect} to {invariant, advisory, effect, extension_point}, folded in from specodelic.md Revision 7 the same session per AGENTS.md. Same pattern as Revisions 2 and 3 — row shape itself is untouched (still exactly {id, kind, expr, traces_to}); only the closed value-set kind_field_extensible governs grows by one member. An extension_point row states a contract a consumer’s code must satisfy (a method signature, a behavioral expectation) rather than an invariant this file’s own author enforces — what makes a Constraint reference that row meaningful lives, as with effect/emits, entirely outside this file, in specodelic.md’s Reference Typing table, which now types a new field, satisfies, at Constraint, kind == extension_point only. constraint_row_extension_point_accepted above is the matching acceptance case, added the same way constraint_row_advisory_accepted and constraint_row_effect_accepted were.

Revision 5

constraint_row_shape stated its fields as exactly {id, kind, expr, traces_to} — but the format already carries optional typed reference columns beside traces_to: Revision 7 of specodelic.md added satisfies (USAGE §2.6’s five-column example), and Revision 9 adds observes. The “exactly four fields” reading and the Reference Typing table contradicted each other — HITL ticket specodelic-mp1 row 9 asked which governs; this Revision answers: the table governs.

• constraint_row_shape now states the general rule: base fields are exactly {id, kind, expr, traces_to}, plus optional typed reference columns — each such column must be declared in specodelic.md’s Reference Typing table, and carries no meaning beyond that typing (the table row is the whole contract). No observes special case — the next field costs one typing row, zero shape edits.
• No existing file changes meaning: every optional column in use (satisfies) was already valid under the table-driven reading; the narrowing “exactly four” was the only reading it violated, and no checker enforced it.

Row shape is otherwise untouched — the same general-rule-instead-of-special-case move as kind_field_extensible.

Revision 6

EXCL-001 is resolved by dissolution — property_row_shape’s kind set stays {unit, law} and no audit member is added (HITL ticket specodelic-mp1 row 5, user-approved 2026-09-30, advised by a typed Jev evaluation, jev-1.13.0, confidence 1.00).

The only instance that ever motivated an audit kind was linter-schema_shape.md’s no_prose_field_parsed — a claim about the parser’s implementation, framed as “verified by code audit, not by a runnable PBT case”. That framing was wrong: the claim is mechanically testable by a planted-prose differential parse (generate a spec with prose in rationale/description, parse, assert no parsed row contains it). An enum member whose definition is “not machine-verified” would crack the format’s promise that Properties are runnable, and kind_field_extensible should be spent when the shape genuinely needs it — not on a singleton. The rewrite of that property to a runnable unit row lands with the corpus-reconciliation work (specodelic-cxq); a genuinely unrunnable implementation claim remains a possible future widening, on demand and under a Revision heading, as always.

Revision 7

Two spec-text fixes from the Rule-of-5 corpus review (2026-10-01, specodelic-x4w, CORR-002 + CORR-003, both MEDIUM) — rewordings that narrow nothing, folded under one Revision heading:

• reject’s guard was a tautology. It read ¬(intent_row_shape ∧ constraint_row_shape ∧ state_row_shape ∧ transition_row_shape ∧ property_row_shape) — but no single row can satisfy all five mutually-exclusive shape conditions (a frontmatter block is never also a table row), so the conjunction is always false and reject fired unconditionally from shape_checked: well-formed rows had both accept and reject enabled — a non-deterministic model. Fixed to negate the applicable disjunct: ¬((row.kind==Intent ∧ intent_row_shape) ∨ (row.kind==Constraint ∧ constraint_row_shape) ∨ …) — exactly one disjunct applies per row, and its negation is the rejection condition. Contrast (kept as-is): linter-graph_shape.md’s same-shaped reject is correct — its four conjuncts co-apply to one artifact (the whole graph), not to five alternative shapes of one row.
• intent_row_shape acknowledges optionally-declared frontmatter keys. It read “fields are exactly {id, kind, statement}”, but ten corpus files carry a fourth key, checked_against_core (the AGENTS.md convention recording a core-check pass) — documented in openspec/specs/AGENTS.md, undeclared in the format. constraint_row_shape received the optional-declared-columns carve-out in specodelic.md Revision 9’s move (this file’s Revision 5); the Intent layer never did. Now: base fields stay exactly {id, kind, statement}, plus optionally-declared frontmatter keys (currently checked_against_core, per AGENTS.md’s convention). No linter change accompanies this — frontmatter_valid is a subset check (it never rejects unknown keys) and stays one; the spec text is the only guard, and the pinning fixture (extra_frontmatter_key_lints_clean, tests/cli.rs) asserts the tool-level reading: a spec carrying the key lints clean, and the parser captures it as an extra field rather than dropping it.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: unknown_kind_rejected

• WHEN row_belonging_to_a_sixth_section("Actions")
• THEN check(row) == failed
• VERIFIES [[kinds.unknown_kind_rejected]]

Scenario: intent_missing_statement_rejected

• WHEN intent_row_without("statement")
• THEN check(row) == failed
• VERIFIES [[kinds.intent_missing_statement_rejected]]

Scenario: constraint_row_extra_field_rejected

• WHEN constraint_row_with(extra_field: "guard")
• THEN check(row) == failed
• VERIFIES [[kinds.constraint_row_extra_field_rejected]]

Scenario: state_row_with_extra_field_rejected

• WHEN state_row_with(extra_field: "kind")
• THEN check(row) == failed
• VERIFIES [[kinds.state_row_with_extra_field_rejected]]

Scenario: transition_missing_guard_rejected

• WHEN transition_row_without("guard")
• THEN check(row) == failed
• VERIFIES [[kinds.transition_missing_guard_rejected]]

Scenario: property_row_bad_subkind_rejected

• WHEN property_row_with(kind: "audit")
• THEN check(row) == failed
• VERIFIES [[kinds.property_row_bad_subkind_rejected]]

Scenario: subkind_addition_without_revision_rejected

• WHEN diff_adding_subkind_value_with_no_new_Revision_heading()
• THEN check(diff) == failed
• VERIFIES [[kinds.subkind_addition_without_revision_rejected]]

Scenario: constraint_row_advisory_accepted

• WHEN constraint_row_with(kind: "advisory")
• THEN check(row) == passed
• VERIFIES [[kinds.constraint_row_advisory_accepted]]

Scenario: constraint_row_effect_accepted

• WHEN constraint_row_with(kind: "effect")
• THEN check(row) == passed
• VERIFIES [[kinds.constraint_row_effect_accepted]]

Scenario: state_row_emits_accepted

• WHEN state_row_with(emits: an_effect_kind_constraint_id)
• THEN check(row) == passed
• VERIFIES [[kinds.state_row_emits_accepted]]

Scenario: state_row_without_emits_still_passes

• WHEN state_row_with(fields: {id}) — no emits
• THEN check(row) == passed — emits is optional, not a second required field
• VERIFIES [[kinds.state_row_without_emits_still_passes]]

Scenario: state_row_emits_wrong_kind_rejected

• WHEN state_row_with(emits: an_invariant_kind_constraint_id)
• THEN check(row) == failed
• VERIFIES [[kinds.state_row_emits_wrong_kind_rejected]]

Scenario: constraint_row_extension_point_accepted

• WHEN constraint_row_with(kind: "extension_point")
• THEN check(row) == passed
• VERIFIES [[kinds.constraint_row_extension_point_accepted]]

Scenario: well_formed_row_passes

• WHEN arbitrary_well_formed_row_of_one_kind()
• THEN check(row) == passed
• VERIFIES [[kinds.well_formed_row_passes]]

Scenario: kind_shape_naturality

• WHEN arbitrary_row_of_one_kind(), arbitrary_id_rename()
• THEN identity: assigned_kind(rename(row,a,a)) == assigned_kind(row) associativity: assigned_kind(rename(rename(row,a,b),b,c)) == assigned_kind(rename(row,a,c)) — renaming a row’s id never changes which of the five kinds it belongs to
• VERIFIES [[kinds.kind_shape_naturality]]

Scenario: kind_assignment_failure_label_asserted

• WHEN kind_assignment_failure_raised()
• THEN error_label == "kinds.kind_assignment_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[kinds.kind_assignment_failure_label_asserted]]

Scenario: shape_check_failure_label_asserted

• WHEN shape_check_failure_raised()
• THEN error_label == "kinds.shape_check_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[kinds.shape_check_failure_label_asserted]]

packs — domain-pack mechanism

id: packs kind: intent checked_against_core: clear statement: “WHEN a workspace enables a domain pack, THE format SHALL make the extension mechanism first-class — a kind: profile spec file whose six per-facet manifest tables declare exactly the sections, namespaced kinds, reference fields, checkers, floors, and requirements the pack introduces — and SHALL activate pack checking advisory-first by vocabulary use or a declared uses edge, never by config files, never by narrowing any base closed set, and never by changing how files without packs lint.”

Packs

Make specodelic’s extension mechanism first-class: a domain pack is a declared, discoverable, versioned artifact in the corpus itself — not a convention followed by hand. Base closed sets stop growing; vocabulary is pack-fiber-relative (the Grothendieck construction one level up, per [[theory]] precedent); independent packs coexist namespaced instead of colliding in the global kind sets.

Purpose

Make specodelic’s extension mechanism first-class: a domain pack is a declared, discoverable, versioned artifact in the corpus itself — not a convention followed by hand. Base closed sets stop growing; vocabulary is pack-fiber-relative (the Grothendieck construction one level up, per [[theory]] precedent); independent packs coexist namespaced instead of colliding in the global kind sets.

Constraints

Model

States

• draft
• published
• deprecated

Transitions

Properties

Notes

Fiber kinds in base-table kind columns (2026-10-03, beads specodelic-ung): mechanism v1’s closed-set walkers (property_kind_closed / constraint_kind_closed, openspec/specs/linter-schema_shape/spec.md) walked the static base sets, so a pack-declared fiber kind in a base-table kind column fired the finding even with its pack discovered — the sibling packs never hit this because their kinds live in pack-added sections. The walkers’ effective set is now base ∪ active-pack-fiber: the ## Kinds tokens of every pack active for the file (declared uses edge or vocabulary match — the same advisory-first activation rule as everything else here). This completes namespaced_vocabulary: a fiber kind is typeable in fiber scope, per-file. The base sets themselves do not grow (no format Revision; base pins stay valid) and a fiber kind with no active declaring pack stays outside the closed set — the labeled finding fires, never a silent pass. First consumer: empirical.registry’s empirical.statistic (the empirical-registry-pack capability spec’s fiber_kinds_typeable constraint and kind_column_accepts_fiber_kinds property).

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: manifest_round_trips

• WHEN pack_file_parsed_then_manifest_read()
• THEN declared entries equal parsed manifest rows — no drift, no prose leakage
• VERIFIES [[packs.manifest_round_trips]]

Scenario: discovery_finds_all_packs

• WHEN corpus_with_n_profile_files()
• THEN scan reports exactly n packs, order-independent
• VERIFIES [[packs.discovery_finds_all_packs]]

Scenario: subdir_lint_discovers_workspace_packs

• WHEN lint_subdirectory_with_pack_at_workspace_root()
• THEN pack discovered, its vocabulary checks run, zero orphan findings
• VERIFIES [[packs.subdir_lint_discovers_workspace_packs]]

Scenario: no_pack_no_change

• WHEN corpus_linted_before_and_after_mechanism()
• THEN lint findings byte-identical for a corpus using no pack vocabulary
• VERIFIES [[packs.no_pack_no_change]]

Scenario: overlapping_vocabulary_activates_both

• WHEN two_packs_declare_identical_vocabulary_and_a_file_uses_it()
• THEN both packs' checkers run; findings attributed per pack
• VERIFIES [[packs.overlapping_vocabulary_activates_both]]

Scenario: orphan_finding_names_pack

• WHEN corpus_using_vocabulary_without_pack()
• THEN failure finding names the candidate pack and both remediations, exit non-zero
• VERIFIES [[packs.orphan_finding_names_pack]]

Scenario: uses_edge_typing

• WHEN file_with_uses_edge_to_profile_id()
• THEN graph edge typed uses resolves to the profile id; wrong-kind targets violate typing
• VERIFIES [[packs.uses_edge_typing]]

Scenario: pack_self_activation_absent

• WHEN pack_file_linted_alone()
• THEN its checkers report an empty checked-set; no orphan findings from the pack's own manifest rows
• VERIFIES [[packs.pack_self_activation_absent]]

Scenario: skew_is_warning_not_failure

• WHEN pack_pinned_to_older_revision()
• THEN exit 0 with warning-channel advisory naming the pack's base pin and the corpus revision
• VERIFIES [[packs.skew_is_warning_not_failure]]

Scenario: empty_vocabulary_honest

• WHEN pack_enabled_without_instances()
• THEN checker reports empty checked-set; no fabricated findings
• VERIFIES [[packs.empty_vocabulary_honest]]

Scenario: narrowing_rejected

• WHEN pack_removing_previously_declared_kind()
• THEN pack_shape fails naming the removed entry and the append-only law
• VERIFIES [[packs.narrowing_rejected]]

Scenario: profile_file_is_four_layer

• WHEN pack_parsed_as_standard_spec()
• THEN all four layers parse from the pack file alone — no sidecar artifact needed
• VERIFIES [[packs.profile_file_is_four_layer]]

Scenario: pack_vocabulary_qualified

• WHEN two_packs_claim_same_mechanism()
• THEN both packs' declared vocabulary resolves without cross-pack collision
• VERIFIES [[packs.pack_vocabulary_qualified]]

Scenario: base_sets_unchanged_by_packs

• WHEN guide_sets_compared_across_pack_enable()
• THEN INTENT_KINDS and Reference Typing sets identical with and without packs discovered
• VERIFIES [[packs.base_sets_unchanged_by_packs]]

Scenario: lifecycle_states_parsed

• WHEN pack_model_section_parsed()
• THEN each lifecycle state yields exactly its declared checking behavior
• VERIFIES [[packs.lifecycle_states_parsed]]

Scenario: fiber_kinds_typeable

• WHEN base_table_kind_column_with_active_fiber_kind()
• THEN the base closed-set walkers accept the pack-qualified kind when the pack is active; the same token without the pack fires the labeled finding (base ∪ active-pack-fiber, never narrower)
• VERIFIES [[packs.fiber_kinds_typeable]]

Using packs

A domain pack is specodelic’s extension mechanism: a way to give a domain — data lineage, numeric predicates, bioimage metadata — its own typed sections, kinds, and reference fields without a format revision and without touching the core’s closed kind sets. This page is the practical guide: what a pack is, how a workspace enables one, what it adds, and the CLI loop you run against a pack-enabled spec. The machine truth lives in the packs spec; this page explains how to use the mechanism, not how it is specified.

Everything shown below is real output from specodelic 0.11.0 (on a TTY spk prints human-readable text; piped, it emits a JSON envelope).

What a pack is

A pack is a four-layer spec file with kind: profile in frontmatter — the same Intent → Constraints → Model → Properties shape as every other spec, plus six per-facet manifest tables:

## Sections, ## Kinds, ## References, ## Checkers, ## Floors, ## Requires

There is no separate artifact format and no sidecar manifest: the pack file is self-hosting, and linter.pack_shape checks the six tables’ row shapes at lint time in every lifecycle state. A malformed manifest is a labeled failure, never a silent pass.

In this repo the pack definitions live in packs/*.md (packs/data-lineage.md, packs/numeric-predicates.md, …). The frontmatter there is the source of truth for the pack inventory — CI derives the pack set from it (scripts/check_pack_doc_counts.py, the specodelic-typ0 gate) so doc pages that talk about “the standard packs” cannot drift from what actually ships. The in-repo packs are the five standard packs (data.lineage, numeric.predicates, empirical.registry, quant.finance, and svc.contracts — the last still draft) plus the bioimage.data D6 pilot (the first cross-pack ## Requires user). Each pack also has a capability spec in the rendered corpus — e.g. data-lineage-pack.

How a pack is enabled: corpus scan, not a config file

This is the part people coming from other tools trip on, so it is stated plainly: there is no packs.toml, no config file, no registry outside the corpus. Enablement is corpus-scan discovery:

• Every kind: profile file in the workspace is a candidate pack, found by scanning alone. Put a kind: profile file anywhere in the repo and it is a pack.
• The scan is anchored at the git repository toplevel of each linted directory (the lint target directory itself when no git root exists). Every linted path contributes its anchor, so discovery is order-independent: spk lint spec/a.md spec/b.md and spk lint spec/b.md spec/a.md discover the same pack set. Linting a subdirectory still discovers packs living anywhere in the workspace, because the anchor is the toplevel, not the subdirectory.
• The pack’s frontmatter id (e.g. data.lineage) is how everything else refers to it.

Activation is advisory-first and opt-in per file: a spec activates a discovered pack either by using its vocabulary (a word-boundary match; matching is longest-prefix) or by declaring a uses reference to the pack’s id on a Constraint row. A pack file is never a consumer of its own vocabulary — its manifest rows never trigger its checkers. Identical vocabulary declared by two discovered packs activates both, with findings attributed per pack.

What a pack adds

Once a pack is active for a file, the mechanism adds six things. All of them are namespaced: pack vocabulary is pack-qualified (data.dataset, not dataset), so two packs may independently claim a same-named concept and never collide — collision resolves by pack-qualified naming, not by error.

1. Namespaced sections. The pack’s ## Sections table declares typed extra sections with a fixed row shape. data.lineage declares a ## Data section whose rows are | name | kind | dtype | units | binding |.
2. Fiber kinds. Pack-declared kinds usable in the closed kind columns of base tables. The base closed sets never grow — the walkers accept a fiber kind only when its declaring pack is active for that file (base ∪ active-pack-fiber, never narrower); the same token without its pack is the labeled orphan_vocabulary finding below.
3. Reference fields. Set-valued typed references such as produced_by / consumed_by, resolving to declared rows of the same file (see the pack’s ## References table).
4. Pack-qualified checkers. Rules named inside the pack’s namespace, e.g. data.lineage.closure. Checkers ship as declarations — the mechanism interprets the declaration at activation and reports honestly.
5. Kind-dependent case-label floors. A pack’s ## Floors table can require named cases for law-kind properties of specific fiber kinds (e.g. data.artifact laws must carry a provenance: case).
6. A ## Requires pin. Each pack pins the base format revision it was written against; skew with the workspace corpus is advisory (below), never a failure.

Two hard guarantees round this off:

• Byte-identical guarantee. A spec that uses none of the pack vocabulary lints byte-identically to pre-mechanism behavior — no pack advisory, no new findings, nothing. With zero kind: profile files discovered, the machinery is inert.
• Append-only packs. A pack release may only add vocabulary; removing or narrowing a previously declared entry fails linter.pack_shape, naming the entry and the append-only law. The same law keeps base closed sets frozen — a pack can never narrow or retype an existing entry.

Lifecycle and honest-empty checkers

A pack is draft, published, or deprecated (declared through the pack’s own Model section). draft packs activate advisory-first with the draft status named in the finding; deprecated packs keep checking with the deprecation named. A checker with no workspace fixtures, data, or vocabulary instances reports an empty checked-set — honestly, with no fabricated discoveries. That is exactly what the activation advisories below show: empty checked-set (no violations to report).

The CLI loop

Set up a scratch workspace with a pack file and a consumer spec (here: data.lineage from the repo’s packs/ directory, and a lab-ETL spec):

mkdir demo && cd demo && git init
cp /path/to/specodelic/packs/data-lineage.md .

spk lint — discovery and activation

A consumer spec that declares a typed ## Data table using the pack’s vocabulary:

---
id: lab.etl
kind: intent
statement: "WHEN the lab runs its ETL pipeline THE system SHALL record every dataset the pipeline produces or consumes."
---

## Data

| name      | kind          | dtype | units | binding          |
|-----------|---------------|-------|-------|------------------|
| raw_reads | data.dataset  | fastq | reads | s3://lab/reads   |
| counts    | data.artifact | tsv   | count | parquet://counts |

| row       | produced_by | consumed_by |
|-----------|-------------|-------------|
| raw_reads |             | counts      |
| counts    | raw_reads   | qc_report   |

Lint it (the rest of the four-layer file is elided here):

spk lint lab-etl.md

lint: 1 file(s) linted, 0 finding(s), 1 advisory warning(s)
  advisory lab.etl [linter.observability] pack `data.lineage` activated for `lab.etl` (vocabulary match: data.dataset, data.artifact, Data, produced_by, consumed_by) — empty checked-set (no violations to report)
→ Run: specodelic graph

exit 0 — the pack was discovered by corpus scan (the git toplevel is the anchor) and activated by vocabulary match. The advisory is the activation note on the warnings channel: the pack’s declared rules ran and found nothing to report. No uses edge was needed.

The explicit route is a declared uses edge — a uses column on a Constraint row pointing at the pack’s frontmatter id:

| id | kind      | expr     | traces_to     | uses            |
|----|-----------|----------|---------------|-----------------|
| c1 | invariant | `plain`  | [[lab.etl]]   | [[data.lineage]] |

lint: 1 file(s) linted, 0 finding(s), 2 advisory warning(s)
  advisory lab.etl [linter.skew_advisory] pack `data.lineage` pins base Revision 14, workspace corpus is at Revision 18 — revision skew is advisory (never failing); consider updating the pack's `## Requires` base pin
  advisory lab.etl [linter.observability] pack `data.lineage` activated for `lab.etl` (declared uses edge) — declared rules: 6; empty checked-set (no violations to report)
→ Run: specodelic graph

The skew_advisory fires because this copy of the pack pins an older base revision than the corpus — a labeled advisory on the warnings channel, never a failure.

spk lint — what failure looks like

A declared uses edge naming a pack that is not discovered — say you lint the consumer file in a directory with no pack file in it — fails with labeled findings, never a silent pass (exit 1):

lint: 1 file(s) linted, 2 finding(s), 0 advisory warning(s)
  lab-etl.md [linter.total_refs] dangling reference `[[data.lineage]]` from constraints.uses — target not defined in any spec file
  lab.etl [linter.orphan_vocabulary] orphan vocabulary: `uses` edge targets `data.lineage`, but no `kind: profile` pack with that id is discovered — candidate pack `data.lineage`; remediations: add/enable a `kind: profile` pack file declaring it, or fix the vocabulary (remove or retype the `uses` edge)
→ Run: fix the reported invariants — each rule's semantics: spk explain lint-rules

The orphan_vocabulary finding always names the candidate pack — prefix-derived from the vocabulary token’s namespace when only the namespace is known (a data.* token with no data.lineage-like pack discovered names the data.* namespace) — and states both remediations: enable a pack declaring the vocabulary, or fix the vocabulary. Pack-qualified tokens in a base table’s kind column fire the same rule when their namespace has no discovered pack; the pack-added section’s own rows stay inert without the pack. A malformed pack manifest (wrong row shapes, a missing facet table, a non-pack-qualified kind) is a linter.pack_shape labeled failure on the pack file itself.

spk graph and spk compile — same loop, pack-aware

spk graph lab-etl.md

graph: 1 file(s), 5 node(s), 5 edge(s), 0 dangling, 0 typing violation(s), 0 supersedes cycle(s), 0 external boundary(ies)
→ Run: specodelic lint

spk compile lab-etl.md

compile: 1 compiled, 0 failed
  lab-etl.md [lab.etl] → specodelic/lab-etl.toml, specodelic/lab-etl_props.rs, specodelic/lab-etl.tla
→ Run: specodelic verify (consumes the *_props.rs artifacts)

The declared uses edge resolves corpus-wide: with the pack file in the linted corpus, both the dangling-reference finding and the orphan_vocabulary finding clear. It is an outbound leaf — it joins no reachability path and no acyclic edge set (mutual pack use is well-formed), and v1’s graph projection records no edge row for it: pack enablement is a lint-level fact. Compile and verify treat a pack-enabled spec like any other: pack vocabulary adds no compile-time artifacts, it extends what lint understands.

Where to go next

• The mechanism’s normative home: packs — domain-pack mechanism (every guarantee on this page is a constraint or property row there).
• The in-repo packs’ capability specs: data-lineage-pack, numeric-predicates-pack, empirical-registry-pack, bioimage-data-pack, quant-finance-pack, svc-contracts-pack.
• Writing a spec end-to-end (without packs): the worked example.
• Rule semantics offline: spk explain packs and spk explain lint-rules.

graph

id: graph kind: intent checked_against_core: clear statement: “THE graph tool SHALL derive, from every typed reference field in the repo, a single authoritative adjacency structure over 𝒦’s kinds, kept as a generated artifact that is never hand-edited, and SHALL answer transitive-closure (blast-radius) queries against it without re-walking markdown per query.”

Graph

Every checker in this repo (linter-referential_integrity.md, linter-graph_shape.md, rename.md) already walks the reference edges specodelic.md’s Reference Typing table defines — but each does it independently, on demand, by re-reading markdown. Nothing keeps a single standing structure of “what points at what” that a tool could query directly. This file specifies that structure: a derived artifact, not a hand-authored one, so merge.md’s conflict check and refactor.md’s fan-in signal can both query it instead of each re-deriving reachability their own way — the same “one stated fact, not several hand-maintained copies” discipline specodelic.md Revision 6 already applied to append_only_variants, here applied to the graph itself rather than a constraint.

Purpose

Every checker in this repo (linter-referential_integrity.md, linter-graph_shape.md, rename.md) already walks the reference edges specodelic.md’s Reference Typing table defines — but each does it independently, on demand, by re-reading markdown. Nothing keeps a single standing structure of “what points at what” that a tool could query directly. This file specifies that structure: a derived artifact, not a hand-authored one, so merge.md’s conflict check and refactor.md’s fan-in signal can both query it instead of each re-deriving reachability their own way — the same “one stated fact, not several hand-maintained copies” discipline specodelic.md Revision 6 already applied to append_only_variants, here applied to the graph itself rather than a constraint.

Constraints

| id | kind | expr | traces_to | satisfies | |———————————–|———–|——————————————————————————————————————————————————————|–––––––––––| | graph_is_derived_not_authored | invariant | every edge in the graph artifact is produced by extraction from repo files; the artifact contains no information a hand edit to it could add that isn't already present in some file's reference field | [[graph]] | | | total_extraction | invariant | ∀ reference field instance (traces_to/derives_from/guard/from/to/supersedes/emits/satisfies/observes) in any parsed file: exactly one corresponding edge exists in the graph — a guard’s conjunction of several [[id]] citations counts as one edge per citation, not one edge per transition; the enumeration restates the Reference Typing table’s field set (the authority — satisfies joined it in Revision 7) and links in non-reference columns (expr, predicate, frontmatter) are total_refs’ beat, never edges | [[graph]] | | | edge_kind_matches_typing | invariant | ∀ edge (source, field, target): (source.kind, field, target.kind) ∈ [[specodelic]]'s Reference Typing table — the graph never records an edge the typing table wouldn't allow, whether or not the underlying file is otherwise well-formed | [[graph]] | | | deterministic_derivation | invariant | re-deriving the graph from an unchanged repo produces a byte-identical artifact | [[graph]] | | | blast_radius_is_transitive_closure | invariant | blast_radius(id) == the forward and backward transitive closure of edges reachable from id, computed entirely within the derived artifact — never by re-walking source files | [[graph]] | | | stale_graph_detected | invariant | ∃ file whose on-disk content hash differs from the hash recorded at the artifact's last extraction ⟹ the artifact reports itself stale rather than silently serving an outdated query result | [[graph]] | | | external_boundary_derived | invariant | a file is classified as an external boundary iff it hosts ≥1 extension_point Constraint — the classification is a pure derivation over extracted structure, never an authored tag: removing the rows removes the classification, so a stale boundary tag cannot exist | [[graph]] | | | extraction_failure | effect | graph.extraction_failure(detail) | [[graph]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] |

Model

States

• unindexed
• extracting
• indexed
• queryable
• failed (emits: [[graph.extraction_failure]])

Transitions

Properties

Notes

checked_against_core: clear (see AGENTS.md’s convention). One resolved ambiguity worth recording anyway: total_extraction counts each [[id]] citation inside a conjunctive guard (A ∧ B ∧ C) as its own edge, not the whole guard as one edge — otherwise blast_radius would under-count what a transition actually depends on.

observes (specodelic.md Revision 9) joins total_extraction but no cycle set. An observation claim is not a dependency: the acyclic invariant’s edge set (linter-graph_shape.md) is a closed union that observes deliberately does not join — satisfies and emits are excluded by the same closure — so mutual cross-file observation is well-formed. The external-boundary classification is the same derived-not-authored discipline applied to visibility: a file is an external boundary because it published a contract, and the fact disappears when the publication does.

Scope boundary, Needs Human Review: this file does not replace linter-referential_integrity.md’s total_refs/unique_id or linter-graph_shape.md’s acyclic_traces/single_root_reachable — those checkers still own those constraints. What’s genuinely open is whether those two files should be refactored to query this artifact internally rather than independently re-deriving reachability, now that a shared artifact exists. That’s an efficiency and single-source-of-truth question, not a correctness gap, so it’s flagged rather than forced — changing either linter file’s internal mechanism without changing what it checks is exactly the kind of edit AGENTS.md’s workflow should route through a deliberate decision, not a side effect of adding this file.

Why extraction only requires parsed, not linted. Building the adjacency structure needs a reference field’s syntactic presence, not its resolution — a dangling [[typo_id]] still produces an edge (to a target that doesn’t yet exist), which is precisely the shape total_refs needs to check against. Requiring linted first would make the graph unable to represent the very files whose brokenness the existing checkers need to detect.

merge.md and refactor.md both depend on this file for blast-radius and fan-in queries respectively, rather than each re-deriving reachability — see each file’s own Constraints for how.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: every_edge_extracted

• WHEN arbitrary_spec_repo()
• THEN count(edges(graph)) == count(reference_field_instances(repo))
• VERIFIES [[graph.every_edge_extracted]]

Scenario: wrongly_typed_edge_rejected

• WHEN hand_inserted_edge(source_kind: State, field: "guard", target_kind: Property)
• THEN check(artifact) == rejected — guard targets an invariant Constraint or a State (specodelic.md Revision 12); a Property target is still rejected
• VERIFIES [[graph.wrongly_typed_edge_rejected]]

Scenario: rerun_deterministic

• WHEN run_extraction_twice_against_unchanged_repo()
• THEN artifact(run_1) == artifact(run_2)
• VERIFIES [[graph.rerun_deterministic]]

Scenario: blast_radius_transitive

• WHEN chain(a traces_to b, b derives_from c)
• THEN c ∈ blast_radius(a) — reachable through two hops, no direct edge required
• VERIFIES [[graph.blast_radius_transitive]]

Scenario: blast_radius_bidirectional

• WHEN edge(a → b)
• THEN a ∈ blast_radius(b) ∧ b ∈ blast_radius(a) — renaming a must be able to find dependent b, and vice versa
• VERIFIES [[graph.blast_radius_bidirectional]]

Scenario: stale_detected_on_edit

• WHEN edit_one_reference_field_without_re_extracting()
• THEN check(artifact) == stale
• VERIFIES [[graph.stale_detected_on_edit]]

Scenario: hand_authored_edge_rejected

• WHEN graph_artifact_with_a_manually_inserted_edge_absent_from_any_file()
• THEN check(artifact) == rejected
• VERIFIES [[graph.hand_authored_edge_rejected]]

Scenario: boundary_tracks_extension_points

• WHEN file_hosting_extension_point_row_then_all_removed()
• THEN classified(file) == true before, == false after removal — no authored residue
• VERIFIES [[graph.boundary_tracks_extension_points]]

Scenario: observes_edge_extracted

• WHEN constraint_row_carrying_observes_pointing_at_effect()
• THEN exactly one edge, kind constraints.observes — and zero edges when the column is absent
• VERIFIES [[graph.observes_edge_extracted]]

Scenario: extraction_failure_label_asserted

• WHEN extraction_failure_raised()
• THEN error_label == "graph.extraction_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[graph.extraction_failure_label_asserted]]

compile

id: compile kind: intent checked_against_core: clear statement: “THE Compile transition SHALL translate a linted-and-covered spec file’s Constraints table, Model section, and Properties table into a TOML document, a TLA+ module, and a set of proptest! blocks respectively, without dropping or altering any id.”

Compile

specodelic.md names compile as the transition from linted to compiled, gated on coverage and law_requires_cases, but never specifies what compiling actually produces (STATUS.md §4, P0). This file is that specification: Compile is the functor Set^𝒦 → TOML (constraints), Set^𝒦 → TLA+ (the model), and Set^𝒦 → proptest! (properties) that STATUS.md §1 describes — one functor with three target categories, not three unrelated tools that happen to run at the same pipeline stage.

Purpose

specodelic.md names compile as the transition from linted to compiled, gated on coverage and law_requires_cases, but never specifies what compiling actually produces (STATUS.md §4, P0). This file is that specification: Compile is the functor Set^𝒦 → TOML (constraints), Set^𝒦 → TLA+ (the model), and Set^𝒦 → proptest! (properties) that STATUS.md §1 describes — one functor with three target categories, not three unrelated tools that happen to run at the same pipeline stage.

Constraints

Model

States

• not_started
• extracting
• emitting
• compiled
• extract_failed (emits: [[compile.extraction_failure]])
• emit_failed (emits: [[compile.emission_failure]])

Transitions

Properties

Notes

This file is what makes specodelic.md’s rename_naturality law fully stated. That property’s naturality case reads compile(rename(I)) == rename(compile(I)) — until now that referenced a compile function with no specification of its own, so the claim was unfalsifiable in practice even though it was written down. With constraint_table_to_toml, model_to_tla, and properties_to_proptest now pinned down field-for-field, compile(·) in that law means something concrete: three specific, checkable translations, not an unnamed black box.

compile_is_total’s “never a silent partial result” is the reason extracting/emitting are split into two states rather than one: a failure during extraction (a malformed Constraint/Model/Property row) and a failure during emission (the three extracted representations don’t agree well enough to produce one coherent output — e.g. a Transition’s guard references a Constraint id that extraction resolved but the TOML and TLA+ passes disagree about its type) are different failure classes, and collapsing them into one failed transition would have been the same God-transition pattern specodelic.md Revision 2 already removed from lint.

Updated for specodelic.md Revision 6: model_to_tla now also compiles a State’s optional emits field into a small Output function alongside Next — the piece that turns a compiled automaton into a compiled Moore machine. This is additive to the existing translation, not a restructuring of it: a Model with no emits fields anywhere compiles exactly as before, Output is simply empty.

checked_against_core: clear (see AGENTS.md’s convention) — every constraint here traces to this file’s own intent rather than to a top-level invariant, the same shape linter-frontmatter.md through linter-coverage.md use for constraints scoped entirely to one feature.

The .tla module is a product of compile alone, not of any checker choice. model_check may run a native interpreter backend that never reads the module (see model_check.md’s Notes on backends), but the module is still emitted: it is the human-reviewable, engine-portable form of the compiled model, and TLC — the opt-in reference engine — consumes it directly. Correspondingly the corpus language no longer offers “or Alloy”: with a native default backend and a reference TLA+ engine it had no remaining role, and dropping it keeps model_to_tla a single, fully specified translation.

model_check and verify (STATUS.md §4, both now done — see model_check.md and verify.md) both consume this file’s output directly: model_check runs a model-check backend against the TLA+ module model_to_tla produces, and verify runs the proptest! blocks properties_to_proptest produces — each specified in its own checker file.

Executable predicate fragments (specodelic.md Revision 15, specodelic-rjb). Every predicate and expr cell may now opt into executable translation with a **rust:** marker — the cell text after the marker is a Rust boolean expression, emitted verbatim, no mini-language in between. This closes the gap the compile functor shipped with: a predicate was compiled to a todo_predicate! placeholder that compiles and panics at execution, so verify’s properties gate failed honestly but could never pass. The four rejection rows keep the marker honest: a fragment on a law row, a non-invariant Constraint, or a Transition guard is a labeled extraction failure, not a silently ignored marker (guards have no binding over the program-counter model — deferred of record). fragment_hygiene is the security/totality guard, deliberately defense-in-depth rather than a sandbox: fragments run on the invoking user’s machine with the invoking user’s privileges, the same trust every compiled artifact already had — the banned-token list catches the escape hatches a table cell should never legitimately need. The scaffolding’s element type is now String (the GenVal tuple-struct wrapper retired in the same Revision) so fragments bind plain generator values — the wrapper existed only to carry the placeholder story, and fragments make that story optional.

The closed language-tag grammar (specodelic.md Revision 16, specodelic-lf3). The opt-in marker’s tag is drawn from the closed set {rust, py, ts}; a marker is ** + a tag-shaped label + :** where the tag matches [a-z][a-z0-9_-]* — the lowercase-initial shape is what separates a marker from ordinary bold prose (**Note:** stays prose). Acceptance is grammar-level and emitter-independent: **py:** and **ts:** extract like **rust:**, but gate compile labeled (no_emitter_labeled_failure) until their emitters land, since an accepted tag without an emitter would silently fall through to Rust — the vacuous outcome the closed set exists to prevent. A tag-shaped marker outside the closed set fails labeled, naming the tag and the closed set (unknown_tag_rejected). The one grammar collision is resolved by row kind: a law-kind predicate’s **label:** occurrences are the law-case grammar (Revision 13), never fragment markers, so the fragment grammar exempts law rows; every other fragment-position occurrence is checked.

Two binding layers, one per tool, never merged (decision of record 2026-10-04, specodelic-lf3 — corrected review finding CORR-001, design openspec/changes/add-language-neutral-property-binding D3): the artifact’s // id: / // case: metadata comments and contract-TOML flags are not two spellings of one neutral ABI. The comments key per-block verdicts inside a specodelic artifact — properties_to_proptest emits them, properties_to_proptest’s own metadata comments key them, and nothing outside this file’s emission consumes them. Contract-TOML flags bind existing tests — pytest node ids, shell escape hatches — to scenarios, which is espectacular’s layer and stays there. Ownership: compile.md owns fragment extraction and artifact emission (the closed-tag grammar above); espectacular owns contract binding of existing tests (its [runners] config, already shipped — no parallel registry is built here, CORR-002); specodelic.md owns the format grammar (Revision 16’s closed set). Nothing in this file consumes or produces espectacular contract binding — merging the layers would couple scaffold execution policy to contract-binding policy with different wall-clock, caching, and toolchain stories.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: precondition_violation_rejected

• WHEN file_that_has_not_passed_lint()
• THEN check(file) == failed
• VERIFIES [[compile.precondition_violation_rejected]]

Scenario: toml_roundtrips

• WHEN arbitrary_constraint_row()
• THEN parse_toml(compile(row)) == row
• VERIFIES [[compile.toml_roundtrips]]

Scenario: tla_disjunct_count_matches

• WHEN arbitrary_model_section(n_transitions)
• THEN count(disjuncts(compile(model).Next)) == n_transitions + 1 — the closing stuttering disjunct
• VERIFIES [[compile.tla_disjunct_count_matches]]

Scenario: output_function_covers_emitting_states_only

• WHEN arbitrary_model_section(n_states_with_emits, n_states_without)
• THEN domain(compile(model).Output) == the_states_with_emits — no entry for the rest
• VERIFIES [[compile.output_function_covers_emitting_states_only]]

Scenario: proptest_block_per_property

• WHEN arbitrary_property_row()
• THEN count(compile(row).blocks) ≥ 1
• VERIFIES [[compile.proptest_block_per_property]]

Scenario: law_property_compiles_required_cases

• WHEN law_property_row_with(cases: ["identity", "associativity"])
• THEN count(compile(row).blocks) == 2
• VERIFIES [[compile.law_property_compiles_required_cases]]

Scenario: compile_completes_or_fails_cleanly

• WHEN arbitrary_linted_and_covered_file()
• THEN compile(file) ∈ {all_three_artifacts, single_labeled_failure} — never partial
• VERIFIES [[compile.compile_completes_or_fails_cleanly]]

Scenario: id_preservation_holds

• WHEN arbitrary_linted_and_covered_file()
• THEN ids_in(file) ⊆ ids_in(compile(file))
• VERIFIES [[compile.id_preservation_holds]]

Scenario: roundtrip_stable

• WHEN arbitrary_linted_and_covered_file()
• THEN compile(file) == compile(parse(compile(file)))
• VERIFIES [[compile.roundtrip_stable]]

Scenario: extraction_failure_label_asserted

• WHEN extraction_stage_fails_on_row()
• THEN error_label == "compile.extraction_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[compile.extraction_failure_label_asserted]]

Scenario: emission_failure_label_asserted

• WHEN emission_stage_fails()
• THEN error_label == "compile.emission_failure" — same three-site rename rule (EDGE-002)
• VERIFIES [[compile.emission_failure_label_asserted]]

Scenario: fragment_body_emitted_verbatim

• WHEN property_row_with_rust_fragment()
• THEN the emitted block body contains the fragment verbatim
• VERIFIES [[compile.fragment_body_emitted_verbatim]]

Scenario: prose_predicate_stays_placeholder

• WHEN property_row_without_fragment()
• THEN compile(row).body contains todo_predicate! — no widening of pre-Revision behavior
• VERIFIES [[compile.prose_predicate_stays_placeholder]]

Scenario: fragment_values_bind_generators

• WHEN property_row_with_two_generators()
• THEN the emitted block's args are v0, v1 — one per named generator, each a String
• VERIFIES [[compile.fragment_values_bind_generators]]

Scenario: rust_fragment_semantics_unchanged

• WHEN revision_15_rust_fragment_cell()
• THEN extract(cell) == revision_15_extract(cell) — byte-identical, pure widening
• VERIFIES [[compile.rust_fragment_semantics_unchanged]]

Scenario: unknown_tag_labeled

• WHEN property_row_with_marker_tag("**go:")
• THEN error_stage == fragment_extraction ∧ message names the tag and the closed set
• VERIFIES [[compile.unknown_tag_labeled]]

Scenario: non_fragment_tag_is_mention

• WHEN property_row_with_mid_span_marker_tag("**py:")
• THEN compile(row) == compile(row_without_marker) — mid-span occurrence never extracts
• VERIFIES [[compile.non_fragment_tag_is_mention]]

Scenario: one_tag_extracts_per_cell

• WHEN property_row_with_marker_tag("**py:")
• THEN extract(cell) == Some(fragment_under("py")) — a fragment-position cell extracts under exactly one tag from the closed set {rust, py, ts}; acceptance is grammar-level and emitter-independent
• VERIFIES [[compile.one_tag_extracts_per_cell]]

Scenario: missing_emitter_labeled

• WHEN property_row_with_marker_tag("**py:")
• THEN error_label == "compile.emission_failure" ∧ the remediation hint names the per-language emitter follow-up — never a silent fall-through to Rust emission
• VERIFIES [[compile.missing_emitter_labeled]]

Scenario: law_fragment_labeled

• WHEN law_row_with_fragment()
• THEN error_stage == fragment_extraction
• VERIFIES [[compile.law_fragment_labeled]]

Scenario: hygiene_violation_labeled

• WHEN fragment_with(banned_token: "std::fs")
• THEN error_stage == fragment_extraction ∧ message names the token
• VERIFIES [[compile.hygiene_violation_labeled]]

Scenario: guard_fragment_labeled

• WHEN transition_row_with_fragment_guard()
• THEN error_stage == fragment_extraction
• VERIFIES [[compile.guard_fragment_labeled]]

Scenario: non_invariant_fragment_labeled

• WHEN effect_row_with_fragment()
• THEN error_stage == fragment_extraction
• VERIFIES [[compile.non_invariant_fragment_labeled]]

Scenario: kernel_expr_extracts

• WHEN invariant_cell_with_kernel_marker()
• THEN the expression extracts under the closed grammar and evaluates to exactly one of verified, counterexample, unknown
• VERIFIES [[compile.kernel_expr_extracts]]

Scenario: kernel_nonmember_labeled

• WHEN invariant_cell_with_nonmember_atomic()
• THEN error_stage == kernel_grammar ∧ the message names the offending atomic and the closed set
• VERIFIES [[compile.kernel_nonmember_labeled]]

Scenario: binding_text_surfaces_verbatim

• WHEN constraint_row_with_arbitrary_binding_text()
• THEN the compiled TOML carries the binding cell text verbatim — no interpretation, no validation of its internals
• VERIFIES [[compile.binding_text_surfaces_verbatim]]

Scenario: claim_path_is_flags

• WHEN external_checker_claiming_a_constraint()
• THEN the claim is carried by contract-TOML flags binding; the toolchain builds no registry
• VERIFIES [[compile.claim_path_is_flags]]

model_check

id: model_check kind: intent checked_against_core: clear statement: “THE model_check step SHALL run a model-check backend — stateright (embedded, default) or TLC (opt-in) — against the model compile.md’s model_to_tla produces, and SHALL report either that no counterexample was found within a stated bound, or a minimal counterexample trace naming the violated invariant.”

Model check

specodelic.md names model_check as the compiled → model_checked transition, guarded only by model_present — a structural check that a Model section exists. Whether the model actually holds (no_counterexample) is a separate invariant, consumed later by the verify transition’s guard, not by model_check itself. That split was never made explicit anywhere (STATUS.md §4, P0): this file specifies the run model_check names — what “invoking the checker” actually does to the module compile.md produces, and what a stated result must contain.

Purpose

specodelic.md names model_check as the compiled → model_checked transition, guarded only by model_present — a structural check that a Model section exists. Whether the model actually holds (no_counterexample) is a separate invariant, consumed later by the verify transition’s guard, not by model_check itself. That split was never made explicit anywhere (STATUS.md §4, P0): this file specifies the run model_check names — what “invoking the checker” actually does to the module compile.md produces, and what a stated result must contain.

Constraints

Model

States

• not_run
• running
• clean
• counterexample_found
• timed_out
• exploration_only

Transitions

Properties

Notes

This clarifies a naming trap in specodelic.md’s lifecycle, flagged as CLAR-003 (same shape as CLAR-001, CLAR-002 — not resolved here for the same reason: renaming a live state name should go through rename_naturality, not be done by hand). model_checked sounds like it means “the model was checked and holds,” but its guard, [[specodelic.model_present]], only confirms a Model section exists — checker_invoked above is what “a run actually happened” means, and whether that run found a counterexample (no_counterexample) is a fact consumed only by the next transition, verify. A file can be in state model_checked while its most recent run found a counterexample, or before any run has happened at all if model_present alone were treated as sufficient. no_counterexample_feeds_verify and rerun_on_model_change above are what close that gap: no one may claim no_counterexample without having actually run this state machine to clean, and a clean result older than the last Model edit doesn’t count.

timed_out is a real terminal outcome, not a failure this file papers over as “counterexample” or “clean” by default: an unbounded or very large state space may exhaust its budget before exhaustive_within_bound is satisfied either way. So is exploration_only (specodelic-len): the native stateright backend interprets guards as prose (Decision 3, Option A) and executes zero invariant predicates, so its completed runs terminate in finish_exploration, NOT finish_clean — a completed exploration proves the space ends within the bound and nothing more. no_counterexample is reserved for a backend that actually executed invariant predicates and found no violation; consumers (verify’s gate, the no_counterexample_feeds_verify property above) must treat exploration_only exactly like timed_out — not-clean, though not evidence of a violation either. Backends. The contract above is engine-neutral, and any backend satisfying it sits behind the same state machine. Two are specified: stateright (default) — an embedded Rust model-checking crate, no external dependencies: its breadth-first exploration makes counterexample_is_minimal hold by construction (the first counterexample found is the shortest), target_max_depth/timeout/target_state_count give exhaustive_within_bound’s stated bound and timed_out’s budget-exhausted outcome directly, and its named properties give counterexample_names_violated_invariant when each property is named after the Constraint id it derives from. The native backend interprets the compiled model (states as values, transitions as actions) rather than generating Rust source. TLC (opt-in) — the mature JVM reference engine, run as a subprocess against the .tla module compile.md emits, with -depth as the stated bound. Alloy was dropped from the corpus language alongside this change: with a native default and a reference TLA+ engine it had no remaining role, and a SAT-based engine returns an instance, not a minimal trace — which would fight counterexample_is_minimal rather than satisfy it. verify’s downstream guard treats timed_out the same as counterexample_found for the purpose of no_counterexample (both are not-clean), but they are reported differently, since a timeout is not evidence of a violation — just of an inconclusive run.

checked_against_core: clear (see AGENTS.md’s convention) — no_counterexample and model_present already existed there and are referenced, not restated. verify (STATUS.md §4, now done — see verify.md) consumes this file’s clean/counterexample_found outcome alongside compile.md’s proptest! blocks.

Executable invariants (specodelic.md Revision 15, specodelic-rjb). Decision 3’s Option C ships: the **rust:** fragment (see compile.md) turns a kind == invariant Constraint into something the native backend actually executes — as a scratch-crate run, because a Rust expression cannot be evaluated in-process from source text. The scratch runner is a dependency-free breadth-first search over the same program-counter model the embedded interpreter walks, which keeps counterexample_is_minimal holding by construction (BFS discovers the shortest violating path) and keeps the bound semantics honest: a completed exploration with ≥ 1 executed invariant and no violation is no_counterexample; zero executed invariants stays exploration_only; a budget cap is timed_out. A panicking fragment is a violation at the state where it panicked (invariant_totality — a predicate that explodes is not a predicate that holds). The engine attribution of the scratch run is native-bfs with the tool’s own version — it is not stateright, and backend_identified requires the report not to imply otherwise. TLC cannot execute Rust fragments at all: against the same artifact it still reports exploration_only, which is the honesty this file already pinned for prose predicates.

The module’s staleness key now covers fragments: model_to_tla emits the executable-invariant manifest (id + fragment verbatim) as module comments, so editing a fragment changes the artifact hash and rerun_on_model_change (reworded above to name fragments explicitly) fails the stale report closed — an invariant that changed since the clean run is not the invariant the run checked.

Claim-gated aggregation (define-verification-claim-gates). claim_aggregate_governs refines what a clean run means without redefining any state: a refuted required claim is a real counterexample_found (named, via the existing minimal-trace machinery), an exhausted bound is still timed_out, and an incomplete required set — unknown, unsupported, missing, or empty — lands in exploration_only, joining the zero-predicates case the Notes above already pinned. The priority order matters and is normative: refutation outranks exhaustion outranks incompleteness, so a passing Rust claim can never launder a false kernel or citation claim into no_counterexample. claim_report_schema gives the verdict an evidence carrier: a versioned report whose scope_sha256 digest binds the parsed structured content and consumed artifacts — not filesystem paths — so reordering CLI inputs or editing prose alone reuses a report, while genuinely different invariant content never does. corpus_identity_scope (named dual_format_isolated_scope before Revision 18) is the corpus-identity side of the same policy: the intent ids of a command’s parsed inputs must be unique. Before Revision 18 this was two rules — the identity law plus a separate isolated-scope refusal for id: spec files — but id: spec itself retired in Revision 18 (specodelic-mcy): dual-format files now carry real ids and the identity law is the only scope law left, strictly stronger than the old pair (a same-id delta/deployed pair is now refused outright, where the old law’s per-file exemption let them coexist).

Revision-discipline note. These rows deliberately do NOT touch specodelic.md (this file’s scope-law revision rode specodelic.md Revision 18 without touching no_counterexample’s expr there): “the selected model-check backend finds no violated invariant”, and this file — already the owner of that row’s precise meaning via no_counterexample_feeds_verify — narrows the reachable clean leg instead of restating it in the core (the AGENTS.md rule 3a preference for widening an existing constraint’s scope over restating it). verify.md carries the acceptance-side twins: the claim gate on verified, scope-bound evidence, and view parity. All three implementations share one aggregation path (design D4 of openspec/changes/define-verification-claim-gates), so model-check, verify, and orchestrate cannot drift apart on these rules.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: stale_claim_rejected

• WHEN compiled_module_with_zero_runs_against_it()
• THEN no_counterexample(file) == undetermined — never defaults to true
• VERIFIES [[model_check.stale_claim_rejected]]

Scenario: bound_must_be_stated

• WHEN run_report_with_no_stated_bound()
• THEN check(report) == invalid
• VERIFIES [[model_check.bound_must_be_stated]]

Scenario: shortest_counterexample_reported

• WHEN model_with(two_violating_traces_of_different_length: true)
• THEN reported_trace(check(model)) == the_shorter_of_the_two
• VERIFIES [[model_check.shortest_counterexample_reported]]

Scenario: violated_invariant_named

• WHEN model_with_exactly_one_violated_invariant()
• THEN check(model).violated_invariant_id == the_expected_id
• VERIFIES [[model_check.violated_invariant_named]]

Scenario: backend_named_in_report

• WHEN run_report_from_any_backend()
• THEN check(report).backend == a named engine and version
• VERIFIES [[model_check.backend_named_in_report]]

Scenario: clean_run_satisfies_verify_gate

• WHEN arbitrary_model_with_no_violation_within_bound()
• THEN no_counterexample(file) == true
• VERIFIES [[model_check.clean_run_satisfies_verify_gate]]

Scenario: stale_result_invalidated_by_edit

• WHEN (clean_run, model_edited_afterward_with_no_rerun)
• THEN no_counterexample(file) == false — until re-run
• VERIFIES [[model_check.stale_result_invalidated_by_edit]]

Scenario: clean_model_passes

• WHEN arbitrary_model_with_no_violation_within_bound()
• THEN check(model) == clean
• VERIFIES [[model_check.clean_model_passes]]

Scenario: exploration_run_is_not_a_clean_verdict

• WHEN model_with_only_prose_invariants_exhausted_within_bound()
• THEN check(model).outcome == exploration_only — never read as no_counterexample
• VERIFIES [[model_check.exploration_run_is_not_a_clean_verdict]]

Scenario: fragment_invariants_checked

• WHEN compiled_model_with_one_executable_invariant()
• THEN check(model).invariants_checked == [the_invariant_id]
• VERIFIES [[model_check.fragment_invariants_checked]]

Scenario: fragment_clean_run_is_no_counterexample

• WHEN model_with_executable_invariants_no_violation()
• THEN check(model).outcome == no_counterexample — the model gate’s reachable leg
• VERIFIES [[model_check.fragment_clean_run_is_no_counterexample]]

Scenario: panicking_fragment_violates

• WHEN model_with_panicking_invariant_fragment()
• THEN check(model).outcome == counterexample_found ∧ violated_invariant_id == the_panicking_id
• VERIFIES [[model_check.panicking_fragment_violates]]

Scenario: fragment_violation_traces

• WHEN model_with_falsifiable_executable_invariant()
• THEN check(model).trace == the_reachable_state_path — the trace leg is the existing constraint’s, not a new one
• VERIFIES [[model_check.fragment_violation_traces]]

Scenario: false_claim_is_counterexample_found

• WHEN model_with(passing_rust_claim, counterexample_kernel_claim)
• THEN check(model) == counterexample_found naming the false claim id — a passing Rust claim never hides it
• VERIFIES [[model_check.false_claim_is_counterexample_found]]

Scenario: unknown_or_missing_claim_blocks_clean

• WHEN model_with(unknown_or_missing_required_claim)
• THEN check(model) == exploration_only with reasons naming the claim ids
• VERIFIES [[model_check.unknown_or_missing_claim_blocks_clean]]

Scenario: exhausted_bound_stays_timed_out

• WHEN model_with(all_verified_claims_but_exhausted_bound)
• THEN check(model) == timed_out — verified claims cannot outrank an incomplete exploration
• VERIFIES [[model_check.exhausted_bound_stays_timed_out]]

Scenario: prose_only_is_unchecked_not_required

• WHEN model_with_only_prose_invariants()
• THEN required_claims(model) == [] ∧ unchecked_claims(model) == those ids — never implied verified
• VERIFIES [[model_check.prose_only_is_unchecked_not_required]]

Scenario: report_binds_claims_and_scope_digest

• WHEN run_report_from_current_inputs()
• THEN report.claim_schema_version == 1 ∧ expected/unchecked ids present ∧ scope_sha256 present
• VERIFIES [[model_check.report_binds_claims_and_scope_digest]]

Scenario: reordered_paths_and_prose_preserve_scope

• WHEN same_structured_inputs_in_different_cli_order()
• THEN scope_sha256 unchanged — the digest binds content, not paths
• VERIFIES [[model_check.reordered_paths_and_prose_preserve_scope]]

Scenario: swapped_reports_rejected_unrewritten

• WHEN two_files_same_claim_names_opposite_invariants()
• THEN digest(a) ≠ digest(b) ∧ each run rejects the other's report without rewriting it
• VERIFIES [[model_check.swapped_reports_rejected_unrewritten]]

Scenario: combined_same_identity_scope_refused

• WHEN two_parsed_files_claiming_the_same_intent_id()
• THEN check(invocation) == duplicate_corpus_identity before any artifact or report write (Revision 18)
• VERIFIES [[model_check.combined_same_identity_scope_refused]]

Scenario: distinct_ids_compose_and_lint_together

• WHEN several_dual_format_files_with_distinct_ids_linted_and_checked_together()
• THEN check(lint) == valid — files with distinct real ids compose like any corpus (Revision 18)
• VERIFIES [[model_check.distinct_ids_compose_and_lint_together]]

verify

id: verify kind: intent checked_against_core: clear statement: “THE verify step SHALL run every proptest! block compile.md’s properties_to_proptest produced to completion, and SHALL transition a file to verified only when all of them pass and model_check.md’s most recent run against the current compiled artifact reported clean.”

Verify

specodelic.md names verify as the model_checked → verified transition, guarded by no_counterexample ∧ properties_pass — but neither what “running the properties” means nor how that conjunction is actually enforced was ever specified (STATUS.md §4, P0, last of the three pipeline items). This file closes it: verify is what actually executes compile.md’s output and combines it with model_check.md’s outcome into the one fact specodelic.md’s lifecycle calls verified.

Purpose

specodelic.md names verify as the model_checked → verified transition, guarded by no_counterexample ∧ properties_pass — but neither what “running the properties” means nor how that conjunction is actually enforced was ever specified (STATUS.md §4, P0, last of the three pipeline items). This file closes it: verify is what actually executes compile.md’s output and combines it with model_check.md’s outcome into the one fact specodelic.md’s lifecycle calls verified.

Constraints

| id | kind | expr | traces_to | satisfies | |————————————|———–|——————————————————————————————————————————————————|–––––––––––| | blocks_run_to_completion | invariant | verify actually executes every proptest! block compile.md produced against the current compiled artifact — properties_pass is never satisfied by a partial run or a cached prior result | [[verify]] | | | properties_pass_reflects_latest_run | invariant | [[specodelic.properties_pass]] holds iff every block from the most recent run against the current compiled artifact passed; a run predating the last edit to Properties, Constraints, or Model does not count | [[verify]] | | | failure_reports_shrunk_counterexample | invariant | when a proptest! block fails, the report gives the shrunk (minimal) failing input, not the first randomly-generated failing input encountered | [[verify]] | | | both_gates_required | invariant | verify only transitions a file to verified when both [[specodelic.no_counterexample]] (model_check.md's clean outcome) and [[specodelic.properties_pass]] hold — passing properties alone, or a clean model alone, is insufficient | [[verify]] | | | law_cases_unexecuted | invariant | for a law-kind property compiled into multiple blocks (one per required case), all compiled blocks must pass — a partial pass (identity passes, associativity fails) is a failure of the property, not a partial success | [[verify]] | | | verify_is_idempotent | invariant | re-running verify against an unchanged compiled artifact yields the same pass/fail outcome as the prior run, even though proptest may resample inputs each run for coverage | [[verify]] | | | bounded_wall_clock | invariant | the verify runner bounds its cargo test run on a wall-clock clock (default 600s, –timeout-secs 0 disables the bound); a run exceeding the bound is killed and reported as a labeled timeout — never a silent hang, and never indistinguishable from a block failure | [[verify]] | | | verification_failure | effect | verify.verification_failure(detail) | [[verify]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | required_claims_govern_acceptance | invariant | verify only transitions a file to verified when every required claim (model_check.md's required_claims_classified set) is verified in the current report AND every generated property block passes — a passing property run alone never covers an unknown, missing, or refuted claim; invalid or duplicate claim records are rejected as malformed evidence, never inferred as unknown success, and prose-only invariants stay unchecked | [[verify]] | | | evidence_scope_bound | invariant | verify recomputes the scope digest and the required claim set from the current inputs and compares them against the stored report: old or unrecognized claim-schema versions, absent scope fingerprints, omitted or duplicate records, changed contributing inputs, or artifact mismatch fail with a rerun hint naming the model-check command — a stored report is never rewritten to manufacture evidence, and the digest binds structured content, not filesystem paths, so swapped reports from different scopes never verify | [[verify]] | | | assurance_views_agree | invariant | CLI JSON, human output, and the persisted report agree on evaluated, unchecked, and blocking claims — no view reports verified while another names a blocker — and release documentation distinguishes structural lint, bounded model exploration, verified declared claims, and external application-test binding without advertising pending capabilities as implemented | [[verify]] | |

Model

States

• not_run
• running
• properties_evaluated
• verified
• failed (emits: [[verify.verification_failure]])

Transitions

Properties

Notes

This closes STATUS.md §4’s P0. The three pipeline items — compile.md, model_check.md, and this file — now cover the full linted → compiled → model_checked → verified lifecycle specodelic.md names but had never specified past the data-shape level. STATUS.md §1 describes “something you can simulate before writing code” as one of the four things a spec file gives you; compile.md is what makes the simulation buildable, model_check.md is what makes running it meaningful, and this file is what makes trusting its result well-defined rather than an unstated conjunction of two booleans.

both_gates_required is the one constraint doing the most work here: it restates specodelic.md’s bare no_counterexample ∧ properties_pass guard, but as an actual mechanism — single_gate_insufficient’s test case (properties pass, model doesn’t) is exactly the failure mode a project would hit if someone treated a green proptest run alone as sufficient to ship, skipping the model checker.

law_cases_unexecuted is a deliberate echo of specodelic.md’s law_requires_cases (which gates compiling a law-kind property on it having ≥ 2 cases in the first place). That constraint ensures the cases exist before compilation; this one ensures they’re all actually run and passing before verification — the same discipline applied at two different pipeline stages, on either side of compile.md.

checked_against_core: clear (see AGENTS.md’s convention). With this file, STATUS.md §4’s P0 is fully done; P1 (the rename/refactor tool) is next.

Executable fragments make verified reachable (specodelic.md Revision 15, specodelic-rjb). Before that Revision the verdict’s verified status was unreachable by construction — every compiled block carried a todo_predicate! placeholder that panics at execution, and the native backend executed zero invariant predicates, so both gates failed honestly on every file. fragments_reach_verified pins the way out without touching both_gates_required or any honesty rule: a predicate opting in with **rust:** executes for real, an executable invariant gives the model run a predicate to actually check, and verified becomes the conjunction both gates always demanded — reachable, never redefined. Files whose cells carry no fragment behave exactly as before.

Claim-gated acceptance and scope-bound evidence (define-verification-claim-gates). required_claims_govern_acceptance completes both_gates_required rather than replacing it: the two gates already demanded — a clean model run and passing properties — are now joined by the third input they were silently missing, the per-claim statuses the model report carries. A refuted or unknown kernel/citation claim blocks verified even with a green proptest run; prose-only invariants stay explicitly unchecked, and having a deriving Property never makes one executable. evidence_scope_bound is what makes the first constraint trustworthy: verify recomputes scope and the required set from the current inputs instead of trusting the stored report’s word, so a stale, swapped, or malformed report fails with a rerun hint — old evidence is rejected, never silently re-scored or rewritten. This is deliberately stricter than the pre-change acceptance path; the rerun instruction ships with the release. assurance_views_agree keeps the three report surfaces (CLI JSON, human output, the persisted <stem>.check.json) from telling different stories about the same run.

The claim-side machine itself (required/unchecked classification, the aggregate priority, the report schema, and dual-format command isolation) is specified once, in model_check.md — this file consumes it, mirroring how it already consumes model_check’s clean outcome rather than restating specodelic.md’s bare guard. No specodelic.md Constraint is touched, so no Revision bump: the acceptance conjunction lives here (see the Revision-discipline note there).

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: partial_run_rejected

• WHEN run_that_skips_one_compiled_block()
• THEN check(run) == invalid
• VERIFIES [[verify.partial_run_rejected]]

Scenario: cached_result_rejected

• WHEN (passing_run, properties_edited_afterward_with_no_rerun)
• THEN properties_pass(file) == false — until re-run
• VERIFIES [[verify.cached_result_rejected]]

Scenario: shrunk_counterexample_reported

• WHEN block_with(large_random_failing_input: true, smaller_reachable_by_shrinking: true)
• THEN reported_input(check(block)) == the_smaller_one
• VERIFIES [[verify.shrunk_counterexample_reported]]

Scenario: single_gate_insufficient

• WHEN file_with(properties_pass: true, no_counterexample: false)
• THEN check(file) == failed
• VERIFIES [[verify.single_gate_insufficient]]

Scenario: both_gates_clean_passes

• WHEN file_with(properties_pass: true, no_counterexample: true)
• THEN check(file) == verified
• VERIFIES [[verify.both_gates_clean_passes]]

Scenario: partial_law_case_rejected

• WHEN law_property_with(identity_case: "pass", associativity_case: "fail")
• THEN check(property) == failed
• VERIFIES [[verify.partial_law_case_rejected]]

Scenario: rerun_matches_prior_outcome

• WHEN (run_1, run_2) on an unchanged compiled artifact
• THEN outcome(run_1) == outcome(run_2)
• VERIFIES [[verify.rerun_matches_prior_outcome]]

Scenario: verification_failure_label_asserted

• WHEN verification_failure_raised()
• THEN error_label == "verify.verification_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[verify.verification_failure_label_asserted]]

Scenario: hang_reported_as_labeled_timeout

• WHEN runner_with(predicate_that_never_terminates, timeout: 1)
• THEN check(run) == timeout_labeled ∧ outcome(run) ≠ failed — a timeout is no verdict on the property: distinct from properties_failed so a legitimately long suite can be re-run with a raised bound instead of misread as a failing predicate
• VERIFIES [[verify.hang_reported_as_labeled_timeout]]

Scenario: fragments_reach_verified

• WHEN fixture_with(fragment_predicate_passing, executable_invariant_clean)
• THEN check(file) == verified — with executable fragments (specodelic.md Revision 15) both gates are reachable: a passing executable predicate and a clean executable-invariant run verify a real file, the state the gate could never reach before this Revision
• VERIFIES [[verify.fragments_reach_verified]]

Scenario: claim_complete_evidence_verifies

• WHEN fixture_with(all_required_claims_verified, properties_pass)
• THEN check(file) == verified with the exact required and unchecked sets
• VERIFIES [[verify.claim_complete_evidence_verifies]]

Scenario: false_claim_blocks_verified

• WHEN file_with(properties_pass: true, counterexample_kernel_claim)
• THEN check(file) == failed naming the false claim id — properties never cover a refuted claim
• VERIFIES [[verify.false_claim_blocks_verified]]

Scenario: malformed_records_rejected

• WHEN report_with(missing_or_duplicate_claim_record)
• THEN check(file) == failed with a rerun hint — never inferred as unknown success
• VERIFIES [[verify.malformed_records_rejected]]

Scenario: stale_report_rejected_with_rerun_hint

• WHEN (clean_report, structurally_edited_inputs_afterward)
• THEN check(file) == failed naming the rerun command — the report is never rewritten
• VERIFIES [[verify.stale_report_rejected_with_rerun_hint]]

Scenario: swapped_scope_report_rejected

• WHEN report_from_a_different_structured_scope()
• THEN check(file) == failed — the digest binds structured content, not paths
• VERIFIES [[verify.swapped_scope_report_rejected]]

Scenario: views_agree_on_blockers

• WHEN run_with(required_unknown_claim_and_prose_invariant)
• THEN json.blockers == human.blockers == report.blockers ∧ unchecked sets agree
• VERIFIES [[verify.views_agree_on_blockers]]

Scenario: release_docs_match_implemented_capabilities

• WHEN docs_built_for_a_release()
• THEN version derives from Cargo metadata ∧ pending capabilities not advertised as implemented
• VERIFIES [[verify.release_docs_match_implemented_capabilities]]

rename

id: rename kind: intent checked_against_core: clear statement: “WHEN a user requests renaming a spec row’s id, THE rename tool SHALL update the defining row and every referencing [[link]] as a single atomic operation, or leave the repo unchanged.”

Rename Tool

rename_naturality is asserted as a property in three other files (specodelic.md, linter-referential_integrity.md, linter-graph_shape.md’s topo_sort_naturality), but the tool those properties are about has never had its own Intent, Constraints, Model, or Properties (STATUS.md §4, P0). This file is that spec: what a rename request actually does, step by step, and what must hold before it’s allowed to report success.

A rename is the concrete operation whose existence makes η : I ⇒ I' (STATUS.md §1’s natural transformation between two instances of 𝒦) more than a formal description — it’s the thing that has to actually construct I' from I and a single (old_id, new_id) pair, honoring naturality rather than merely being checked against it after the fact.

Purpose

rename_naturality is asserted as a property in three other files (specodelic.md, linter-referential_integrity.md, linter-graph_shape.md’s topo_sort_naturality), but the tool those properties are about has never had its own Intent, Constraints, Model, or Properties (STATUS.md §4, P0). This file is that spec: what a rename request actually does, step by step, and what must hold before it’s allowed to report success. A rename is the concrete operation whose existence makes η : I ⇒ I' (STATUS.md §1’s natural transformation between two instances of 𝒦) more than a formal description — it’s the thing that has to actually construct I' from I and a single (old_id, new_id) pair, honoring naturality rather than merely being checked against it after the fact.

Constraints

| id | kind | expr | traces_to | satisfies | |––––––––––––––|———–|–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––|–––––––––––| | new_id_available | invariant | new_id ∉ index(repo) — renaming never collides with an existing id | [[rename]] | | | new_id_matches_filename | invariant | if the renamed row is a file's own Intent, [[specodelic.id_matches_file]] must hold between new_id and the (possibly also renamed) filename | [[rename]] | | | old_id_fully_replaced | invariant | ∀ [[old_id]] reference anywhere in repo: rewritten to [[new_id]]; zero occurrences of old_id remain post-rename | [[rename]] | | | atomic_operation | invariant | the definition-row update, every reference rewrite, and any required filename change apply as one transaction: all succeed, or the repo is left byte-identical to its pre-rename state | [[rename]] | | | kind_unchanged | invariant | assigned_kind(row) is the same before and after rename — both 𝒦's five-object kind and, where present, the row's own kind/sub-kind column — see [[kinds.kind_shape_naturality]] | [[rename]] | | | prose_untouched_by_rename | invariant | rename rewrites only [[id]] wiki-link syntax and structured id fields (frontmatter id, table id/traces_to/derives_from/guard/from/to cells) — it never edits rationale/description prose, even if the prose happens to mention the old name in words | [[rename]] | | | validation_failure | effect | rename.validation_failure(new_id, reason) | [[rename]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | apply_failure | effect | rename.apply_failure(detail) | [[rename]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | post_check_failure | effect | rename.post_check_failure(detail) | [[rename]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] |

Model

States

• requested
• checked
• applying
• applied
• verifying
• passed
• validate_failed (emits: [[rename.validation_failure]])
• apply_failed (emits: [[rename.apply_failure]])
• check_failed (emits: [[rename.post_check_failure]])

Transitions

Properties

Notes

checked_against_core: clear (see AGENTS.md’s convention). The properties this file needs (atomicity, prose-non-interference, kind-preservation) are local to what a rename operation must guarantee, the same way compile.md, model_check.md, and verify.md each carry constraints specific to their own step of the lifecycle without requiring new entries in specodelic.md itself — this file’s Intent is the fourth instance of that pattern, not an exception to it.

rename_naturality now exists in four places (specodelic.md, linter-referential_integrity.md, linter-graph_shape.md’s topo_sort_naturality, and here). That’s intentional, not duplication to clean up: each site states the same law at the altitude that site owns — specodelic.md as the format’s top-level refactor-safety guarantee, the two linter files as “this is exactly the check that would catch a naive rename tool,” and this file as the actual operation those laws are about. This file is the one whose apply/apply_ok/apply_fail transitions give the law something to be a law of, rather than a fact asserted with no corresponding process.

Why verify re-runs two checkers instead of all six. apply_ok already establishes old_id_fully_replaced (no dangling old-id refs) and kind_unchanged directly as this file’s own constraints. What apply_ok can’t see on its own is whether the rewrite altered anything at the repo-graph level it wasn’t watching for — a same-file collision the local check missed, or a graph edge that only becomes visible once every file’s refs are re-indexed together. linter.referential_integrity and linter.graph_shape are exactly the two checkers whose owned constraints (unique_across_repo, ref_resolves, acyclic, single_root_reachable) depend on cross-file state a single-rename’s local bookkeeping can’t fully self-certify. The other four checkers (model_shape, ears_syntax, schema_shape, coverage) check properties a rename can’t perturb — it never changes a transition’s guard-presence, a statement’s EARS pattern, a table’s column shape, or whether a constraint has a deriving property — so re-running them would be redundant Needs Human Review overhead, not signal.

Decision of record (2026-09-30, user-approved; advised by a typed Jev evaluation, jev-1.13.0, conf 0.74): a batch rename is one atomic transaction, not n independent ones. All files touched by the batch are staged and validated as a set — the same precondition-then-apply-then-reverify shape a single rename already uses — and any validation failure aborts the whole batch, leaving every file byte-identical to before. Partial success is exactly the failure mode the single-rename atomic_operation constraint exists to prevent: a half-renamed namespace is a corpus where ref_resolves dangles by design, and the whole-commit atomicity git already provides makes per-file partial commits a policy choice a tool shouldn’t silently make. atomic_operation therefore means the same thing at batch scope as at single-rename scope: all-or-nothing. A batch-rename implementation is a separate follow-up ticket; nothing in this file’s constraint text changes.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: rename_naturality

• WHEN arbitrary_spec_repo(), arbitrary_id_rename()
• THEN identity: rename(I, a, a) == I associativity: rename(rename(I,a,b), b,c) == rename(I,a,c) naturality: compile(rename(I)) == rename(compile(I))
• VERIFIES [[rename.rename_naturality]]

Scenario: collision_rejected

• WHEN (repo_with_id: "x", new_id: "x_taken_by_other_row")
• THEN check(request) == failed
• VERIFIES [[rename.collision_rejected]]

Scenario: filename_mismatch_rejected

• WHEN rename_of_a_files_own_intent_id_without_a_matching_filename_change()
• THEN check(request) == failed
• VERIFIES [[rename.filename_mismatch_rejected]]

Scenario: partial_failure_rolls_back

• WHEN apply_interrupted_after_definition_row_updated_but_before_all_refs_rewritten()
• THEN post_state(repo) == pre_state(repo)
• VERIFIES [[rename.partial_failure_rolls_back]]

Scenario: stray_ref_caught_by_verify

• WHEN rename_that_misses_one_[[old_id]]_occurrence()
• THEN check(request) == failed — caught at verify, not silently accepted
• VERIFIES [[rename.stray_ref_caught_by_verify]]

Scenario: prose_mention_left_alone

• WHEN row_whose_rationale_prose_contains_the_old_id_as_a_word()
• THEN rationale_text(post_rename_row) == rationale_text(pre_rename_row)
• VERIFIES [[rename.prose_mention_left_alone]]

Scenario: clean_rename_passes

• WHEN well_formed_repo(), id_not_used_elsewhere()
• THEN check(request) == passed
• VERIFIES [[rename.clean_rename_passes]]

Scenario: kind_preserved_by_rename

• WHEN rename_of_a_constraint_row_to_a_new_id()
• THEN assigned_kind(post_rename_row) == assigned_kind(pre_rename_row) — both the five-object kind and, where present, the row’s own kind column survive the rewrite
• VERIFIES [[rename.kind_preserved_by_rename]]

Scenario: validation_failure_label_asserted

• WHEN validation_failure_raised()
• THEN error_label == "rename.validation_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[rename.validation_failure_label_asserted]]

Scenario: apply_failure_label_asserted

• WHEN apply_failure_raised()
• THEN error_label == "rename.apply_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[rename.apply_failure_label_asserted]]

Scenario: post_check_failure_label_asserted

• WHEN post_check_failure_raised()
• THEN error_label == "rename.post_check_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[rename.post_check_failure_label_asserted]]

merge

id: merge kind: intent checked_against_core: clear statement: “WHEN two branches derived from a common ancestor spec repo are joined, THE merge tool SHALL detect id collisions and reference breaks introduced by the union of their edits — using [[graph]]’s blast-radius query rather than re-deriving reachability independently — before reporting the merge complete, and SHALL never report success against a tree that [[linter.referential_integrity]] or [[linter.graph_shape]] would reject.”

Merge

A textually clean 3-way merge (no conflict markers) can still produce a semantically broken repo: two branches mint the same new id independently, or one branch renames an id (rename.md) while the other adds a fresh reference to the old name in a file the rename never touched. Git’s line-based merge can’t see either problem — both are clean at the text layer. This file specifies the check that runs after git’s merge succeeds: it reuses graph.md’s derived reachability rather than re-deriving it, and rename.md’s actual rewrite mechanism rather than inventing a second one, applied across two histories instead of one linear line — the “existing mechanism, new scope” move AGENTS.md #3a asks for before adding anything new.

Purpose

A textually clean 3-way merge (no conflict markers) can still produce a semantically broken repo: two branches mint the same new id independently, or one branch renames an id (rename.md) while the other adds a fresh reference to the old name in a file the rename never touched. Git’s line-based merge can’t see either problem — both are clean at the text layer. This file specifies the check that runs after git’s merge succeeds: it reuses graph.md’s derived reachability rather than re-deriving it, and rename.md’s actual rewrite mechanism rather than inventing a second one, applied across two histories instead of one linear line — the “existing mechanism, new scope” move AGENTS.md #3a asks for before adding anything new.

Constraints

| id | kind | expr | traces_to | satisfies | |——————————————|———–|––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––|–––––––––––| | graph_reused_not_rederived | invariant | merge's collision and blast-radius checks query [[graph]]'s artifact for both branch tips; merge never independently re-walks markdown for reachability | [[merge]] | | | no_new_id_collision | invariant | ∀ id ∈ index(branch_A) ∩ index(branch_B): id was already defined, identically, in the common ancestor — an id newly minted by both branches independently is a collision, not a merge | [[merge]] | | | blast_radii_recorded_pre_merge | invariant | before applying the union of edits, merge records [[graph]].blast_radius(touched_ids) for each branch separately, against the common ancestor's graph | [[merge]] | | | semantic_conflict_iff_blast_radius_intersects | invariant | blast_radius_A(touched_A) ∩ blast_radius_B(touched_B) ≠ ∅ ⟹ the merge requires human review, even when the two branches' literal file diffs don't overlap | [[merge]] | | | rename_replayed_onto_foreign_edits | invariant | if branch A contains a [[rename]] application of (old_id, new_id) and branch B independently adds a new [[old_id]] reference within blast_radius_A, the merge rewrites that reference to [[new_id]] using rename.md's own rewrite mechanism — it is never left dangling and never silently dropped | [[merge]] | | | post_merge_relint_required | invariant | merge is not reported passed until [[linter.referential_integrity]] and [[linter.graph_shape]] are re-run against the merged tree and both report passed | [[merge]] | | | sequential_number_reassigned_on_conflict | invariant | if both branches independently claim the same next sequential number (a CHANGELOG entry or Revision heading), the merge tool renumbers one of the two rather than allowing a silent duplicate | [[merge]] | | | collision_failure | effect | merge.collision_failure(detail) | [[merge]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | reverification_failure | effect | merge.reverification_failure(detail) | [[merge]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | merge_aborted | effect | merge.merge_aborted(detail) | [[merge]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] |

Model

States

• diverged
• collision_checked
• needs_review
• rename_replayed
• ref_integrity_reverified
• merged
• collision_failed (emits: [[merge.collision_failure]])
• reverification_failed (emits: [[merge.reverification_failure]])
• merge_failed (emits: [[merge.merge_aborted]])

Transitions

Properties

Notes

checked_against_core: clear (see AGENTS.md’s convention). rename_replayed_onto_foreign_edits was checked against AGENTS.md #3a specifically before being added as a new row rather than reusing rename.md’s old_id_fully_replaced as-is: it isn’t a duplicate, because it operates over two divergent histories being joined, not one linear history — old_id_fully_replaced guarantees completeness within a single rename’s own transaction, and says nothing about a reference minted on a different branch that the rename operation never saw. This file’s constraint is what makes that reference get rewritten anyway, once the branches meet.

What this file doesn’t replace. Two edits to the same row’s own field on both branches is an ordinary textual conflict — git already marks it, already forces a human to resolve it, and nothing here changes that. This file exists only for the cases where the text merge is clean but the result isn’t: id collisions and rename/reference splits that don’t overlap a single line.

Depends on graph.md, not a local reachability walk. Every blast-radius computation in this file’s Constraints is a graph query, computed once against the common ancestor for each branch (blast_radii_recorded_pre_merge) rather than recomputed after the union is applied — recomputing post-union would already have mixed the two branches’ edges together and lost the ability to tell which branch’s change reached which id.

Depends on rename.md, not a second rewrite mechanism. resolved/ auto_proceed’s rewrite step calls the same rewrite rename.md’s apply transition performs — this file only decides when a cross-branch replay is required, never how the rewrite itself works.

Decision of record (2026-09-30, user-approved; HITL ticket specodelic-mp1 row 2): “a human has explicitly approved” means an explicit, attributable, recorded human decision by the operator — a deliberate approve step (never inferred, timed-out into, or defaulted) whose decision lands in the repo’s decision trail (change notes / ticket). No CI gate or role requirement is assumed: the format describes tool contracts, not hosting policy, and an implementation may layer a gate or role on top, but the floor the resolved guard checks is the attributable operator decision itself. CI gates and roles were deliberately excluded — both presume infrastructure the spec cannot see, whereas a recorded operator decision is checkable by the merge lifecycle itself. This paragraph records the decision; constraint text is unchanged, same treatment as rename.md’s batch-rename decision.

Resolved question (was Needs Human Review): what “a human has explicitly approved” (the resolved transition’s guard) means operationally is now decided — see the decision of record above. The mechanism-agnostic floor stands: an attributable operator decision, recorded in the repo’s decision trail; gates and roles are layers an implementation may add, not assumptions the format makes.

Open question, relationship to refactor.md: a blast-radius intersection that triggers needs_review here may also be exactly the “unrelated fan-in” shape refactor.md flags as a tidy-first candidate — both files answer different questions (can this merge proceed safely, vs. should this node be split before more changes land on it) and are deliberately left as two files rather than merged into one, but a same-session finding from both on the same node is worth surfacing together rather than as two unrelated notices. Left open rather than wired automatically.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: collision_across_branches_rejected

• WHEN two_branches_each_independently_defining_new_id("x")
• THEN check(merge) == failed
• VERIFIES [[merge.collision_across_branches_rejected]]

Scenario: inherited_id_not_falsely_flagged

• WHEN id_defined_in_common_ancestor_unchanged_in_both_branches()
• THEN check(merge) != failed
• VERIFIES [[merge.inherited_id_not_falsely_flagged]]

Scenario: textually_clean_semantic_conflict_flagged

• WHEN branch_A(renames x to y), branch_B(adds a new [[x]] reference in a file branch_A never touched)
• THEN check(merge) == needs_review
• VERIFIES [[merge.textually_clean_semantic_conflict_flagged]]

Scenario: rename_replay_repairs_dangling_ref

• WHEN same scenario, after human approval
• THEN post_merge_repo has zero occurrences of [[x]]; branch_B's new reference now reads [[y]]
• VERIFIES [[merge.rename_replay_repairs_dangling_ref]]

Scenario: disjoint_blast_radii_auto_merge

• WHEN two_branches_touching_disjoint_namespaces_with_disjoint_blast_radii()
• THEN check(merge) == merged — no human review required
• VERIFIES [[merge.disjoint_blast_radii_auto_merge]]

Scenario: duplicate_sequential_number_renumbered

• WHEN both_branches_add_a_CHANGELOG_entry_claiming_the_same_next_number()
• THEN post_merge_repo has two distinct sequential numbers; neither is duplicated
• VERIFIES [[merge.duplicate_sequential_number_renumbered]]

Scenario: relint_gates_merge

• WHEN merge_where(linter.referential_integrity or linter.graph_shape: fails against the merged tree)
• THEN check(merge) == failed — mirrors rename.md’s stray_ref_caught_by_verify
• VERIFIES [[merge.relint_gates_merge]]

Scenario: blast_radius_recorded_before_apply

• WHEN merge_history_where_edits_were_applied_before_both_branches'_radii_were_recorded()
• THEN check(merge) == failed — apply never precedes the recording step, for either branch
• VERIFIES [[merge.blast_radius_recorded_before_apply]]

Scenario: reachability_from_graph_artifact_only

• WHEN merge_invoked_with_the_markdown_walker_patched_to_panic()
• THEN merge of an otherwise-clean diverged repo succeeds — collision and blast-radius checks only query [[graph]]’s artifact
• VERIFIES [[merge.reachability_from_graph_artifact_only]]

Scenario: collision_failure_label_asserted

• WHEN collision_failure_raised()
• THEN error_label == "merge.collision_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[merge.collision_failure_label_asserted]]

Scenario: reverification_failure_label_asserted

• WHEN reverification_failure_raised()
• THEN error_label == "merge.reverification_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[merge.reverification_failure_label_asserted]]

Scenario: merge_aborted_label_asserted

• WHEN merge_aborted_raised()
• THEN error_label == "merge.merge_aborted" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[merge.merge_aborted_label_asserted]]

refactor

id: refactor kind: intent checked_against_core: clear statement: “WHEN a proposed changeset would edit rows owned by a node with high, unrelated fan-in in [[graph]], THE refactor advisor SHALL surface a non-gating suggestion to split that node first, and SHALL never block or delay any transition in [[specodelic]]’s or [[orchestrate]]’s lifecycle.”

Refactor Advisor

STATUS.md §2 already names the pathology this mechanizes — “God object / cyclic dependency” — and specodelic.md Revision 2 already fixed one real instance of it by hand (splitting the flat 7-clause lint guard into the Checker Ownership table) before anyone had a tool that would have flagged it proactively. This file is that tool’s spec: Kent Beck’s tidy-first rule (“separate the structural change from the behavioral one”) read as a graph query — a node with fan-in from unrelated namespaces, or a changeset that only needs a fraction of what a node owns, is a candidate for splitting before the behavioral edit lands, not after.

Purpose

STATUS.md §2 already names the pathology this mechanizes — “God object / cyclic dependency” — and specodelic.md Revision 2 already fixed one real instance of it by hand (splitting the flat 7-clause lint guard into the Checker Ownership table) before anyone had a tool that would have flagged it proactively. This file is that tool’s spec: Kent Beck’s tidy-first rule (“separate the structural change from the behavioral one”) read as a graph query — a node with fan-in from unrelated namespaces, or a changeset that only needs a fraction of what a node owns, is a candidate for splitting before the behavioral edit lands, not after.

Constraints

Model

States

• idle
• analyzing
• clean
• found emits: [[refactor.advisory_finding_emitted]]

Transitions

Properties

Notes

checked_against_core: clear (see AGENTS.md’s convention). Nothing new was needed to make the finding non-gating: advisory_finding_emitted is kind == effect, and [[specodelic.ref_kind_compatible]]’s own typing already restricts every transition’s guard field to kind == invariant Constraints only, tested generically by [[specodelic.advisory_cannot_gate]]. An effect-kind Constraint is excluded from guard-eligibility by that same rule, for the same reason an advisory-kind one is — so this file needed no invariant of its own asserting “the finding can’t gate anything”; that was already true, globally, before this file existed. (An earlier draft of this file carried two such invariants plus a redundant unit test — removed as an instance of the exact “one rule, restated three ways” pattern specodelic.md Revision 6 already caught once, for append_only_variants.) advisory_finding_emitted’s emits reuses the Moore-machine mechanism Revision 6 built for State; this file adds no sixth 𝒦 object and no new kind of Constraint — a new consumer of an existing mechanism, not a new one.

This file never decides how to split a node. It only detects the fan-in/narrow-diff shape and emits a finding; the actual split — a new file, an updated traces_to, an updated Checker Ownership-style table if the node is itself a dependency hub — is an ordinary edit, checked the normal way by the six existing linters. Deciding how to split is a design judgment this file deliberately doesn’t automate.

Depends on graph.md, not on re-deriving reachability: analyze’s guard cites graph’s own queryable state by typed citation ([[graph.queryable]] — a State, which Revision 10’s guard typing admits) instead of bare prose (the same “cite another file’s state fact when it isn’t itself a Constraint row” pattern orchestrate.md already uses for model_check.md/verify.md), and every fan-in count is a graph.blast_radius query, never an independent markdown walk.

Decision of record (2026-09-30, user-approved; advised by a typed Jev evaluation, jev-1.13.0, conf 0.54): “unrelated fan-in” keys off the id namespace — the “shares no namespace segment below root” test stands as written. Physical directory placement is rejected as the keying: ids are the format’s primary identity (id_matches_file ties them to filenames, the Reference Typing table types them as foreign keys), so relatedness judged by namespace is consistent with how every other checker reads the corpus, while directory placement would make the advisory’s meaning depend on filesystem layout the format doesn’t own. The flat-namespace failure mode is real but contained: the finding is kind == advisory-shaped (non-gating by typing), and the threshold is already per-repo configurable — a flat-namespace repo raises the threshold or lives with noise. A configurable keying mode (namespace or directory) stays a possible future widening under kind_field_extensible-style governance if a real flat-namespace corpus ever adopts the format; nothing in this file’s constraint text changes.

Open question, Needs Human Review: threshold_is_per_repo_setting deliberately leaves the actual number unset here — this file specifies that the threshold is configurable, not what a reasonable default is.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: fan_in_graph_sourced

• WHEN node_with_precomputed_blast_radius_in_graph()
• THEN advisor_source_calls(markdown_walker) == 0 — every count comes from graph’s artifact
• VERIFIES [[refactor.fan_in_graph_sourced]]

Scenario: unrelated_fan_in_flagged

• WHEN node_referenced_by_dependents_in_three_disjoint_top_level_namespaces()
• THEN check(node) == found
• VERIFIES [[refactor.unrelated_fan_in_flagged]]

Scenario: related_fan_in_not_flagged

• WHEN node_referenced_only_by_dependents_within_its_own_namespace_subtree()
• THEN check(node) == clean
• VERIFIES [[refactor.related_fan_in_not_flagged]]