Polygraph

Your tests check the paths you thought of. Polygraph checks the ones you didn't.

Polygraph is a Claude Code plugin (and standalone CLI) that finds bugs in
stateful code — workflows, reducers, protocol handlers, checkout flows,
session managers — by exhaustively exploring every state the code can reach
over a finite, declared domain of actions and payloads, and flagging the
ones that break rules you care about, like "a customer is never charged
twice."

You don't need to know anything about formal verification to use it. You
write the rules as plain JavaScript predicates. The heavy lifting — deriving a
formal model of your code, exploring the state space, producing a shortest
path to each violation — is done for you.

Disclosure — read this first. Polygraph is experimental, not
peer-reviewed, unproven technology. It is a consistency check, not a
proof: a clean run means the code's observable behavior matches an
independent reading of its own source, and nothing more. "Exhaustive"
always means exhaustive over the finite (action, data) domains declared
in the contract — not over unbounded real-world data (see
What "exhaustive" means).
Every finding is a
lead to investigate by hand, not an established result. Do not rely on it
as your only safeguard for correctness- or safety-critical code.

About

Polygraph is developed by Cognitive Fab LLC (https://cognitivefab.com). For
questions, commercial support, or collaboration, reach us at
[email protected].

Demos & write-ups

The DAAO demo — a Dual-Authorization Action Order machine taken end to end
through the method (author it, break it, catch it, version-gate it) — lives in
its own repo: cognitive-fab/polygraph-demo-daao.

Three articles walk the demos:

1. DeepSeek wrote the code. A two-line prompt checked every reachable state. — auditing existing code with /polygraph:verify.
2. polygen wrote the dual-authorization code — authoring verified-from-birth code with polygen.
3. You just changed the code of your state machine. Now what? — version-gating a change against the live fleet with polyvers.

Why Polygraph

Unit tests execute the scenarios you wrote. A state machine of even modest
size has orders of magnitude more reachable states than any test suite
visits — and the bugs that hurt in production live in the combinations nobody
wrote a test for: a retry landing after a cancel, a timeout racing a
confirmation, an event arriving in a state where nobody expected it.

Polygraph attacks that gap in two ways:

• Audit existing code (/polygraph:verify). An LLM reads your source and
  writes an independent, executable specification of it — a second opinion on
  what the code does. Polygraph then (1) replays real execution traces
  against that spec to confirm it's faithful, and (2) model-checks it:
  starting from the initial state, it tries every action with every declared
  payload value, visits every state reachable that way, and reports any state that violates
  one of your rules — with the shortest sequence of actions that gets there.
  That counterexample path is a ready-made repro for the bug.

• Author new code (polygen). Give it a one-sentence feature description
  and it writes the state machine and its rules, model-checks its own
  output, repairs violations, and hands you code with a passing exhaustive
  check plus a generated regression trace corpus — verified from the moment
  it's written.

Real result: on a production SaaS subscription-billing machine, this method
independently corroborated a genuine double-charge bug
(examples/case-study-subscription.md).
In the controlled eval, replay alone found 0/5 seeded bugs — model checking
found 5/5, with counterexamples
(eval/FINDING-faithful-reproduction.md).

Why not use TLA+ / Alloy / a model checker directly?

Those tools work — but you have to hand-translate your code into their
language and keep the translation current, which is why almost nobody does
it. Specifying even a small-to-midsize system is a multi-month effort, and
every code change invalidates the spec. Polygraph's bet is that an LLM can
produce that formal model from your source cheaply enough to rerun on every
change, and that replaying real traces against the model tells you whether to
trust it. You stay in JavaScript the whole time. (If you do want the real
thing, an optional --tla flag mechanically transpiles the winning spec to
TLA+ and runs TLC over it.)

This bet is no longer a fringe position — and the strongest evidence for it
comes from a project that is ahead of Polygraph on the one axis the two
share:

Specula: Scaling formal specifications for autonomous model checking of
system code. arXiv:2607.25333, July 2026.
https://github.com/specula-org/Specula (Apache-2.0)

Specula is an agentic TLA+ pipeline standing on the same three legs Polygraph
does — spec generation, model checking, trace validation. Its paper reports
249 bugs across 48 projects (MongoDB, Etcd, ScyllaDB, GCC libgomp, LLVM
libomp), 207 previously unknown, 68 confirmed and 24 fixed upstream, at a
median of $57 and 3.7 hours per system. The convergent finding is the one
that matters: the LLM alone is not trustworthy, but an LLM held accountable
by a model checker and trace validation is a practical bug-finder.

Where Specula is ahead of Polygraph's audit engine, plainly:

• Its capture is engine-owned and repeatable. Its agents instrument the
  target, and a replay harness verifies post-state agreement inside the
  pipeline, with a conformance repair loop. Polygraph's capture is owned by
  the agent per run (Step 2 of the skill), so the harness is not by default a
  committed, re-runnable artifact.
• It reproduces bugs in the running system, forcing the counterexample
  schedule at code level and assessing consequence. Polygraph stops at a
  spec-level counterexample path.
• It triages. 48.8% of its model-level violations were discharged as
  masked — real invariant breaks with no observable consequence. Polygraph
  hands you all of them as leads to check by hand.
• It has third-party confirmation. Upstream maintainers fixed 24 of its
  findings. Polygraph has one corroborated production bug and a seeded-bug
  eval.
• It requires invariants to cite their evidence — a commit, code
  location, or issue. polynv harvests candidates but does not demand
  provenance.

The difference is not that Polygraph audits better. It is that auditing is
one engine of several here, and Specula has no authoring, no CI gate, no
runtime, and no versioning — its paper states specs are generated from a
snapshot and must be regenerated when the code changes. At $57 and 3.7 hours
per system it structurally cannot run on every merge request; Polygraph's
model check and replay are keyless and deterministic, which is what makes
polygate possible. Different bet, different slot. If your problem is deep
bugs in a large concurrent or distributed system written in C, C++, Go, Rust,
Java, or Erlang, use Specula — that is what it is for, and it is good at
it.

The five engines share one artifact family, so what one produces the
next can consume: Polygraph audits (this document), polygen
authors, polyrun executes,
polyvers evolves, polynv
elicits the rules they all check against.

Deep dives: docs/ARCHITECTURE.md — how the
five engines fit together;
docs/SDLC.md — a team lifecycle for
integrating them into agentic workflows, with the human gates spelled out;
docs/polyrun-spec.md — the durable-execution
harness specification; docs/VERSIONING.md — an
essay on why versioning state machines is hard and how the gates here
make compatibility a checked property instead of a review vibe. Each doc
has interactive diagrams inline; browse them all at
docs/diagrams/index.dc.html.

How it works

Everything revolves around three artifacts you can read and diff:

1. A contract (contract.json) — what's observable: the state fields
   that matter, the actions the machine accepts, the data each action can
   carry, which states are terminal. This is the scope of the audit.

2. A spec — an executable model of your code, written by an LLM from your
   source. By default it's a strict, self-describing state-machine module
   (the SAM pattern v2 strict profile): every action it
   ignores must say why (reject(reason)), it can't hide bookkeeping
   state, and it declares its own action/data domains — so the model checker
   knows exactly what to explore with zero configuration. Several specs are
   generated independently and vote, so one bad generation doesn't decide the
   outcome.

3. Invariants (invariants.mjs) — your rules, as plain JS functions over
   a state: "never charged without a confirmed transaction", "an expired
   session can't accept input." These encode your intent, which is the
   one thing no tool can derive from the code — code with a bug is a faithful
   description of the wrong behavior.

Then two checks run:

Check 1 — replay (is the spec faithful?). Real execution traces —
captured by wrapping your dispatch/reducer once, so every step logs a
{pre, action, data, post} window — are replayed against each spec. Before
any generated spec is trusted, controls run: a hand-written reference spec
must score 100% and a deliberately mutated one must fail, proving the harness
can actually tell good from bad. Disagreements are triaged into
spec-errors (the LLM misread the code), code-findings (the code
disagrees with an independent reading of itself — investigate), and
contract-errors (the contract mis-scoped the problem).

Check 2 — model check (where the bugs are). The faithful spec is iterated
exhaustively from its initial state against your invariants. This is the step
that finds what tests miss: replay can only flag a bug when spec and code
disagree, and a faithful spec reproduces the bug right along with the code.
Model checking reaches the bad state anyway and prints the shortest path to
it. Every check also runs a determinism double-pass for free.

What "exhaustive" means — and what it doesn't

The checker enumerates a finite (action, data) domain declared in the
contract (or inferred from traces) and visits every state reachable from
init over that domain. So the precise coverage claim is: state machines
expressible in the SAM v2 strict profile with finite declared domains —
control-dominated logic (order workflows, auth lockouts, approval flows)
whose data can be finitized to representative values. It is not "arbitrary
state machines": a machine whose behavior depends on unbounded counters,
amounts, or strings is checked only at the representative values someone
declared. Finitizing data this way is the classic, defensible modeling move —
it is exactly what TLA+ users do with model bounds — but the abstraction gap
between the declared domain and real data is where bugs can hide, and no
current gate measures that gap. Choosing domain values that exercise every
boundary the code branches on (and re-checking the contract when the code
grows a new branch) is human judgment, on the same footing as writing the
invariants. One mitigation is built in: the domain cross-check that catches
contract/code vocabulary mismatches
(examples/case-study-polygen-domain-gap.md)
— but it checks spelling agreement, not representativeness. The other
half of the judgment — whether the invariants you wrote are strong — now
has a partial measure: polynv's mutation adequacy grade
(polynv/README.md) reports how many behaviorally
distinct machine mutations your rule set kills, with its own blind spot
stated (behavior-removing mutations largely evade safety invariants).
The domain-representativeness gap itself remains unmeasured.

polygen runs the same machinery in reverse: draft contract → author
module → propose invariants → model-check → self-repair on violations (capped
at --repair-max rounds; a non-converging run is reported as NOT converged,
never silently presented as clean) → synthesize and independently replay a
trace corpus. It also cross-checks that contract and code agree on their
action/data vocabulary, because the two come from independent model calls —
examples/case-study-polygen-domain-gap.md
shows a real run where a silent enum-spelling mismatch collapsed the
explorable state space, and how the check caught it.

polygen output is JS/TS only: the generated module is directly usable in a
JS/TS codebase; porting a verified model to another language would need its
own differential check and is out of scope.

Effort and prerequisites

Trace capture is historically what made this kind of verification expensive,
and it's the step the agent now carries: in the origin study, a Claude agent
built a payment-terminal emulator and a fault-injection proxy, instrumented a
production payment workflow, drove 17 scenarios, and produced a 75-window
corpus autonomously. What stays with you is judgment: confirming the contract
covers the right state, and sanity-checking any doubles the agent built
against reality.

One hard prerequisite: the code must be runnable in isolation, because
traces are ground truth captured from the code actually executing. If it has
a clean step boundary (a dispatch, reducer, or handler), you're set. If it
only runs against a DB/network/device, stand up doubles first (or let the
agent do it). If it can't run at all, replay degenerates to checking specs
against your expectations, which can't find code bugs.

Wrapping the boundary standalone is one line per scenario:

import { withTracing } from '<plugin>/scripts/instrument/trace-emitter.mjs';

// project ONLY the contract's observable keys:
const project = () => ({ txState: m.txState, orderId: m.orderId });
const dispatch = withTracing(rawDispatch, project, 'traces/s1_normal.ndjson');
// Redux-style reducer: tapReducer(...)  ·  SAM component: withSamTracing(...) — see scripts/instrument/

When an API key is required

Only spec generation, code authoring, and polynv's optional
headless --llm harvest call the Anthropic API. Everything that
checks, replays, explores, elicits, grades, or drift-checks runs locally
on Node ≥ 20.

This applies inside Claude Code too: the skills and subagents shell out to
these same scripts, so the generate and polygen steps need
ANTHROPIC_API_KEY set in your environment — your Claude Code session
credentials are not used for them.

Install

As a Claude Code plugin (this repo is its own marketplace):

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

Or clone directly: git clone https://github.com/cognitive-fab/polygraph ~/.claude/plugins/polygraph.
Update later with /plugin marketplace update polygraph. Requires Node ≥ 20.

No npm install is needed for the core loop: the SAM runtime is vendored
(scripts/vendor/sam-pattern.cjs, resolved through scripts/sam-lib.mjs), and
the two npm dependencies are each used by exactly one optional path — acorn
by the --tla escalation tier, pg by polyrun's Postgres store.

In the VS Code extension

Everything here works in the Claude Code VS Code extension as well as the
terminal — the extension bundles the same CLI, runs locally with the same
filesystem and shell access, and shares ~/.claude/settings.json with the CLI,
so a plugin installed on one surface is available on the other.

Type /plugin in the prompt box and select Manage plugins, then:

1. Marketplaces tab → paste https://github.com/cognitive-fab/polygraph
   and hit Add. (The field says "GitHub repo, URL, or path…", but the
   owner/repo shorthand that works in the terminal may not be accepted
   here — the full GitHub URL always is.)
2. Back on the Plugins tab → polygraph appears under Available →
   Install, and pick a scope: for you (all projects), for this
   project (shared with collaborators), or locally (just you, just this
   repo)
3. Restart Claude Code when the banner asks

Open Manage plugins → add the marketplace by URL → install from the Plugins tab. Click any screenshot to enlarge.

Two things behave differently from the terminal, and both look like a broken
plugin if you hit them cold:

• ANTHROPIC_API_KEY may not reach the extension. VS Code does not
  reliably inherit your shell environment, so the key that works in your
  terminal can be invisible to the extension — and the generation steps above
  need it. Set it in the env block of ~/.claude/settings.json (shared by
  both surfaces, so it is the one place worth doing this), or launch VS Code
  from a terminal with code ., or use the claudeCode.environmentVariables
  extension setting. Everything in the no-key half of the table above —
  --specs replay, check.mjs, polyvers, polynv, polyrun, polyviz, the
  controls — is unaffected.
• Long runs are less visible. The extension shows background progress only
  in the status bar. A full generate-and-replay sweep runs for minutes, so
  prefer the integrated terminal (Ctrl+`) for those:
  node scripts/verify.mjs … works there directly, and everything in
  Use it as a plain CLI applies
  unchanged.

Then just ask in plain language — "verify this state machine", "does this
code do what I think it does?", "write a verifiable checkout flow",
"what invariants should this machine have?" — or use
the entry points directly:

Use it as a plain CLI (no Claude Code)

# replay saved specs (no API key)
node scripts/verify.mjs --contract contract.json --traces traces/ --specs specs/ --out out/

# generate + replay (needs ANTHROPIC_API_KEY)
node scripts/verify.mjs --contract contract.json --source src/machine.ts \
  --traces traces/ --model opus-5 --n 5 --out out/

# validate a corpus (no API key)
node scripts/validate_corpus.mjs contract.json traces/

# escalate the winning spec to TLC (no API key; needs Java toolchain)
POLYGRAPH_JAVA=/path/to/java POLYGRAPH_TLA_JAR=/path/to/tla2tools.jar \
  node scripts/verify.mjs --contract contract.json --traces traces/ --specs specs/ --tla --out out/

# elicit invariants: harvest candidates, then grade the confirmed set (no API key)
node polynv/bin/polynv.mjs harvest --artifacts <machine-dir> --traces traces/
node polynv/bin/polynv.mjs questions --artifacts <machine-dir>   # ranked, pre-checked; answer via `record`
node polynv/bin/polynv.mjs grade --artifacts <machine-dir> --include-invariants

# author NEW verifiable code (needs ANTHROPIC_API_KEY)
node scripts/polygen.mjs --intent "<feature description>" --model opus-5 --out out/

# gate a version change against the live fleet (no API key)
node polyvers/bin/polyvers.mjs check --old machines/v1 --new machines/v2 --snapshots archive/

# run it durably, and keep checking it in production (no API key)
node polyrun/bin/polyrun.mjs deploy        --config polyrun.config.mjs
node polyrun/bin/polyrun.mjs check-product --config polyrun.config.mjs --parent order \
  --invariants invariants.compose.mjs
node polyrun/bin/polyrun.mjs audit         --config polyrun.config.mjs

polygen writes everything to <out>/: contract.json, next.cjs (the
module), invariants.mjs, traces/*.ndjson, and polygen-report.md. The
handoff after a polygen run is deliberately manual: review the contract and
invariants (they're the model's reading of your intent, not ground truth),
wire the module into your real handler — call it, don't reimplement it — then
run /polygraph:verify against traces captured from the integrated code.
That last step catches drift between the pure model and the glue around it.

Models

There is no default model — pass --model. Recommended: opus-5 or
better — deriving a faithful transition-function spec is a hard reasoning task,
and lighter models (e.g. sonnet-5) are not powerful enough for it.

The recommendation is per-step (RECOMMENDED_MODELS in scripts/models.mjs;
full analysis in docs/opus5_consolidated_report.md).
The split from the 2026-07-24 study: on reading code, opus-5 beat fable-5
outright at half the price; on one-shot formal authoring with no retry,
fable-5 was ahead — and the gap closes as soon as a repair loop feeds
checker errors back.

opus-5 measured on the 8-machine A/B (eval/ab-v2.mjs, 2026-07-24, n=3):
5/5 seeded bugs detected, 0 false alarms, 0 dead specs — all five detections at
the model-check tier rather than the cheaper replay tier, so budget for the
exhaustive pass. One caveat, seen only on the legacy bare-next prompt: the API
refused two of the eight machines (stop_reason: refusal, category: cyber)
because their source comments describe a payment-guard bypass. opus-4.8 and
sonnet-5 did not refuse the same input, and the default v2 prompt was
unaffected — but if a refusal costs you a run, that is the fallback to reach
for.

Anything not in the alias table (scripts/models.mjs) is passed to the API
verbatim, so an exact Anthropic model id always works. Reasoning models spend
output tokens on thinking before the answer; if you lower --max-tokens from
the default 32000 and see empty specs (stop_reason: max_tokens), raise it
back.

Examples

• Quickstart — the turnstile (examples/turnstile-v2/, no API key):
  npm test validates the corpus and runs the positive/negative controls;
  npm run verify:turnstile-v2 replays the bundled specs.
• Production case study (examples/case-study-subscription.md): a real
  end-to-end run on a closed-source SaaS billing machine that corroborated a
  genuine double-charge bug — plus an honest look at the risks the method
  can't see (external-service boundaries).
• polygen — OTP flow (examples/polygen-otp/): authored from one
  sentence; 8 states, 0 violations, a 134-window synthesized corpus, 0
  independent-replay failures.
• polygen — cart checkout, and a bug polygen found in itself
  (examples/polygen-cart-checkout/, narrated in
  examples/case-study-polygen-domain-gap.md): the contract/code vocabulary
  mismatch that motivated the domain cross-check, including a false positive
  the fix introduces.
• TLC tier reference (examples/etcd-raft-v2/): a v2 spec + invariants
  exercising the TLA+ escalation.

Layout

.claude-plugin/plugin.json   plugin manifest
skills/                      the methods, as instructions Claude follows:
                             polygraph (audit), polygen (author),
                             polyvers (version), polynv (elicit)
commands/                    /polygraph:verify, :polygen, :polyvers, :polynv
agents/                      polygraph-verifier, polygen, polyvers, polynv subagents
scripts/                     the shared core: sam-tv.mjs (replayer),
                             check.mjs (model checker), to-tla.mjs +
                             tla-check.mjs (TLC tier), verify, generate,
                             polygen, validate_corpus, models,
                             vendor/sam-pattern.cjs, instrument/*
polyrun/                     durable execution engine (README.md)
polyvers/                    versioning engine (README.md)
polynv/                      invariants-elicitation engine (README.md)
templates/                   contract.schema.json + contract.example.json
examples/                    worked examples and case studies (see above)
eval/                        the seeded-bug A/B eval and findings
test/                        npm test — no API key needed

Engine introductions: docs/polygen.md ·
polyrun/README.md ·
polyvers/README.md ·
polynv/README.md. The audit engine (Polygraph
itself) is this document.

Origin

The method is introduced in:

Jean-Jacques Dubray. Can Code Specify a System Precisely Enough to Formally
Verify It? arXiv:2607.05076, July 2026. https://arxiv.org/abs/2607.05076

The 2.0 release gate: a seeded-bug A/B eval passing at parity or better at two
model tiers, with two bugs newly caught at the cheap replay tier and zero dead
specs.

Where we actually stand on SysMoBench

SysMoBench (v3, January 2026) grades a generated
specification in four phases, the decisive one replaying execution traces
captured from the running system. Three things worth stating plainly:

• Polygraph has no published SysMoBench bug-finding score. Our work on the
  benchmark — Executable JavaScript as a Checkable Specification Language: A
  JS-SAM Case Study on SysMoBench (arXiv:2607.13092)
  — is a controlled language/contract comparison that adds JS-SAM as the
  benchmark's first non-formal backend. It is not a bug-finding result and
  should not be read as one.
• Specula reports 100% on all four phases (syntax, runtime correctness,
  conformance, invariant satisfaction), against 81–82% for unaided agent
  baselines. That is the number to beat, and we have not beaten it. In
  fairness to the reader on both sides of the ledger: SysMoBench and Specula
  share eight of Specula's nine authors, so that figure is a self-evaluation
  on the team's own benchmark — just as SysMoBench-1 below is our own fork.
  Neither fact is disqualifying; both should be visible.
• Our JS-SAM finding is why the SAM v2 strict profile looks the way it
  does: conformance against the real system is the only phase that
  discriminates among models, and once the comparison is drawn like for like
  it is the specification contract, not the language, that governs
  fidelity — JavaScript in the shape of the TLA+ transition relation is as
  faithful as TLA+. Both projects converge on the same place from opposite
  directions; Specula got there with an agentic repair loop, we got there by
  constraining the contract.

https://github.com/jdubray/SysMoBench-1 is our own fork, not an
independent evaluation of Polygraph.

Related work: Emilie Ma,
Scaling formal methods with LLMs
(Berlin Buzzwords), which presents SysMoBench and Specula together and
reaches the same conclusion from the formal-methods side: model checking plus
trace validation is what makes LLM-generated specs trustworthy.

If you use Polygraph in your work, please cite the paper (see CITATION.cff).

Polygraph 1.x derived a bare next(state, action, data) function instead of
the strict SAM v2 module. That pipeline remains available end-to-end behind
--legacy-bare-next for one release (npm run test:legacy,
npm run verify:turnstile). The v2 strict profile replaced it because it
closes whole failure classes by construction — silent no-op specs, hidden
bookkeeping state, vacuous exploration — while the N-spec voting layer absorbs
what v2 gives up. The one discipline sentence the study showed carried
bare-next's replay robustness is kept verbatim in the v2 prompts. (The repo's
historical disk name, bare-next-verify, records this lineage.)

License

Apache-2.0 — see LICENSE.