Versioning & live migration

Durable workflows outlive their code. An execution started under version 3 may still be running when you ship version 7, and replay only works if the code that resumes it agrees, event for event, with the code that recorded its history. Every durable execution engine has to answer the same question: what happens to the executions already in flight when the code changes?

The industry-standard answer is marker-based patching: branch in the code (if patched("my-change") { … }), let old histories take the old branch, and hope nobody ever has to read that code again. It works, but the translation from old behavior to new is invisible, unchecked, and impossible to compose. Hopskip’s versioning model is [experimental]: the checkable core is a pure library (hopskip-versioning), coupled to the engine through hopskip-versioning-bridge and driven by the hop migration CLI. It replaces marker patching with an explicit artifact: the patch.

Two questions, kept separate

A version change raises two independent questions, and the model keeps them apart.

1. Behavior compatibility. Does the new code, replaying an old execution’s history, issue the same commands the old code did? This is checked by shadow replay: run the new code against the recorded history and compare every issued batch of commands with the recorded one, by command id, over decoded payload values, never over bytes. The result is either “compatible” or the exact index of the first divergence with a diff of the batch (which command ids are missing, extra, or changed).

2. Data compatibility. Do the recorded events of an old execution translate into events the new version understands? Every version publishes an event graph: its event types and the derivations between them. Every patch carries a mapping from the old graph to the new one. Migration copies each recorded event across the mapping, fills in what the new graph requires, and computes each new value from old data (a backfill) or leaves it blank for old runs (a placeholder), exactly as the patch declares.

A patch is the pair: a mapping for the data plus a replay plan for the behavior, tied together by a per-execution replay check that runs at migration time no matter how much confidence the patch earned beforehand.

Certification: what is known before you touch a fleet

Patches are written as a list of plain verbs: rename this event, retype that payload, add this event backfilled from old data, split one command into two. Each verb carries a static check, and a patch built entirely from verbs whose checks pass is Certified. The engine knows before migrating anything that the translation is well-formed and total.

Changes that don’t decompose into the verbs are not rejected; they downgrade. CorpusTested means the patch passed shadow replay against a corpus of recorded histories. Unchecked means registration was allowed and fleet migration requires an operator override. The checker never dead-ends: it tells you which evidence path is still open.

Plan, then apply

Migration follows the plan/apply idiom. A dry run partitions the selected fleet before anything changes:

• migratable: every check passes.
• needs backfill for X: a value of type X cannot be computed for these executions; register a backfill and re-plan.
• diverges at event N: the new code replays these histories differently; the report carries the batch diff.
• must be replaced: the execution sits at a point the patch cannot cross (for example, mid-way through a command being split in two).
• blocked: with the precise reason.

Nothing migrates that a plan did not show. Failures are never a generic “nondeterminism detected”. Every error names the execution, the event types, and the history positions involved, and comes with a fix menu:

execution ord-8841 cannot migrate to billing@4:
  RiskCheck has no value between ChargeCmd#4 and AuthResult#4
  fix: add a backfill for RiskCheck
       or: exclude executions started before 2026-07-01 from this rollout

Exact rollback, with a tracked window

After migrating an execution, the engine tracks whether rolling it back to the old version would restore it exactly. The window opens if the patch loses nothing (no merged events, no unarchived drops), and it stays open while every newly appended event still has a place in the old version’s event graph. The first event that doesn’t, say the first occurrence of a brand-new event type, closes the window permanently and is recorded as the point of no return: “rollback expired at event N”. While the window is open, rollback is exact; after it closes, rollback requires a separately registered reverse patch or is refused.

The window is only one of two conditions, because a rollback is itself a deploy. Rolling back to the old version resumes speaking the old form on every contract the workflow participates in, including its own callers. If a counterparty has already upgraded past you, rolling back is allowed only when the resulting old-you/new-them pair can still communicate. When it can’t, the refusal says so and names the recovery order: roll the counterparty back first, or go forward through a reverse patch. (This rule was found by model-checking the migration machinery’s swap protocol, not by intuition; the checker enforces it in both the per-execution rollback gate and plan validation.)

Format changes are free

Every stored payload is tagged with its meaning (a semantic type) and its wire format (a codec), and the two evolve independently. A codec change, JSON to a binary format say, touches no meaning, so it needs no replay plan and no shadow replay: its entire check is that every stored payload still parses. Histories with mixed formats are normal; the tag on each event, not the current version, says how to read it.

This split is also the adoption path for existing untyped workflows. The first patch for a legacy workflow type is a typing patch that assigns a type and codec to every payload position, and its dry run partitions the fleet by exactly one question: does every recorded payload parse?

Deploy order across services

When two services talk, through signals, child workflows, or just launching and awaiting each other, their versions form a grid, and upgrading them is a path through it. For each pair of changes, the checker classifies the mixed states: either order is safe, deploy A before B, deploy B before A, or these two must cut over together (or add a shim). Plan validation walks your rollout order through the grid and reports the first step that strands a mixed pair, with the reordering or shim that repairs it. Changing a workflow’s input or output type is the same machinery: whether callers or the workflow upgrade first is read off which conversion functions the patch carries.

Where the guarantees come from

The model’s guarantees are not aspirational: the checker’s core is machine-checked (Rocq proofs in verification/rocq/), the engine’s swap protocol is model-checked (TLA+ models in docs/tla/, chaos-tested by Jepsen), and the production kernel is diffed against the extracted proofs in CI. The patch guide tells that story with the repo artifacts. The formal account behind the vocabulary on this page lives in one place, the theory appendix, and is deliberately absent everywhere else.