A Polygraph engine

polyrun — durable execution for verified machines

A verified state machine that loses state on a crash, or fires the same effect twice on a retry, is verified in theory and unreliable in production. polyrun closes that gap: one commit per step, effects emitted exactly once, and a composition gate that checks the check-then-effect sequence itself.

When you reach for it

A verified machine still has to survive a crash mid-step and a retry that would fire the same effect twice. Correct on paper is not the same as reliable in production.

What you have when it finishes

One commit per step, every effect emitted exactly once, and a journal that feeds the verification gates back — so the machine keeps being checked after it ships.

The pipeline

What goes in, the stages it runs, what it leaves behind. Step through the stages to trace the run.

fig 9

polyrun

run a verified machine durably — and keep checking it

Snapshot durability, not event-sourced replay: no determinism sandbox, no patch() versioning, one ACID transaction per step.

execute

Dispatch

API calls, signals, durable timers and effect completions all arrive as one kind of thing: an action on an instance.

→

Kernel step

Rehydrate with init()+setState(), step the module, classify the result. Dedupe read included in the same transaction.

→

Commit

Journal row, snapshot, effect intents and timers commit together or not at all.

→

Effects

Emitted exactly once, executed at least once under idempotency keys. Workers hold leases, retry, and dead-letter; completions dispatch before row marks on every path.

→

fail loud

Poison

Anything that “cannot happen” for a verified module — a mid-step throw, an unreadable classification, a rejected snapshot — durably poisons that instance.

→

Keep checking

check-effects explores machine ∘ mapper, check-product the joint parent×child space, simulate drives the real kernel on seeded faulty schedules, audit replays production.

consumes

next.cjs · contract.json · effects.cjs + manifest · actions, signals, timers

produces

journal (= the audit trace corpus) · fleet snapshots (= the versioning gate’s initial states)

Rejection is a legal, observable no-op — which is what makes stale timers, duplicate webhooks and at-least-once redelivery safe with no cancellation machinery.

How it works

Correctness that survives a crash, not just a proof.

One commit per step

Every transition is durably recorded before its effect runs, so a crash mid-step never leaves the machine in an undefined state.

Effects emitted once

Retries replay the state, not the side effect; an email sent once stays sent once, even across a restart.

Check-effects composition gate

The gate verifies not just that the machine is correct, but that checking and acting are properly sequenced — closing a class of bug verification alone doesn't catch.

Fits with: Executes what polygen authors and what polygraph or polyvers cleared to ship.