Code Generation Is Solved; Trust Is the Bottleneck

You have a checkout flow. You have 40 tests. They're green.

Now: what happens when a payment webhook arrives after the user cancels? What happens when a retry lands on a session that already expired? What happens on the fourth failed attempt when autoRenew is off and the period boundary has already passed?

You don't know. Not because you're careless — because a state machine with 6 states, 7 actions, and 3 payload values has thousands of reachable (state, action, data) combinations, and your 40 tests visit 40 of them. The bugs that page you at 2 am live in the other several thousand. Polygraph is a Claude Code plugin and standalone CLI that walks all of them.

Why You'd Bother

Polygraph is for stateful code: reducers, workflow engines, protocol handlers, session managers, order state machines, anything with a dispatch(state, action) shape. If your code is a pile of pure functions, go use property-based testing. If it's a state machine, keep reading.

Narrow on shape, not on language. The model reads your source in whatever it's written in — you name it once as lang in the contract — and the trace format is just NDJSON, so any runtime that can log a {pre, action, data, post} line per step can feed it. What's always JavaScript is the derived spec and your rules, because those are what the replayer and model checker execute on Node.

What you get back is not a lint warning. It's a shortest action sequence that reaches a state violating a rule you wrote. Something like:

✗ never-charged-twice [state] — pred returned false
      init                            {"status":"new","attempts":0,"hasDue":false}
      CREATE({})                   -> {"status":"active","attempts":0,"hasDue":false}
      RENEW_CHARGE({"result":"5xx"}) -> {"status":"grace","attempts":1,"hasDue":true}
      RENEW_CHARGE({"result":"ok"})  -> {"status":"grace","attempts":2,"hasDue":true}

That's a repro. You paste it into a test file, and you have a failing test in about ninety seconds. 

A real one: On a production SaaS subscription-billing machine, Polygraph flagged a disagreement on exactly one window: a 5xx from the payment processor during renewal moved the row to grace and marked it due, when the dunning path in the same codebase correctly treated 5xx as ambiguous. The next retry rotated the idempotency key. If the 503'd transfer had actually settled, the customer got charged twice. A human reviewer had found the same bug by hand; five independent model-derived readings of the source landed on it blind.

And in the controlled seeded-bug eval, the split is worth knowing: replaying real traces against the derived spec found 0 of 5 seeded bugs. Model checking found 5 of 5, with counterexamples. Trace replay tells you whether to trust the model. Model checking is where the bugs actually are.

What It Actually Does

Three artifacts, all diffable, all in your repo:

1. contract.json — the scope. Which state fields matter, which actions the machine accepts, what data each action can carry, which states are terminal, and lang is the language your source is written in.

2. A spec — a JavaScript model of your code, written by an LLM from your source (whatever language that is). It's a strict SAM v2 module: every action it ignores has to say why via reject(reason), it can't hide bookkeeping state, and it declares its own action/data domains — so the checker knows what to explore with zero config. Several specs are generated independently and vote, so one bad generation doesn't decide anything.

export const stateInvariants = [  
  { name: 'locked-only-at-limit', pred: (s) => s.status !== 'locked' || s.attempts >= 3 },
];

export const transitionInvariants = [  
  { name: 'expired-never-verifies', pred: (pre, action, data, post) => !(action === 'ATTEMPT' && data?.expired) || post.status !== 'verified' },
];

3. invariants.mjs — your rules, as plain JS predicates:

This part is yours and can't be automated away. Code with a bug is a perfectly faithful description of the wrong behavior. Invariants are where your intent enters the system.

Then two checks run. 

• Replay asks "is the spec faithful?" Real traces ({pre, action, data, post} windows, captured by wrapping your dispatch once) are replayed against each spec, with positive and negative controls proving the harness can tell good from bad. 
• Model check asks "where are the bugs?" It iterates the faithful spec exhaustively from init against your invariants and prints the shortest path to every violation.

The Caveats

• "Exhaustive" means exhaustive over the finite (action, data) domain declared in your contract. A machine whose behavior depends on unbounded counters or arbitrary strings is checked only at the representative values someone chose. That's the standard TLA+ modeling move, and the gap between declared domain and real data is real.
• It's a consistency check, not a proof. A clean run means your code's observable behavior matches an independent reading of its own source. Nothing more.
• Every finding is a lead to investigate, not a verdict. There is no triage step that discharges "real invariant break with no observable consequence."
• It's experimental and not peer-reviewed. Don't make it your only safeguard on safety-critical code.

API Key and Cost 

Only three things call the Anthropic API: spec generation, code authoring (polygen), and polynv's optional headless invariant harvest. You need ANTHROPIC_API_KEY in your environment for those, including inside Claude Code, where the skills shell out to the same scripts and do not use your session credentials.

Ballpark, on a typical machine:

That second row is the load-bearing one. Everything that checks (replay, the exhaustive model check, version gating, the mutation grade, TLC escalation) is keyless, local, and deterministic on Node ≥ 20. Which is precisely what makes CI viable: you commit the spec, and the gate re-runs it on every merge request for free. No key in CI, no per-MR API bill, no nondeterminism in your pipeline.

That gate is polygate, and there's a GitLab reference implementation at <POLYGATE_GITLAB_URL> — a .gitlab-ci.yml you can copy that runs corpus validation, replay, and the model check against your committed artifacts and fails the MR on a violation. (Contrast: Specula, the closest comparable agentic TLA+ pipeline, reports a median of $57 and 3.7 hours per system. Excellent tool, structurally can't run on every MR.)

Getting Started

Prerequisite, and it's a hard one: The stateful code has to be runnable in isolation, because traces are ground truth from the code actually executing. A clean step boundary: a dispatch, reducer, or handler, from experience, Claude will refactor it easily for you. If it only runs against a live DB or device, stand up doubles first (in Claude Code, the agent will build them). Note this is the only place your language matters, and only for convenience: the bundled withTracing / tapReducer helpers are JS, so a Go or Python machine means writing the {pre, action, data, post} NDJSON lines yourself. It's about ten lines.

Zero-cost first (no key, five minutes):

git clone https://github.com/cognitive-fab/polygraph
cd polygraph && npm test        # validates the bundled corpus, runs the controls
npm run verify:turnstile-v2     # replays bundled specs — see the output shape

Then on your own machine, as a plugin:

/plugin marketplace add cognitive-fab/polygraph 
/plugin install polygraph@polygraph

…and just ask: "verify this state machine", or /polygraph:polygraph for the guided end-to-end run (Claude drafts the contract, instruments the boundary, captures traces, runs controls, triages with you). Trace capture is historically what made this expensive; it's the step the agent now carries.

Or plain CLI, no Claude Code:

Wrap your dispatch once, projecting only the contract's observable keys (JS shown; in another language, emit the same NDJSON shape by hand):

import { withTracing } from '<plugin>/scripts/instrument/trace-emitter.mjs';
const dispatch = withTracing(
  rawDispatch, () => ({ status: m.status }),'traces/s1_normal.ndjson'
);

Note --source takes your real file, in your real language:

node scripts/validate_corpus.mjs contract.json traces/  # no key
node scripts/verify.mjs --contract contract.json --source src/machine.ts \  
     --traces traces/ --model opus-5 --n 5 --out out/   # key, ~$0.50

That writes out/findings.md and the generated specs to out/specs/. Commit the winning one, and from then on the loop is free:

node scripts/check.mjs --spec out/specs/spec_0.js --contract contract.json \  
    --invariants invariants.mjs  # no key, forever

There's no default model: pass --model. Use opus-5 or better; deriving a faithful transition function is a hard reasoning task and lighter models don't clear the bar. If you see empty specs, you lowered --max-tokens below what the reasoning block needs; put it back to 32000.

Apache-2.0. The method is written up in arXiv:2607.05076.

Your test suite is a sample. This is the census.