/polygraph

name: polygraph
description: A polygraph for your state machine. Audit a stateful piece of code end-to-end: YOU (the agent) instrument a copy, build any test doubles needed to run it, and capture real execution traces, then derive a transition-function spec from its source with an LLM (default artifact: a SAM v2 strict-profile module — named intents/schemas/domains, keyed acceptors, observable reject(reason), sealed model, next-state (prime) acceptors; --legacy-bare-next keeps the original bare next(state, action, data) contract), replay the traces against it, model-check it against invariants, and surface every disagreement as a spec-error, a code-finding, or a contract-error. Optional --tla tier escalates the winning spec to TLC. Use when the user wants to verify a state machine, workflow, reducer, or protocol implementation against its own behavior; check whether code does what it is believed to do; or reproduce/triage suspected state-handling defects. Trigger phrases: "polygraph", "verify this state machine", "check my reducer/workflow", "does this code do what I think", "audit the payment/order/session flow", "bare next / trace validation", "SAM spec verification".

Polygraph — a polygraph for your state machine

Guide the user through a five-step, trace-driven consistency check. You (the in-session assistant) do the intelligent parts — designing the contract, instrumenting the code, capturing traces, and triaging findings. The bundled scripts do the mechanical parts — building the prompt, generating specs, replaying, and classifying.

> **Tell the user this up front, once.** Disclosure: Polygraph is experimental, > not peer-reviewed, unproven technology — newly published and highly > speculative. It is a *consistency check, not a proof*: > a clean run means the code's observable behavior matches an independent > reading of its source, nothing more. "Exhaustive" means exhaustive over the > finite (action, data) domains the contract/module declares — data-dependent > behavior beyond those representative values is unchecked, and that > abstraction gap is not measured by any gate. Every finding is a lead to investigate by > hand, not an established result. Do not present it as a guarantee, and do not > let it be the only safeguard for correctness- or safety-critical code.

> **Prerequisite — real traces, or this is the wrong tool.** The trace corpus > is not an input among others; it IS the verification. Part 1 (replay) checks > the code's *captured behavior* against an independent reading of its source — > with no real traces there is nothing to check, and hand-modeling both sides > is grading your own homework (the model-check half then only tests whether > your own model agrees with your own invariants). If the code cannot be run > and instrumented — no way to execute it, no test doubles buildable, capture > forbidden — say so and stop: recommend hand-written modeling (e.g. TLA+ from > the spec) instead of Polygraph. Do not substitute synthetic traces derived > from reading the source; they inherit every misreading the specs will make.

All scripts live under `${CLAUDE_PLUGIN_ROOT}/scripts/`. Node ≥ 20 is required. Generation needs `ANTHROPIC_API_KEY` and an explicit model (recommend `opus-5`; on an API policy refusal retry with `opus-4.8` — per-step source of truth: `RECOMMENDED_MODELS` in `scripts/models.mjs`; there is no default). Replay and controls need no key.

**The artifact (v0.7):** by default the derived spec is a **SAM v2 strict-profile module** (`@cognitive-fab/sam-pattern` 2.2.0, vendored at `scripts/vendor/sam-pattern.cjs`): named intents with per-intent schemas and finite payload **domains** declared in a manifest, acceptors keyed by intent name, every ignored action an observable `reject(reason)`, a sealed model (no hidden state), and **explicit next-state (prime) semantics** (sam-lib 2.1, #25) — each acceptor is a TLA+-style next-state relation: `model` is the frozen pre-state, writes go to the `next` draft (`next.x = model.x + 1`), and every declared variable is either assigned or named `unchanged(...)` per accepted step. This buys evidence bare-next could not produce: a failing no-op window now says *why* the spec did nothing (`rejected(reason)` / `identity-by-mutation` / `unhandled`), dead wiring is a load-time error instead of a silent zero, statement order can no longer change a transition's meaning, the checker's exploration domains come from the module's own manifest, every check runs a determinism double-pass, and the spec is mechanically transpilable to TLA+ (`--tla`). The original bare `next(state, action, data)` artifact remains available end-to-end behind `--legacy-bare-next` for one release. (2.0-form strict modules — acceptors that write `model.x` directly — throw `SamShapeError` under 2.1: migrate them, see sam-pattern's docs/MIGRATION.md.)

House rule (from sam-lib #29, fixed structurally in 2.0.0-alpha.2): never rely on `instance({}).state()` — on machines whose primary control key is `state` it returns data, not the method. The pipeline and the prompts use `getState()`/`setState()` exclusively.

Step 1 — Define the contract (do this WITH the user)

Produce a `contract.json` (schema and example under `${CLAUDE_PLUGIN_ROOT}/templates/`). Decide, by reading the code:

• **stateKeys** — the minimal observable-state fields the behavior depends on.

Exclude display strings, timestamps, and IDs that do not drive transitions. The FIRST key is the primary control state.

• **actions** — the discrete events that step the machine, each with its data

shape. Use the step boundary the code already has (a dispatch, a reducer action, one handled message).

• **initState**, **terminalStates**, and **specialRules** (guards / rewrites /

special cases that live outside the main state table — these are the rules models most often miss, so flag them for extra trace coverage). A rule's name/note is DOCUMENTATION of why a branch behaves as it does