Patching workflows

Workflows are durable, so they outlive their code: you will ship version 4 while runs started under version 3 are still going. This guide shows how to move those runs to the new version with hop migration, how to preview the change before anything moves, and how the checks are verified. Authoring the patch itself (the Rust API, verb by verb) is covered in Writing migrations.

When you need a patch

Not every code change needs one. hop deploy diffs the new build’s control-flow graph against the old one and blocks changes that would break in-flight runs; for compatible changes, that gate is enough (see Compatibility & versioning).

Use a patch when the change breaks replay and you want existing runs to move across anyway:

an event type is renamed, or its payload changes shape or meaning
a new piece of derived data should exist for old runs too
two commands should have been one, or one should have been two
the workflow’s input or output type changes while callers are live

A wire-format change with no meaning change is also a patch, but a trivial one: it applies without a replay check and rolls back exactly.

How a patch works

A patch is a list of named changes (rename this, convert that, add this computed from old data) plus the functions those changes refer to. You do not write the workflow’s event graph; it is derived from the workflow’s signature.

Every change has a built-in check, and the checks run before anything touches a real execution. Before applying, you dry-run the patch against the live fleet and get a per-execution report: which runs can move, which need a backfill from you, which disagree with the new code, and which must be replaced rather than updated. Apply then moves one run at a time, re-verifying each against the new code before it switches. Runs that fail a check stay on the old version and keep running.

Quickstart

# 1. Serve the migration API (loopback; it is an operator surface).
export HOPSKIP_VERSIONING_API_BIND=127.0.0.1:8091
hopskip-server

# 2. Adopt the workflow type: register its current shape as version 1.
hop migration adopt billing --version 1

# 3. Register the new version's manifest and the patch from old to new.
hop migration register-version billing-v4.json
hop migration register-patch  billing-4.json

# 4. Register the new version's code, so each run can be replayed
#    against it before switching.
hop migration register-artifact billing 4 target/module.wasm

# 5. Preview, then apply.
hop migration dry-run billing-4
hop migration apply   billing-4

The patch files in steps 3 and 4 come from the authoring step in Writing a patch. Every command is one HTTP call to the loopback API; the CLI renders the server’s reports and relays refusals without adding judgment of its own.

Where patches run

Surface	What it is	Use it when
`hop migration`	the CLI above	driving a rollout
The versioning HTTP API	the same routes, served by `hopskip-server` (`HOPSKIP_VERSIONING_API_BIND`) or the standalone `versioning-api-dev` over a data-directory copy	scripts, the console’s Migrations page
The `hopskip-versioning` Rust crate	the library where patches are authored and checked	generating patches programmatically
Migration as a workflow	`sdk/rust/migration-workflow` + `migration-worker`	large fleets

The command surface is pre-GA and may change. There is no separate migration-file language: patches are authored with the Rust library and driven with the CLI.

Running a migration

Start the migration API

export HOPSKIP_VERSIONING_API_BIND=127.0.0.1:8091
hopskip-server        # or: versioning-api-dev <data-dir>

Mounted in the server, a dry run partitions the fleet the engine is actually running, and an apply commits into the same log partition the next replay reads. The surface has no authentication today; bind it to loopback.

Adopt the workflow type

hop migration adopt billing --version 1

Existing workflows decode their own payloads, which makes their recorded histories opaque to every check. Adoption derives the starting version from the recorded fleet itself. (Equivalent HTTP route: POST /versions/legacy.)

Register the version and the patch

hop migration register-version billing-v4.json
hop migration register-patch  billing-4.json

Both are JSON manifests produced by the authoring step. Registration validates them again, statically: a manifest that disagrees with itself, or names a function nobody registered, is refused here rather than mid-rollout.

Register the target code

hop migration register-artifact billing 4 target/module.wasm

A patch that changes meaning replays the new code against each translated history before switching that run, so the service needs the new code. The module is built like any guest module. The upload is loaded before the call answers, so a broken module fails here, not later. Until the target’s code is registered, apply returns 409 with that reason.

Dry-run

hop migration dry-run billing-4

The dry run performs every step of the migration except the final switch, for every execution, and writes nothing. Each execution lands in one bucket:

Bucket	Meaning	What to do
ready	every check passed	nothing; apply covers these
needs a backfill	a new event type has no value for these runs and no computation is registered	register the backfill, dry-run again
diverges	replaying the new code against the translated history disagreed with the record, at a named position	see Debugging a divergence
paused at a rewrite point	the run sits exactly where a structural change (split, reorder) rewrites the plan	fork it; it cannot be updated in place
blocked	a named check refused, with the reason and a fix	follow the message

The console’s Migrations page renders the same report as a graph: version chains per service, each patch’s changes on the event graph, the fleet partition, and the rollout-order verdict.

Apply

hop migration apply billing-4

Apply commits one switch per execution. Each switch is confirmed by re-reading the log before it is acknowledged. A run that appended something in the race window reads back refused stale: nothing happened to it; re-run when quiet. Runs that cannot migrate stay on the old version, listed and running. Apply only touches executions the dry run reported.

Roll back

hop migration rollback orders:billing:019a...
# with counterparties upgraded past you: --standings standings.json

Every migrated run carries a rollback status. The window starts exact (rolling back restores the pre-migration state precisely) when the patch lost nothing, and it stays open until the first appended event that has no place in the old version. From that point, rollback requires a registered reverse patch.

Rollback is itself a deploy step: if another service has upgraded past you, the old version must still be able to talk to it, or the rollback is refused with the required recovery order (roll them back first, or go forward through a reverse patch). Model checking of the commit protocol produced this rule.

Migrating a large fleet

For chunked progress, retries, and triage, run the migration itself as a workflow on the engine. Build and deploy sdk/rust/migration-workflow, run sdk/rust/migration-worker, and start it like any workflow:

hop run hopskip:versioning.migrate@1 --input '{"patch":"billing-4","chunk":100}'

Each chunk’s report lands in that run’s own history, and the aggregated fleet summary is its durable result. A re-dispatched chunk is safe: a run that already migrated reads back as wrong-version, a no-op, never a second switch.

Writing a patch

A patch has three inputs: the verbs (one per change), the functions they refer to (payload conversions and backfills, registered by name), and the target version’s code. You never write the event graph; it is derived from the workflow’s signature. The full verb-by-verb reference, with the check each verb carries and the failure messages, is in Writing migrations. In outline:

use hopskip_versioning::combinator::{CombinatorStep, elaborate};
use hopskip_versioning::patch::VersionId;
use hopskip_versioning::schema::TypeName;

let steps = vec![
    CombinatorStep::RenameEvent {
        old: TypeName::new("PaymentCmd"),
        new: TypeName::new("ChargeCmd"),
    },
    // ...more steps
];

let elab = elaborate(
    "billing-4",
    VersionId::new("billing", 3),
    VersionId::new("billing", 4),
    &from_manifest.schema,
    &from_manifest.signature,
    &steps,
    &regs,
)?;
// elab.manifest: the certified patch, ready to register

If a change does not decompose into verbs, it is not rejected; it is registered at a lower certification level (corpus-tested or unchecked) and the per-execution check at apply time still runs.

Errors

Every refusal states what failed, where, and at least one fix:

execution ord-8841 cannot migrate to billing v4:
  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

Deploy order across services

If your workflow talks to another service, or you changed its input or output type, validate the rollout order before deploying anything:

curl -X POST $VAPI/plans/validate -d @rollout.json

The checker answers with one of four sentences per service pair: either order is safe, deploy A before B, deploy B before A, or these two must cut over together (or add a conversion so mixed versions can talk). The request format and the full walkthrough are in Writing migrations.

How this machinery is proven correct

The checking machinery is itself checked: its core algorithms are proven with machine-checked proofs, the commit protocol was model-checked for races and then fault-injected on a real system, and the production code is continuously diffed against the extracted proofs in CI. The argument, including every assumption it rests on, is written down and frozen.

The claim, in plain words: after every operation the engine performs (delivering an event, crashing and resuming, migrating, rolling back, re-encoding), replaying a run’s recorded history reproduces it exactly, with the same work in flight. Ten theorems state that each operation preserves this: that rollback through an open window restores the pre-migration state exactly, that no command is resolved twice under any interleaving, that a certified patch migrates everything the verbs promise, that format-only changes are inert, and that a validated deploy order never leaves two services unable to talk.

Instrument	What it is	What it gives you
Rocq proofs (`verification/rocq/`)	machine-checked theorems	replay, migration, rollback, and linearity guarantees; termination proofs for the core algorithms; every verb’s built-in check; the deploy-order calculus
TLC model checking (`docs/tla/`)	exhaustive small-world protocol check	the commit protocol has no race, including a crash mid-migration. Two enforced rules came out of this lane: a rollback is a deploy, and order gates are checked at commit time
Jepsen fault injection (`jepsen/hopskip`, `--workload versioning`)	the real system under real faults	kill -9 mid-apply and mid-rollback over a real disk store, restart over what survived: every acknowledged migration held, and a wipe control proves the checker can see the loss it hunts
Property and differential tests (`core/hopskip-versioning/tests/`)	sampled runs against the real Rust, and the Rust diffed against the extracted proofs	every certified patch is accepted by the proofs’ own checker, so code and proofs cannot drift; a mutation probe corrupts certified patches and confirms nothing escapes

The proofs rest on four assumptions, each discharged separately: storage’s atomic write (bridged by the model checking and exercised by Jepsen), codec round-trip laws beyond the samples (property-tested, not proven), workflow determinism (enforced by the sandbox), and production code agreeing with the proofs (the differential CI lane above). Everything else is a theorem.

The theorem inventory is versioned (MT-1); every patch manifest records the version it was certified under, and registration refuses one stamped with an unknown version. CI gates releases on the proofs compiling, the protocol models passing, and the differential and property suites staying green.

Status: mechanized and in CI today are the path-equality core, the carry-forward loop, the behavior-layer theorems, every verb’s data check, and the deploy-order calculus, plus the commit protocol under TLC and Jepsen. Remaining, tracked as explicit completion gates: extending the mechanization from its models to arbitrary production artifacts end to end, and widening the differential lane to the full checker. Where this page and the mechanization disagree, the mechanization wins.

The mathematical account behind this summary lives in one appendix: the theory behind versioning.