Polygraph 2.1.0 — polyrun, the OMS trilogy, and the pipeline gates
The headline: a new component and two capstone examples that take Temporal's OMS reference application full circle — reimplemented on verified machines, then audited in its original Go form.
polyrun — durable execution for verified machines
A durable-execution harness for polygen-authored SAM v2 strict-profile machines (spec: docs/polyrun-spec.md, code: polyrun/):
- Snapshot-based durability — no event-sourced replay, no determinism sandbox, no
patch()versioning; deploys are gated mechanically over live snapshots (polyrun deploy), including a model check using production states as initial states - One-transaction dispatch with actionId dedupe; transactional outbox with idempotency keys, leases, retries, DLQ +
onExhausted; durable timers whose staleness resolves as verifiedreject(reason) - SQLite and Postgres adapters (the full suite runs against both), standalone worker, HTTP facade + read-only ops console
- First-class parent/child machines (spawn/signal/completion/cancel-on-parent-terminal) and post-commit journal fan-out — and the journal is a Polygraph trace corpus (
polyrun auditreplays production against the model, version-aware) polyrun check-effects: exhaustive exploration of the machine ∘ effect-mapper composition against emission invariants ("no reachable path emits chargeCard twice", "spawns exactly N children")- Migration (
migrate.cjs: pure, two-phase, fenced,$migrate-journaled) and archival tooling - Every milestone (M0–M3) shipped through adversarial multi-agent review; all confirmed findings fixed. 60+ tests green on both stores; the kill -9 mid-charge demo recovers with exactly one charge
The OMS trilogy
examples/polyrun-oms— Temporal's order-management reference app rebuilt on polyrun: multi-fulfillment orders splitting into shipment children with a completion rollup, amend-with-timeout, idempotent billing, a User/Courier storefront. Every machine is polygen-authored from a pinned contract and model-checked before first run (one recorded hand-repair, honestly documented inmachines/order/REPAIR-NOTE.md).examples/polygraph-oms-go— both workflows of the reference app audited in their original Go: ground-truth traces from the unmodified code via Temporal's own testsuite (no server), positive/negative controls, three independently LLM-generated specs per workflow (27/27 and 21/21 replay), and unanimous model-check verdicts with shortest counterexamples. Findings, framed as intent observations rather than bug reports: an all-unavailable amended order completes with nothing fulfilled or charged; partial failure reports as plain success; carrier status is applied verbatim (any string, free regression). The negative control for the shipment audit is itself the finding: a spec of the documented behavior fails replay against the real code.
polygen pipeline hardening
- Object-aware domain-gap heuristic (object-valued
dataDomainentries are checked by their scalar leaves — no more permanently-unsatisfiable false positives) - Dead-at-init gate: a module that validates strict-clean but rejects every action from its initial state is refused with a diagnosis (catches the
name:-component local-state binding), fed back into the authoring retry
Documentation
docs/ARCHITECTURE.md (three engines, one artifact family), docs/SDLC.md (team lifecycle for agentic workflows, incl. versioning best practices), docs/VERSIONING.md (an essay on state-machine compatibility), docs/polyrun-spec.md.
Full details in CHANGELOG.md. Plugin users: /plugin marketplace update polygraph, then start a fresh session.
Same disclosure as always: Polygraph is experimental, and a consistency check, not a proof — every finding is a lead to investigate by hand.