Polygraph – Now your tests can't lie Polygraph, a new Claude Code plugin and standalone CLI, uses LLMs to automatically generate formal models of stateful JavaScript code and exhaustively check for bugs, finding violations like double charges that unit tests miss. In a production subscription-billing system, it independently corroborated a genuine double-charge bug and found all 5 seeded bugs in a controlled eval where replay alone found none. The tool aims to make formal verification practical by having an LLM produce and update the model on every code change, keeping developers in JavaScript. 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 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 isexperimental, not peer-reviewed, unproven technology.It is aconsistency check, not a proof: a clean run means the code's observable behavior matches an independent reading of its own source, and nothing more. Every finding is alead to investigate by hand, not an established result. Do not rely on it as your only safeguard for correctness- or safety-critical code. 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 relevant payload, visits every reachable state, 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 /jdubray/polygraph/blob/main/examples/case-study-subscription.md . In the controlled eval, replay alone found 0/5 seeded bugs — model checking found 5/5, with counterexamples . /jdubray/polygraph/blob/main/eval/FINDING-faithful-reproduction.md eval/FINDING-faithful-reproduction.md 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. Emilie Ma's Berlin Buzzwords talk Scaling formal methods with LLMs https://www.youtube.com/watch?v=M2wb2ug2gYg presents the same thesis from the TLA+ side: SysMoBench, a benchmark showing frontier LLMs can't yet write conformant specs unaided, and Specula, an agentic pipeline spec generation + model checking + trace validation — the same three legs Polygraph stands on that found 160+ bugs in production systems like MongoDB and etcd-raft, over 130 previously unknown, at roughly $40 per repository. The convergent finding: the LLM alone is not trustworthy, but an LLM held accountable by a model checker and trace validation is a practical bug-finder. Everything revolves around three artifacts you can read and diff: - 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. - 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 https://sam.js.org 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. - 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. 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 /jdubray/polygraph/blob/main/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. | step | who does it | how long | |---|---|---| | Define the contract observable fields, actions, terminals | you, or Claude drafts it for your review | minutes | | Capture traces instrument a copy, drive scenarios | the agent, in Claude Code — it builds test doubles/emulators if needed; standalone, you wrap your dispatch once snippet below | the bulk of the work standalone; delegated in Claude Code | | Write invariants your rules as JS predicates | you — this is your intent; the tool can propose, only you can confirm | minutes per rule | | Generate specs, replay, model-check | automatic | minutes | | Triage findings | you — every finding is a lead, not a verdict | depends on what it finds | 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: js import { withTracing } from '