v6.2.0 — a named rule is not an instruction to reject (n8n field study)

Fifth field target: n8n's execution-status classification — no defect in n8n. But the pure-reject trap reproduced 5/5 after the 6.1.0 prompt-wording fix, and the study isolated the real trigger: generations reject every branch that maps to a named specialRules entry — because the template and renderer literally commanded it ("REQUIRED reject(reason) cases") for every rule, including rules naming behavioral branches. Full finding: eval/FINDING-n8n-reject-no-write.md.

Changes

• Corpus-classified special rules. renderSpecialRulesAsRejections(contract, windows) classifies each rule by what the code actually does on its matching windows: all no-op → [REJECTION — must reject]; all change → [BEHAVIORAL — must perform the transition, MUST NOT reject; the name is only the why]; mixed → two-armed instructions split by pre-state, or the per-branch observable-change test when the arms overlap (one absolute would manufacture the inverse trap — caught by adversarial review on the repo's own eval corpus). whenState idioms (key == 'value', any) normalize before matching; name-only rules render as documentation; canonical (stable) equality throughout. polygen's no-corpus authoring path keeps the must-reject reading.
• Auto-regeneration. When the first generation pass hits the reject-as-annotation signature uniformly (every live spec rejected ≥2 windows the code acted on), verify regenerates once with the offending (pre-state, action) windows called out — the correction addendum takes precedence over the base prompt — and reports the second pass with both spec sets kept (specs/, specs_regen/). findings.md flags the contract-question tension (if the contract deliberately declared those windows no-ops, the first pass was the signal); --no-auto-regen opts out. Tested end-to-end via a generation seam, no live API in tests.
• Template/skill: the Special-rules section teaches the observable-change decision test; the skill's contract step and Step-5 triage updated to match.

🤖 Generated with Claude Code

v6.1.0 — the field-study release: no defects in raft/xstate/hatchet, seven traps fixed in the tool

Four field studies (hashicorp/raft role + commitment machines, xstate's transition-resolution engine, hatchet's workflow-status rollup) found no defects in any target — and every multi-spec failure traced to a structural gap in what the tool told the generations, never model comprehension. This release fixes all of them, each milestone adversarially reviewed.

Since v5.0.0

sam-pattern 2.2.0 vendored (includes the 6.0.0 move to 2.1.2 prime semantics, previously unreleased). Both upstream issues drafted from the field studies shipped in the library and are adopted here:

• Union types (sam-lib #35): renderModelShape emits real union declarations ({ type: ['string','object'] }) for keys detected as unions from trace evidence, init, or pure-type-token notes — the xstate trap (5/5 generations mistyped state.value) is closed with shape checking intact.
• Reject-after-write hard-fail (sam-lib #36): the hatchet trap (5/5 generations annotated success with reject(reason), silently discarding correct work) now throws SamFrameError at step time; verify keeps a trace-signature fallback (rejectedActedWindows, projection-basis) and findings.md surfaces per-window spec runtime errors.

verify enhancements (plan M1–M7, docs/verify-enhancements-plan.md):

• M1 — frozen-state-key warning: a key no action changes leaves Part 2 structurally blind behind it (raft's startIndex — a deleted safety gate still model-checked clean); now warned per spec, with --initial-states plumbed through verify as the remedy.
• M2 — runaway-exploration guardrails: drift detection flags likely-unbounded keys (raft's term bump) within seconds instead of a silent 15-minute grind, with a progress heartbeat; completed explorations loudly retract mid-run suspicion.
• M3 — spec-vs-spec agreement: pairwise agreement, named outliers, and a per-finding split column (4-vs-1 (minority: …)) — with the report stressing the majority is NOT automatically right (in the raft study the lone dissenter was correct).
• M4 — scripted negative control (scripts/mutate.mjs): one command replaces hand-edited controls — polynv's four mutation operators applied to the reference and replayed with pipeline-parity scoring; zero flipped windows on a distinguishable mutation = a corpus blind spot, exit 1.
• M5 — skill guidance: real-traces prerequisite (no captured traces → wrong tool), capture-by-subscription-not-polling (the raft Candidate miss), and reading guides for every new report signal.
• findings.md gains: frozen-key and drift warnings, the agreement/consensus line, the reject-as-annotation triage hint, and a distinct spec-runtime-errors section.

Field-study reports: eval/FINDING-raft-field-study.md, eval/FINDING-xstate-union-schema.md, eval/FINDING-hatchet-reject-annotation.md.

🤖 Generated with Claude Code

v5.0.0 — the fleet study, the Tier 3 replication, and an external benchmark run

polyvers gains an evidence base. The compatibility mechanism was previously argued for; it is now measured — in a pre-registered three-tier fleet study — and replicated against an external benchmark task.

Corpus provenance is decisive

Four incompatible changes, run against corpora differing only in where the states came from:

corpus	caught
archived (real provenance)	4/4
synthesized (BFS-reachable states of the old machine)	3/4

The one that escapes is the landmine: a state the old version could reach, that production therefore holds, and that the new version forbids. A synthesized corpus cannot contain it, because it contains only states the old model says are reachable. Same tool, same change, same gates — the verdict turns on provenance alone. No false positives on either tier.

The composition cases separate the two levels of the cross-machine check: a narrowed cancel window passes the pairwise matrix and fails the joint product.

A machine can be internally consistent and still unsafe to deploy

A dunning-budget narrowing explores 19 states clean from init() and fails seeded from the fleet, which holds a subscription at exactly the depth the new budget makes terminal. Affected population: one snapshot — stated, because class of defect and blast radius are different claims.

Real releases do not announce themselves

Two Medusa version pairs, replayed under a freeze protocol (the old-version model committed before the new version's diff is read):

pair	one-line summary	outcome
v2.4.0 → v2.5.0	"enum gains members"	FAIL — 6 of 32 states stranded
v2.17.1 → v2.17.2	"enum gains a member"	PASS — 0 stranded

Interchangeable summaries, opposite behaviour. The first changed a status derivation; the second changed nothing but a domain. A team classifying either from its release notes would have been wrong in both directions. The first finding is corroborated by the maintainers' own PR text, which names that inconsistency class as deferred work.

Conformance and exploration fail in different directions

An external replication on SysMoBench's etcd Raft task — real traces from a real 3-node cluster, via the tracing hook upstream in etcd-io/raft:

	replay	explorer + invariants
8 injected defects	2/8	1/8 definitive, 6/8 inconclusive
5 one-shot generated specs	4/5	0/5

Replay misses defensive code a correct system never drives — including the heartbeat clamp this project's own prior work singles out. The explorer misses anything the stated invariants omit. Neither subsumes the other, and a specification graded by either alone gets a clean bill it has not earned.

⚠️ Commit f6743a7's title reports "the explorer catches 8/8". That figure is wrong — it was a regex matching the word "violations" inside no invariant violations reachable, and was corrected in 59345b6. The table above is authoritative.

What it reports against itself

• A projection-bound miss. A zero-amount payment collection reads unpaid under one version and completed under the next; the declared money abstraction collapses at zero, so the case is inexpressible. Out-of-projection, with the bound declared before the analysis.
• A self-inflicted false positive. Rewording type-description prose manufactured a shape diff — operator error, reported rather than quietly fixed.
• Two measurement bugs, both caught by control rows deliberately scored on identical terms.
• A corrected claim in the paper. Finite action domains do not imply a finite state space: exhaustiveness requires a finite reachable state space, which a contract is not currently required to declare.

Also in this release

Two polyvers defects the study found and fixed: the migrate gate conflating structural with invariant failures, and the semantic gate understating its own coverage. Plus polyrun simulate, the joint product check, engine READMEs rewritten as introductions, and the SDLC diagrams.

Bounded results are not passes — enforced in code throughout, not assumed.

3.0.0 — polyvers: the fourth engine

New engine: polyvers — versioning for state machines with mechanical compatibility gates. Polygraph audits, polygen authors, polyrun executes, polyvers evolves: two verification gates now sit between authoring and execution — the first version of a machine takes the correctness path (Polygraph), every later version takes the compatibility path (polyvers) — and execution feeds both gates back.

Given two versions of a machine's artifact family and fleet snapshots:

• polyvers classify fires the compatibility lanes the change touches (shape / vocabulary / intent / semantic / migration / composition); each lane names exactly the gates it demands.
• polyvers check runs them: setState round-trip; cross-version stimuli replay (everything the old version can still deliver — timers, completions, old-vocabulary callers — must land as accepted or a named observable reject, kernel-parity classification); migration validation (migrate scaffold generates migrate.cjs from the shape diff; the gate checks purity, acceptance, projection equality, state and transition invariants, then swaps the corpus so every downstream gate runs over post-migration states); and the headline — an exhaustive model check seeded from live fleet snapshots: can any state the fleet actually holds be driven to an invariant violation under the new rules? The landmine hunt, mechanized — with a fixture proving only the seeded check catches it.
• polyvers matrix checks parent×child rollout-window pairings over the spawn/completion protocol and its delivery.

Deterministic, byte-identical compat-reports a PR can be gated on; refusals instead of vacuous passes (empty corpus, missing invariants, BOUNDED exploration without --allow-bounded); no API key anywhere. Plugin surfaces: /polygraph:polyvers command, skill, and subagent.

Worked example: examples/polyvers-oms versions the OMS order machine — a shape+rules+intent change, the scaffolded migration, and the committed compat-report and matrix report. Docs: the four-engine architecture with an updated interactive diagram set, the SDLC's Phase 7 mechanized, and a literature-context section in the versioning essay (docs/VERSIONING.md).

Every milestone (M0–M3) shipped with an adversarial multi-agent review; all confirmed findings fixed. 62 polyvers tests, plus the full pipeline/polyrun suites, all green.

Breaking notes: scripts/check.mjs gained initialStates, and its result shape changed (statesExplored counts discovered states only; seededStates reported separately). The polyvers artifact-dir convention reserves migrate.cjs/effects.cjs as sibling artifacts a machine module may not be named after.

🤖 Generated with Claude Code

https://claude.ai/code/session_01NpdSdufYcKnkvzhB56NkVn

Polygraph 2.1.0 — polyrun, the OMS trilogy, and the pipeline gates

The headline: a new component and two capstone examples that take Temporal's OMS reference application full circle — reimplemented on verified machines, then audited in its original Go form.

polyrun — durable execution for verified machines

A durable-execution harness for polygen-authored SAM v2 strict-profile machines (spec: docs/polyrun-spec.md, code: polyrun/):

• Snapshot-based durability — no event-sourced replay, no determinism sandbox, no patch() versioning; deploys are gated mechanically over live snapshots (polyrun deploy), including a model check using production states as initial states
• One-transaction dispatch with actionId dedupe; transactional outbox with idempotency keys, leases, retries, DLQ + onExhausted; durable timers whose staleness resolves as verified reject(reason)
• SQLite and Postgres adapters (the full suite runs against both), standalone worker, HTTP facade + read-only ops console
• First-class parent/child machines (spawn/signal/completion/cancel-on-parent-terminal) and post-commit journal fan-out — and the journal is a Polygraph trace corpus (polyrun audit replays production against the model, version-aware)
• polyrun check-effects: exhaustive exploration of the machine ∘ effect-mapper composition against emission invariants ("no reachable path emits chargeCard twice", "spawns exactly N children")
• Migration (migrate.cjs: pure, two-phase, fenced, $migrate-journaled) and archival tooling
• Every milestone (M0–M3) shipped through adversarial multi-agent review; all confirmed findings fixed. 60+ tests green on both stores; the kill -9 mid-charge demo recovers with exactly one charge

The OMS trilogy

• examples/polyrun-oms — Temporal's order-management reference app rebuilt on polyrun: multi-fulfillment orders splitting into shipment children with a completion rollup, amend-with-timeout, idempotent billing, a User/Courier storefront. Every machine is polygen-authored from a pinned contract and model-checked before first run (one recorded hand-repair, honestly documented in machines/order/REPAIR-NOTE.md).
• examples/polygraph-oms-go — both workflows of the reference app audited in their original Go: ground-truth traces from the unmodified code via Temporal's own testsuite (no server), positive/negative controls, three independently LLM-generated specs per workflow (27/27 and 21/21 replay), and unanimous model-check verdicts with shortest counterexamples. Findings, framed as intent observations rather than bug reports: an all-unavailable amended order completes with nothing fulfilled or charged; partial failure reports as plain success; carrier status is applied verbatim (any string, free regression). The negative control for the shipment audit is itself the finding: a spec of the documented behavior fails replay against the real code.

polygen pipeline hardening

• Object-aware domain-gap heuristic (object-valued dataDomain entries are checked by their scalar leaves — no more permanently-unsatisfiable false positives)
• Dead-at-init gate: a module that validates strict-clean but rejects every action from its initial state is refused with a diagnosis (catches the name:-component local-state binding), fed back into the authoring retry

Documentation

docs/ARCHITECTURE.md (three engines, one artifact family), docs/SDLC.md (team lifecycle for agentic workflows, incl. versioning best practices), docs/VERSIONING.md (an essay on state-machine compatibility), docs/polyrun-spec.md.

Full details in CHANGELOG.md. Plugin users: /plugin marketplace update polygraph, then start a fresh session.

Same disclosure as always: Polygraph is experimental, and a consistency check, not a proof — every finding is a lead to investigate by hand.

Polygraph/Polygen 2.0.0

The derived artifact moves from the bare next() contract to the SAM v2 strict profile (@cognitive-fab/sam-pattern 2.0.0): named intents with schemas and finite payload domains, keyed acceptors, observable reject(reason), and a sealed model. The 1.x pipeline stays available end-to-end via --legacy-bare-next for one release.

Highlights

• Step-classified replay triage: rejected(reason) / identity-by-mutation / mutated / unhandled per window, with unexplained unhandled a first-class finding
• Zero-config model checking: exploration domains from the spec's own manifest, determinism double-pass on every check
• --tla: mechanical SAM-to-TLA+ transpilation checked by TLC, folded into the report
• Polygen authors v2 modules with retry-on-truncation, classification/determinism repair feedback, and validate() stage gates
• Release gate: seeded-bug A/B eval (m01-m08) ships at parity or better in both arms at two model tiers (haiku-4.5, fable-5), zero dead specs
• 142 selftest checks; new worked examples turnstile-v2 and etcd-raft-v2

Grounded in the SysMoBench study "Load-Bearing for Verification, Not for Robustness" and sam-lib issues #20-#24, #29, #31.