polygen — author verifiable code, out of the box

Companion to the polygraph skill. That one AUDITS code that already exists. This one AUTHORS new code so it's verifiable from the start — closing the loop at creation time instead of retrofitting it later. v1 is JS/TS only: the generated module is directly usable only in a JS/TS codebase (porting a verified model to another language is a real, separate problem — the port itself would need its own differential check against the JS original — and is out of scope here).

The authored artifact (v0.7): by default a SAM v2 strict-profile module (module.exports = { instance, init, actions, getState, setState }, sam-lib 2.1.2 vendored in the plugin): named intents with schemas and finite domains, acceptors keyed by intent name, every not-applicable action an observable reject(reason) (never a throw), sealed model, and explicit next-state (prime) semantics — acceptors write the next draft and frame untouched variables with unchanged(...) (sam-lib 2.1, #25). Generated code must load strict-clean — instance({}).validate() is a hard gate at every stage boundary, so schema/shape errors block instead of becoming report lines, and dead wiring cannot ship silently. The self-repair loop feeds back lastStep() classifications and determinism flags, not only windows and invariants. (House rule from sam-lib #29, fixed in 2.0.0-alpha.2: never rely on instance({}).state(); the pipeline uses getState()/setState() only.)

Same disclosure as polygraph. This is experimental, unproven technology and a consistency check, not a proof. A converged run means the authored code satisfies its OWN stated invariants over a bounded, explored state space — nothing more, and that space is finite only because the contract declares finite action/data domains; behavior at values outside the declared representatives is unchecked. The contract and the invariants are the model's reading of your intent; they need your review before either is trusted.

All scripts live under ${CLAUDE_PLUGIN_ROOT}/scripts/. polygen.mjs needs ANTHROPIC_API_KEY and an explicit --model (no default; recommend opus-5 with the self-repair loop on, which is the default — fable-5 only for one-shot runs with --repair-max 0, and opus-4.8 as the retry if the API refuses on policy grounds. Per-step source of truth: RECOMMENDED_MODELS in scripts/models.mjs).

Step 0 — Choose the authoring path (key or no key)

Only the AUTHORING model call needs a key. Every gate below it — the strict validate() load, check.mjs model checking, corpus validation, replay, check-effects, the polyrun deploy gate, polyvers, polynv — is pure local execution. That means there are two legitimate paths, and the user chooses:

• Keyed (scripted) — the CI / reproducibility path. polygen.mjs with ANTHROPIC_API_KEY: pinned model id, deterministic harness, the automated self-repair loop, the standard polygen-report.md, and the synthesized corpus independently replayed in a separate process. This is the path for enterprises wiring authoring into CI, and for anyone who wants the run re-executable byte-for-byte later.
• Keyless (in-session) — the zero-cost adoption path. YOU are the authoring model. Author contract.json, the SAM v2 strict-profile module, and invariants.mjs in this session, in the exact artifact style (copy shapes from an existing example, e.g. ${CLAUDE_PLUGIN_ROOT}/examples/workflows-not-loops/pipeline-v1/), then run the SAME mechanical gates the script would: check.mjs (fix code at any counterexample and re-check — that is the self-repair loop, performed by you), drive the module through exported scenarios to synthesize a corpus, validate_corpus.mjs, and replay in a separate process. A/B evidence that this is not a degraded mode: an in-session-authored machine and a scripted polygen.mjs run against the same contract were behaviorally identical over the full explored space (270/270 edges, examples/workflows-not-loops/README.md "Provenance") — the checkers, not the key, carry the guarantee.

When no key is present, ASK — never fail silently and never fall back silently. The user decides, with the tradeoffs in front of them. The question to put to them, roughly:

I don't have an ANTHROPIC_API_KEY in this environment. Two ways forward: (a) continue keyless — I author the artifacts in this session and run every mechanical gate locally (model check, corpus validation, separate- process replay); same checking strength, zero API cost; what you give up is a pinned model id and a scripted, re-runnable authoring step. (b) supply a key — the scripted polygen.mjs run: pinned model, automated repair loop, the standard report; this is the path you'd wire into CI. Which would you like?

If they choose keyless and later want the CI-grade run, the same contract feeds polygen.mjs --contract unchanged.

State the provenance either way in the handoff ("authored in-session, keyless, all gates green" vs "polygen.mjs, model X, converged iteration N") — the artifacts must say which path produced them. What the keyless path gives up is reproducibility of the authoring step itself (no pinned model, no scripted rerun), never checking strength.

Step 1 — Get the feature intent and the contract (do this WITH the user)

Ask for (or draft from) a plain-language description of the feature: the states it moves through, the events that step it, and anything the user already knows should never happen (a payment recorded twice, a lock releasing without an explicit unlock).

You have two paths:

• Model drafts the contract (the default): pass --intent "<description>" with no --contract. polygen.mjs drafts contract.json from the intent — observable state, action alphabet, dataDomain (concrete values for every parameterized action field — this is not optional: an action field missing from dataDomain is silently excluded from model-checking below), terminal states, and special rules. Review this before continuing — it is now the design spec everything else is built against; a wrong contract produces correctly-verified code against the wrong intent.
• You supply the contract (--contract <c.json>): use when the user already knows the exact shape (e.g. this is one leg of a larger system with an established observable-state convention).

Step 2 — Run polygen

node ${CLAUDE_PLUGIN_ROOT}/scripts/polygen.mjs \
  --intent "<feature description>" --model opus-5 --out out/

This authors the v2 SAM module, proposes invariants.mjs, then self-repairs: model-checks the code against its own invariants and, on a reachable violation, patches the code and re-checks — up to --repair-max (default 3) rounds. It then synthesizes a demo/regression trace corpus by driving the final code through model-proposed scenarios, validates it (validate_corpus.mjs), and independently replays it in a separate process as a sanity check (catches nondeterminism the in-process generation wouldn't expose).

Everything lands in <out>/: contract.json, next.cjs (the module file — the name is historical; in the default mode it contains the v2 SAM module), invariants.mjs, traces/*.ndjson, and polygen-report.md (which names the artifact mode it was authored in).

Step 3 — Read the report and triage (do this WITH the user)

• Converged, no domain-coverage gaps: the code satisfies its own invariants over the explored space. Still review the contract and invariants by hand — a converged run against a wrong or incomplete contract proves nothing about the actual feature.
• Did not converge within the repair budget: the report says so plainly and lists the residual violation(s) with a counterexample. Do not treat this as shippable — either fix the code by hand at the counterexample, or re-run with a higher --repair-max.
• Domain coverage gaps (flagged at the top of the report): an action field had no dataDomain entry, so that action was invisible to the checker. Add the missing domain to contract.json and re-run — the "converged" verdict above did not actually examine that action.
• Corpus problems that survived the one feedback retry: read them; usually a scenario that doesn't drive to a declared terminal state.

Step 4 — Hand off to integration + audit

Wiring the generated next() into the real app is deliberately NOT scripted — it needs a human or an integrating agent making real judgment calls about the handler/route/reducer it plugs into. Instruct whoever does this:

• Call the module; do not reimplement the transition logic inline. (v2: dispatch through actions[name](data) and read via getState(); legacy: call next().) The whole point of authoring it this way is that the transition logic lives in exactly one place.
• Once wired up, capture REAL traces from the running integration and run /polygraph:verify (the polygraph skill) against them. This is the step that catches drift — e.g. someone "helpfully" tweaking the wiring later and reintroducing logic outside next(), or the pure model disagreeing with how the real handler actually calls it.

• Do NOT write an instrumentation shim for the generated module. It is already capture-ready: register the framework's step listener and drive the scenarios.

  const control = instance({ initialState, component });
  withSamTracingV2(instance, 'traces/s1.ndjson');  // scripts/instrument/sam-emitter.mjs

  Rejected steps emit windows too, so no-ops are recorded rather than inferred. Instrumenting a copy is the retrofit path for code we did not write; using it here means the wiring, not the module, is what actually needs the seam — say so explicitly instead of patching around it.

Capture-readiness review (Step 3.5 — cheap, and only cheap now)

The v2 artifact gives you most of docs/capture-ready.md structurally: one named step boundary, getState() projecting the declared keys, observable reject(reason), a stepListener seam, one in-flight step per instance (CR-1..CR-4, CR-8). Three requirements are NOT structural — check the generated module for them before handing it off, and repair by hand if needed:

• CR-5 — no ambient non-determinism. Date.now(), Math.random(), crypto.randomUUID(), process.env inside an acceptor. These belong in injected ports so a scenario can pin them at a seed; otherwise the module cannot be re-captured deterministically, and a real corpus can only be made comparable by redacting fields the transition depends on.
• CR-6 — effects declared, not awaited. No await fetch(...) / DB call inside a transition; record the intent and let the caller perform it. This is also the precondition for running the module under polyrun.
• CR-7 — scenarios exported as plain functions, not buried in a test runner, so the same drivers serve the synthesized corpus and any later capture run.

Fixing these after the module is wired into an app is a refactor; fixing them now is an edit. Name any you could not fix in the handoff.

Notes to carry into the work

• The repair loop fixes CODE, never invariants — an invariant encodes intent by definition; if a "violation" is actually a misunderstanding of intent, that's a signal to fix the contract/invariants and re-run, not to weaken the rule until it stops firing.
• A reachable violation on iteration 0 (before any repair) usually means the model's first draft missed a special rule named in the contract — worth noting which one, the same way polygraph's Step 5 does for spec-errors.
• LLM output can have a genuine syntax slip (a stray ; where a , belongs). polygen.mjs retries once with the load error fed back before giving up — if you see a hard failure citing "still fails to load," that's a real defect worth a closer look, not a transient issue.

Reference implementation and origin: the SysMoBench "finixpos" study at https://github.com/jdubray/SysMoBench-1, and the polygraph skill this one complements.