A polygraph for your state machine: an LLM derives a formal model from your code, then Polygraph replays real traces against it and exhaustively model-checks it against your invariants.
Command
Run polygen — draft a contract from a feature description, author a verifiable SAM v2 strict-profile module against it, self-repair against reachable invariant violations, and synthesize a demo/regression trace corpus.
Command
Run polynv — elicit the invariants for a state machine. Harvest candidates from the contract's vocabulary, traces, and fleet snapshots; contribute frontier-model domain priors; pre-check every candidate (HOLDS or a concrete counterexample); drive a plugin-led interview into an append-only intent ledger; grade…
Command
Run polyvers — classify a state-machine version change into compatibility lanes, run the gates those lanes require against fleet snapshots (shape round-trip, vocabulary, in-flight stimuli, migration validation, seeded model check), scaffold migrations, and check parent×child version matrices. No API key.
Command
Run the Polygraph verification loop — generate N transition-function specs from a source file and replay real traces against them, reporting spec-errors vs code-findings.
Command
Build a feature as a workflow, not an agentic loop — design stages/signals/budgets with the user, front-load contract + invariants, author with polygen, declare effects, prove the anti-loop rules with check-effects, and stand it up under polyrun.
Command
Render Polygraph verification artifacts as deterministic diagrams (SVG, optional PNG). Renders a fixed catalog — state-machine, invariants, counterexample, compat-gate, model-card — from a viz-model JSON or straight from a Polygraph/polyvers artifacts directory. Byte-identical output; no model call at render time.