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), 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 was REMOVED in 8.0.0: it is refused by the
prompt builder, the replayer, the checker, and the mutation control alike.
(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 — naming a
  rule does NOT make that branch a rejection. In the v2 pipeline each rule is
  CLASSIFIED against the captured corpus (n8n field study,
  `eval/FINDING-n8n-reject-no-write.md`: generations rejected every branch
  that carried a rule name until the prompt distinguished them): windows all
  no-op → rendered as a required `reject(name)`; windows change state →
  rendered as a named BEHAVIORAL rule the acceptor must perform; unexercised
  → decide-from-source. Name rules for behavioral branches freely — but give
  every rule trace coverage so it classifies from evidence.
- **dataDomain** — REQUIRED in the v2 default for every action with data
  fields: a finite list of representative payload values per field. It is the
  generation domain, the model-checking exploration domain, and the TLC
  transpilation domain; a gap blocks generation loudly (no silent exclusion).

State the **no-op rule** explicitly: an action arriving where the code ignores
it yields `post == pre`. This makes the replay total. In the v2 artifact the
spec makes that no-op *observable* — it must `reject(reason)`, never throw.
Every action that appears in the traces must be declared in the contract: the
strict module has no silent-unknown-action fallback (an undeclared action
classifies as a contract-error, which is what it is).

## Step 2 — Capture traces from the code (YOU run this, autonomously)

This is the heavy step, and it is yours to carry — not the user's. If the code
does not run in isolation, **build the test doubles or emulators needed to run
it** (the finixpos study's agent built a payment-terminal emulator and a
fault-injection proxy to do exactly this), instrument a copy, drive the
scenarios, and produce the corpus. Only escalate to the user for judgment calls:
whether the contract's observable state is right, and whether a double you built
faithfully matches the real dependency (the correlated-oracle risk — validate at
least one assumption against a real service/sandbox when one exists).

Instrument a **copy** of the code (keep the change as a diff/patch) to emit one
NDJSON record per step: `{"pre":{...},"action":"NAME","data":{...},"post":{...}}`.
Capture `pre` before any internal rewriting of the action, `post` after it
settles.

- For JS/TS, offer the helpers in `${CLAUDE_PLUGIN_ROOT}/scripts/instrument/`:
  `withTracing` (wrap a `dispatch(action, data)`), `tapReducer` (a Redux-style
  reducer), `traceStep` (you already have pre/post), and `withSamTracing`
  (`scripts/instrument/sam-emitter.mjs`) for code built on the SAM pattern
  (`@cognitive-fab/sam-pattern`, optionally with `sam-fsm`) — it wraps the
  `component` config so every dispatch emits a window, no-ops included. For other
  languages, write a small emitter by hand following the same shape.
- **Check for an existing seam before writing one.** If the target already
  exposes a step listener / observer / middleware hook, register on it — that
  is a stable attachment point, unlike a patch that rots when the code moves.
  Code authored through this toolchain always has one
  (`docs/capture-ready.md`); code polygen wrote is captured with
  `withSamTracingV2(instance, file)` and needs no shim at all. Only instrument
  a copy when no seam exists. Do NOT reshape someone else's target to make
  capture easier — that changes the thing under audit. (If you are separately
  fixing or authoring code in that repo, `docs/capture-ready.md` is what to
  shape it toward.)
- **Capture by event subscription, never by polling.** Hook the target's own
  event/observer/callback surface (a dispatch wrapper, a reducer tap, the
  library's Observer mechanism) so every transition emits a window. Treat
  "sleep and poll the state" as a red flag for ANY transition that can resolve
  faster than the poll interval: in the hashicorp/raft field study
  (`eval/FINDING-raft-field-study.md`), polling every ~2 ms silently missed
  *every* Candidate occupancy because elections resolved faster than the poll
  — the corpus looked healthy and was structurally blind to a whole state.
- Drive scenarios, one trace file per scenario: the normal path, each failure
  class, races, and deliberate glitches (an action into a terminal state → a
  no-op window). Use existing test doubles or emulators.
- **Sanity-check coverage against the contract**: a state or special rule the
  contract declares but the corpus never visits is a capture bug until proven
  otherwise (too-coarse polling, a scenario you didn't drive) — not evidence
  the state is rare. Step 3's `mutate.mjs --all` makes this check mechanical:
  a zero-flip mutation names a rule no trace exercises.
- Then validate the corpus:
  `node ${CLAUDE_PLUGIN_ROOT}/scripts/validate_corpus.mjs contract.json traces/`
  Fix any chaining or terminal-state problem before continuing (traces are
  ground truth). Give any special rule ≥3 windows or the validator warns.

## Step 3 — Controls FIRST (never skip)

Before involving the model, establish that the replay discriminates:

- **Positive control**: write a reference `next()` yourself by reading the code;
  it must score 100%. Replay it with:
  `node ${CLAUDE_PLUGIN_ROOT}/scripts/verify.mjs --contract contract.json --traces traces/ --specs <dir-of-your-reference-specs>`
- **Negative control — scripted, one command** (this is the only step that
  proves the harness CAN fail; do not hand-edit spec copies):

  ```
  node ${CLAUDE_PLUGIN_ROOT}/scripts/mutate.mjs \
    --spec reference.js --contract contract.json --traces traces/ --all
  ```

  This enumerates targeted mutations of the reference (guard negation,
  transition retarget, acceptor widening, field freeze — the same operators
  polynv's adequacy grade uses), applies each, and reports the windows that
  flip. Read the three outcomes:
  - *windows flipped* — the corpus discriminates that rule ✓;
  - *behaviorally EQUIVALENT* — no corpus could distinguish this mutant;
    discarded, not a problem;
  - *ZERO windows flipped* (exit 1) — a **corpus blind spot**: no captured
    trace exercises that rule, so a real regression there would replay clean.
    Capture a trace that drives it before trusting a clean run. This is the
    trace-side twin of the checker's FROZEN STATE KEY warning.

  `--list` shows the mutation ids; `--apply <id>` runs one.

## Step 4 — Generate and replay

Run the full loop:

```
node ${CLAUDE_PLUGIN_ROOT}/scripts/verify.mjs \
  --contract contract.json --source path/to/source --traces traces/ \
  --model opus-5 --n 5 --out out/
```

This builds a derivation-mode prompt (it never describes per-state semantics),
generates N independent specs, replays each, and writes `out/findings.md` and
`out/findings.json`. Use `--n 3` or more; a single generation may omit a rule.
If the first pass hits the reject-as-annotation signature uniformly (every
live spec rejected ≥2 windows the code acted on), verify **auto-regenerates
once** with the offending branches called out and reports the second pass —
both spec sets are preserved (`specs/`, `specs_regen/`); `--no-auto-regen`
disables this.

If every window comes back `unscoreable-all`, the generations were empty — with
a reasoning model (e.g. `claude-opus-5`) the thinking block spent the token
budget before any answer. Add `--max-tokens 32000` (the default is already 32000;
only lower it deliberately).

If generation reports `refused by the API (category=...)`, that is a **policy**
outcome, not a transient one — retrying the identical prompt will not help.
This is a live risk for this tool specifically: every prompt it sends is
"here is code, here is how it might be wrong," which is also what exploit
research looks like, so a source file whose own comments describe a bug can
trip the classifier. Switch `--model` (it has been model-specific in practice:
on 2026-07-24 `claude-opus-5` refused two eval machines on the since-removed
bare-next prompt that `claude-opus-4-8` and `claude-sonnet-5` accepted), or configure a
fallback model.

## Step 4b — Model-check the spec against invariants (THE BUG-FINDER)

Replay (Step 4) only catches a bug when the derived spec DISAGREES with the code.
A faithful spec — which capable models produce on legible code — does not
disagree, so replay alone misses real bugs (measured: `eval/FINDING-faithful-reproduction.md`).
The half that actually finds bugs is iterating the spec against invariants.

- Write `invariants.mjs` WITH the user — rules encoding what the code *should*
  do (intent), not what it does. Export
  `{ stateInvariants: [{name, pred:(state)=>bool}], transitionInvariants: [{name, pred:(pre,action,data,post)=>bool}] }`.
  A predicate returns true when the rule holds. Aim these at the special rules
  and at the safety properties the code exists to enforce ("never publish without
  approval", "never charge without confirmation", "lock by N attempts").
- Provide a finite `dataDomain` in the contract for actions with data (or rely on
  the values observed in the traces).
- Run it (verify.mjs runs it automatically when an `invariants.mjs` sits beside
  the contract, or pass `--invariants`):
  `node ${CLAUDE_PLUGIN_ROOT}/scripts/check.mjs --spec <mod.js> --contract contract.json --invariants invariants.mjs --traces traces/`
- A reachable violation is a **bug**, reported with the shortest counterexample
  path from init. A violation reached by ALL generated specs is a strong signal
  (every independent reading reaches the bad state). Walk the counterexample in
  the source.
- In the v2 default, exploration domains come from the module's own
  `manifest()` (no `buildDomain()` inference, so nothing is silently excluded)
  and every check runs a determinism double-pass — a `nondeterminism` finding
  means two identical explorations diverged (a clock/random read in the spec).
- Honest limits: exploration is bounded (report cap hits); and a hazard that
  depends on an EXTERNAL service (not in the observable state) is invisible to
  reachability — it needs a real sandbox probe, not a bigger search.
- Read the checker's structural warnings, they are findings about the CHECK
  itself: a **FROZEN STATE KEY** (a key no action changes — Part 2 is blind to
  behavior it gates; seed `--initial-states` with non-default values, or
  capture traces that vary it) and a **drift warning** (a key minting fresh
  states forever — the state space is likely unbounded in that key; abstract
  it in the contract or lower `--max-states`, and treat any clean verdict as
  covering an arbitrary prefix).

## Step 4c — TLC escalation (optional, `--tla`)

Add `--tla` to `verify.mjs` to escalate the winning live spec (most windows
passed; tie → first) from "bounded exploration says" to "TLC says": the spec
is mechanically transpiled to TLA+ (`out/tla/*.tla` + `.cfg`), state
invariants whose predicates stay inside the translatable subset are carried
along as TLA+ INVARIANTs, and TLC runs when a toolchain is available
(`POLYGRAPH_JAVA` or `java` on PATH, plus `POLYGRAPH_TLA_JAR` pointing at
`tla2tools.jar`). The findings report gains a "TLC escalation" subsection:
states generated/distinct, a per-invariant verdict table, counterexample
steps on violation, and every skipped invariant named with its reason
(transition invariants are skipped by kind; check.mjs still checks them in
JS). A missing toolchain is a note, not an error — the `.tla`/`.cfg` are
still written for running elsewhere. A transpiler refusal names the offending
construct: transpilability is a checkable property of the spec.

## Step 5 — Triage each disagreement (do this WITH the user)

`findings.md` classifies every non-consistent window:

- **code-finding / contract-error** (all specs disagree with the trace): either
  the code does something unexpected (a defect — open the source at that
  pre-state and action) or the observable-state contract omits a field that
  drives the transition (widen it and return to Step 2).
- **spec-error** (some specs pass, some fail): usually one generation missed a
  rule — but check the report's **spec agreement** line and the **split**
  column first. A lopsided split (4-vs-1) cuts both ways: several specs making
  the IDENTICAL mistake looks the same as one spec missing a rule, and in the
  raft field study the majority was wrong (4 of 5 collapsed two independently
  gated updates into one; the lone dissenter matched the hand control). Judge
  the minority against the source, not the vote count. Note *which* rule — it
  is typically a special case outside the main state table, and worth a code
  comment for the next reader.
- **unscoreable in all specs**: the generated modules did not load or lack the
  expected surface. Fix generation, not the code.

In the v2 default each finding row also carries a **step classification** per
live spec. `rejected(reason)` and `identity-by-mutation` are the two GOOD
no-op classes (the spec explicitly declined, or explicitly re-committed the
same state); `unhandled` — the spec neither acted nor rejected — is itself a
finding (usually a missing acceptor case, or a rule the code has that the
contract does not). A *uniform* rejection-reason on a code-finding window
usually means the contract took a side (a specialRule the corpus classified —
or an authored rule declaring a no-op) that the code did not — triage it as a
contract question first. Note the tension with auto-regeneration: the regen
trigger fires on this same signature and re-prompts toward the CODE's
behavior; if the contract deliberately declared those windows no-ops, the
first pass in `specs/` was the real signal — re-run with `--no-auto-regen`
before accepting the regenerated pass.
And a `rejected(...)` classification on windows where the TRACE changed state
(the report counts these as "REJECTED while the code ACTED") is the
**reject-as-annotation trap** when uniform: a generation computes the correct
`next.*` writes and then appends `reject(reason)` as a success label,
discarding its own work (hatchet field study — 5 of 5 specs, 0/19 → 19/19 by
deleting that one line). Inspect the specs for a trailing reject after
`next.*` writes before reading any of it as a code finding.

When every window is consistent across all specs, report it as exactly what it
is: the code's observable behavior matches an independent reading of its source.
To go further, propose invariants over the traces, or a hand-written model
checked against an explicit environment.

## Notes to carry into the work

- Traces are ground truth. Spec-vs-trace disagreement with a correct-looking
  spec is a code finding, not a bad window.
- If the source uses a framework, a generated spec may copy the framework's
  wiring instead of the module contract — the bare `next()` contract minimizes
  this; watch for `unscoreable-all`.
- If traces come from a mock/emulator written alongside the code, both may share
  a misunderstanding of a real dependency. Validate at least one assumption
  against the real service (e.g. a sandbox).
- The spec must be deterministic. Model timeouts and other time-driven behavior
  as explicit actions issued by the environment, never as a clock read.

## Provenance — why these two artifacts, and why v2 is the default

The design follows the SysMoBench paper's findings (and its v2 postscript).
The paper's data splits Polygraph's two roles: as a **replay oracle**, the
the (now removed) bare-next artifact plus one discipline sentence was the
best performer for
pure trace conformance — and the control showed it was the sentence, not the
structure, that carried the robustness. That sentence is kept **verbatim** in
the v2 prompts: "Acceptors must guard against invalid proposals (an action
that the implementation does not act on in the current state must be a no-op
via `reject(reason)`, NOT a throw)". As a **checkable substrate**, the v2
strict module is strictly stronger: schema-enforced wiring (no silent dead
specs), sealed model (no hidden state), observable rejection, manifest-
declared domains (closing the silent-exclusion gap), determinism checking,
and a mechanical path to TLC. Polygraph ships one artifact for both roles —
v2 — because the N-spec voting layer absorbs exactly the failure mode v2
gives up (occasional individual conformance misses) while v2 eliminates the
failure modes voting cannot absorb (dead specs, hidden state, vacuous
exploration).

Reference implementation and origin: the SysMoBench "finixpos" study at
<https://github.com/jdubray/SysMoBench-1>. (Lineage note: this repo's disk
name, `bare-next-verify`, records the original bare-next artifact; the repo
is not being renamed.)