1 Introduction↩︎

Durable execution frameworks—Temporal [1], Azure Durable Functions [2], and more recently the Workflow SDK [3]—let developers express long-running, stateful processes as ordinary code. The engine persists an append-only log of events (step invocations, results, timers, external signals); when a process must resume after a crash, a suspension, or a redeployment, the engine re-executes the orchestration function from the beginning and substitutes recorded results for completed steps. Correctness of this replay rests on a determinism contract: given the same event history, the orchestration code must make the same decisions.

The contract has a corollary that is under-examined in both literature and practice: the event log is only meaningful relative to the code that produced it. When version \(V_2\) of a workflow is deployed while runs started under \(V_1\) are still in flight, three distinct failure modes arise:

1. Replay divergence. \(V_2\) reaches a different step than the log expects (a step was inserted, removed, or reordered). Depending on the engine this manifests as a hard nondeterminism error or—worse—as a silently mismatched result substitution.

2. Rehydration failure. The recorded payload of a completed step no longer satisfies the shape that \(V_2\)’s downstream code consumes (a field was removed, renamed, or its type narrowed).

3. Behavioral drift. Replay succeeds, but steps not yet executed behave differently under \(V_2\); the run completes with semantics neither version’s author intended.

The state of the art is operational, not analytical. Temporal offers worker versioning and an explicit patched() API [4] that gates code paths on a run’s provenance; platform-level skew protection pins runs to the deployment that created them and drains old versions. These mechanisms are sound but uniformly pessimistic: they assume every change is incompatible with every in-flight run. For short-lived runs the cost is idle capacity; for workflows that legitimately sleep for months—subscription lifecycles, compliance timers, drip campaigns—pessimism means a critical bug fix cannot reach a stranded run at all.

This paper develops the missing analytical layer. We ask: given the diff between \(V_1\) and \(V_2\) and the telemetry the protocol already persists, what is the probability that upgrading a given in-flight run fails, and how does that risk aggregate over the fleet? Our central observation is that event-sourced workflow engines are an unusually favorable setting for change-risk inference. In a general distributed system, risk models must infer interaction patterns from sampled traces; here, the protocol persists complete histories—every path ever taken, every payload ever produced—as a byproduct of its durability guarantee. Consequently the backward-looking component of upgrade risk can be computed exactly, and only the forward-looking component requires probabilistic estimation.

1.0.0.1 Contributions.

1. A formal model of the durable-workflow protocol (event log, replay relation, determinism contract) sufficient to state upgrade compatibility precisely (§3).

2. A three-axis change taxonomy—protocol, interface, migration—with per-node incompatibility functions computable from the static diff and payload telemetry (§4).

3. The \(\mathrm{WUR}\) risk model: an exact backward term over recorded prefixes and a forward term based on hitting probabilities in an empirically estimated absorbing Markov chain, composed by a noisy-or operator (§5).

4. A Bayesian estimation procedure with credible intervals, using Dirichlet posteriors on transitions and Beta posteriors on payload compatibility, pooled across axes by confidence-weighted log-odds (§6).

5. Soundness and monotonicity results: \(R_{\mathrm{b}}(r)=0\) under conservative matching certifies safe rehydration of run \(r\); a differential-demand lemma confining contract inference to changed consumer slices; and a canonical-form procedure deciding prefix validity modulo trace equivalence of concurrent completions in \(O(L \log L)\) (§7).

6. An \(O(|\Delta|\cdot|\theta|_{\max}\cdot|\mathcal{R}| + |N|^3)\) algorithm and a threshold policy that partitions the fleet into migrate/review/pin classes with expected-loss ranking (§8–9).

7. An inter-run coupling extension (§10): fleet risk as the least fixpoint of a failure-contagion operator on an empirically constructed coupling graph; mixed-version window risk scored by the interface machinery applied across channels and weighted by logged event rates; and an exact coupling-aware migrate/pin partition via \(s\)–\(t\) minimum cut.

These contributions form three deliberate layers, each consuming the previous one’s output and nothing else: a certification layer (§3–7) that decides, per run, what recorded history already proves; a risk layer (§5–9) that quantifies what history can only make probable; and an operations layer (§10) that turns per-run verdicts into a fleet decision under coupling. A reader interested only in the certification result can stop after §7; an operator deploying the model needs all three, because per-run verdicts that ignore coupling recommend partitions that violate saga atomicity in the mixed-version window.

Everything in the model is world-agnostic: it consumes only the protocol surface (run listings, event logs, recorded payloads) and never touches a specific persistence backend or executes workflow code.

2 Related Work↩︎

2.0.0.1 Durable execution and versioning.

Temporal’s versioning facilities [4] (patch markers, worker build IDs, deployment-based routing) and platform-level skew protection are mechanisms for avoiding incompatible replay; they provide no measure of whether a given change is in fact incompatible, and default to pinning. Azure Durable Functions documents versioning as a set of manual strategies [2]. Our model is complementary: it supplies the decision function that these mechanisms lack.

2.0.0.2 Event sourcing and schema evolution.

Event-sourced systems [5] face upgrade problems for data: old events must remain readable by new code. Schema-evolution disciplines in serialization frameworks (Avro, Protocol Buffers) define compatibility lattices over record types [6]. We adopt the lattice view for the interface axis but extend the problem to control flow: in durable workflows the event log encodes not only data but the shape of a partially executed computation.

2.0.0.3 Change-risk prediction.

Defect- and risk-prediction models in software engineering estimate failure probability from change metrics (churn, coupling, history) [7]. These models are statistical over code artifacts and outcomes; they do not exploit an execution protocol. Our setting inverts the balance: the protocol’s determinism contract makes a large part of the risk computable rather than merely predictable.

2.0.0.4 Markov models of program behavior.

Using empirically estimated Markov chains to model control flow and compute reachability or hitting probabilities is classical [8], [9]. We apply the machinery to the step graph of a workflow, with the notable property that the training data (complete path histories) is exhaustive rather than sampled.

2.0.0.5 Energy minimization on graphs.

Exact MAP inference for binary pairwise Markov random fields via minimum cut is classical [10], [11]; multi-label extensions rely on move-making approximations [12]. We import this machinery for the coupling-aware migrate/pin partition, where submodularity of the pairwise terms holds by construction.

2.1 The Engine Landscape↩︎

The model is generic over durable execution engines, but genericity is earned per engine, not assumed: what varies is the site identity discipline that the matching \(\mu\) of Definition 7 must reproduce, the strength of the determinism contract (Assumption 1), and the telemetry surface (Assumption 2). Table 1 fixes these parameters for the engines we are aware of; the rest of the paper refers to this table rather than re-litigating engine differences at each use.

4pt

Three observations structure the comparison. First, the ordinal-identity family (Workflow SDK, Temporal, Azure Durable Functions, Restate) shares the strict discipline formalized in §3: any insertion, deletion, or reordering of sites ahead of recorded events is fatal, replay failures are hard errors, and the model applies with \(\mu\) as defined. It also shares pin-by-default versioning: Workflow SDK pins every run to the deployment that started it, and its versioning guide’s recovery procedure for buggy deployments—find the affected runs, cancel, rerun on the latest deployment—presupposes exactly the affected-run determination this model computes, while its deploymentId:"latest" escape hatch explicitly delegates the cross-deployment compatibility judgment to the developer. Restate’s documentation is the most explicit ancestor of our taxonomy, enumerating as unsafe exactly the reordering, insertion/removal, input-change, and conditional-logic changes that populate \(\Delta_\mathrm{P}\) and \(\Delta_\mathrm{I}\)—but, like Temporal’s pinned-versus-auto-upgrade choice and Durable Functions’ side-by-side guidance, it leaves the per-run decision to human judgment. These engines pay for safety with pin-by-default: old deployments must be kept alive until their pinned runs drain, with the forgone-fix exposure \(\beta_r\) of §9 accruing silently. Temporal’s patch API deserves its own sentence, since it is the most sophisticated native mechanism: patched() lets one worker serve both versions by branching in workflow code, which solves mixed-version execution but creates a new liability—patches accumulate, and knowing when a patch is removable requires knowing that no in-flight run can still traverse its old branch. That is a hitting probability on recorded frontiers, i.e., precisely the forward machinery of §5; the model answers “which runs force this patch to exist” with a number. Our model is, in general, the decision procedure these engines’ escape hatches presuppose.

Second, name-keyed identity (Cloudflare Workflows) trades strictness for tolerance: steps are memoized by name with an occurrence counter, so inserting or reordering differently named steps is tolerated where the ordinal family diverges—but a renamed step is a cache miss that silently re-executes, converting failure class F1 (hard divergence) into F2-like duplicated side effects whose severity is governed by idempotency, precisely the quantity §6.4 estimates from retry telemetry. The framework accommodates this by parameterizing \(\mu\): name-multiset matching with occurrence indices replaces ordinal preservation, \(\Delta_\mathrm{P}\) coarsens, and the severity axis does proportionally more work. A further difference widens \(\Delta_\mathrm{P}\) in the other direction: orchestrator code outside steps is re-executed rather than virtualized, so any change to it is protocol-relevant, not only changes at sites.

Third, definition-based execution (Step Functions) versions the state machine rather than replaying code: executions complete on the definition they started with, so backward risk trivializes (there is no rehydration of recorded state into new code) and the model reduces to its forward-risk and coupling components applied at the boundary between definition versions.

The remainder of the paper develops the model for the ordinal-identity discipline and verifies it against Workflow SDK as the reference instantiation; the parameterization above delimits what transfers elsewhere and at what cost.

3 System Model↩︎

We formalize the protocol implemented by Workflow SDK-class engines. The model is deliberately minimal; any engine satisfying Assumptions 1–2 is covered.

\(G_V\) is computable by static analysis of the orchestration function: the determinism contract confines control flow to a sandboxed subset of the language, which is precisely what makes the extraction tractable.

Figure 1 illustrates the identity discipline on a suspended run: the same recorded prefix replayed against two candidate versions, one insertion at the tail (harmless: every recorded event still meets the consumer holding its identifier) and one at the head (fatal: every subsequent ordinal shifts, so the first recorded event already meets a consumer with a different name).

3.1 Concurrency and Trace Equivalence↩︎

Structured concurrency complicates Definition 3: within a fork–join group the log records step completions in completion order, which is scheduling nondeterminism, not program semantics. Two logs differing only by such permutations denote the same computation, and prefix validity must not distinguish them.

Branch correspondence within a parallel group is accordingly positional, not label-based: \(\mu\) must preserve the fork’s branch invocation order, and a permuted branch list is classified into \(\Delta_\mathrm{P}\) even when a multiset comparison would succeed. The recorded completions of matched branches, by contrast, may appear in any log order.

Assumption 2 is not an idealization—it restates the durability guarantee. It is the reason this domain admits exact backward analysis where general distributed systems do not.

Like Assumption 2, this is less an idealization than a restatement of how these engines already work. Pin-by-default versioning requires immutable, retained deployments—the engine cannot replay a pinned run without the artifact that created it—so \(V_1\)’s code is guaranteed to exist at \(V_2\)’s decision time by the same mechanism the model serves; in git-based deploy flows, both versions additionally resolve to commits. Two practicalities matter. The diff must operate on the post-build representation, where module-qualified site names are assigned—diffing raw source with different naming rules than the runtime’s yields a different protocol view; the build tooling that assigns these names can equally enumerate them. And the diff’s scope is the full bundle closure: a dependency bump changes sites without touching first-party source, so changed modules are identified from the lockfile and the out-of-scope warning rule of §8 applies to anything the diff cannot see.

4 Change Taxonomy and Incompatibility Functions↩︎

Let \(V_1, V_2\) be the deployed and candidate versions, with step graphs \(G_1, G_2\).

Syntactic predicate comparison is conservative by design: semantic equivalence is undecidable, and Theorem 2 requires only that matching never equates sites or predicates that differ observably.

The lattice is defined over hydrated payloads, and that word is doing work: the reference implementation persists step results in a structured serialization (a flattened value array with numeric back-references and typed wrappers for Date, Map, Set, and cycles), so field presence is well-defined only after hydration, and an implementation computing presence frequencies over raw serialized bytes will be wrong. Typed wrappers sit outside the record lattice entirely: a demand reaching into a Map or Date internal receives verdict unk and the maximal-demand treatment of §4.1, since the lattice has nothing sound to say about their evolution. Both the exact and distributional regimes of §6 therefore include a hydration step; its cost is linear in payload size and is included in the measured per-run figures of §12.

Equation 2 is the pivotal substitution that removes the need for dry-run execution. Whether \(V_2\) can consume \(V_1\)’s recorded outputs is not a property of code paths that must be exercised; it is a measure-theoretic property of the observed payload distribution against a static contract. If a new consumption site destructures field \(x\), then \(\rho_\mathrm{I}= 1 - \mathrm{freq}_v(x)\); if it narrows a numeric domain, \(\rho_\mathrm{I}\) is the observed mass outside that domain. Two regimes are available:

• Distributional (aggregate): \(\Phi_v\) summarized as field-presence frequencies and value-domain histograms; \(\rho_\mathrm{I}\) is a fleet-level rate. Cheap; supports pre-deployment scoring.

• Exact (per-run): the actual payload \(x_{r,v}\) is validated against \(D_2\), collapsing \(\rho_\mathrm{I}\) to an indicator per run. Still purely static—data validated against a schema, no code executed.

4.1 Demand Inference and the Differential-Demand Lemma↩︎

The consumption contract \(D_2(v)\) is obtained from static types where the program supplies them and, in untyped code, by access-path abstract interpretation of the consumer slice of \(v\): the set of member accesses, destructuring patterns, comparison and arithmetic domains, and callee-signature flows reachable from the binding of \(v\)’s result. Contract verdicts are three-valued, \(x \vDash D \in \{\mathrm{\small sat}, \mathrm{\small vio}, \mathrm{\small unk}\}\): a demand the analysis cannot resolve (computed property access, reflective use) widens only the affected access path to unk. An unk verdict never enters Equation 4 as a certainty in either direction; it contributes a weak-prior Beta term for \(\rho_\mathrm{I}\) with low confidence, which under the pooling rule of §6.3 routes the affected runs toward review rather than silently toward migrate or pin.

Crucially, the inference burden is bounded by the diff, not the program:

Contract inference (and Assumption 5) is therefore required only at changed consumer slices—typically a handful of access paths per release—rather than across the codebase. Historical success is itself compatibility evidence wherever code did not change; the analyzer spends its precision budget exactly where the diff spends its risk. Per-site incompatibilities across axes are pooled into a single \(\rho(v)\) by the confidence-weighted operator of §6.3.

4.1.0.1 Demand satisfiability and the invocation gate.

One class of change escapes both the differential-demand lemma and per-site contract validation: the consumer slice is untouched, but its producer is deleted or moved after the consumer, so the demand edge is no longer satisfiable in \(V_2\)’s structure at all. The analysis therefore includes a static satisfiability check over \(V_2\): for every demand edge \((c, u)\), the producer \(u\) must lie in the certainly-preceding scope of \(c\) (preceding at top level, in the same parallel branch, or in the same conditional arm, together with everything preceding the enclosing construct). An unsatisfiable demand faults whenever its consumer is invoked, so the per-run question reduces to whether replay invokes \(c\); because the protocol may have changed, that gate must be evaluated against \(V_2\)’s structure, not the run’s recorded frontier: replay invokes \(c\) once every site certainly preceding \(c\) in \(V_2\) that \(V_1\) can produce has completed in the prefix. Both the rule and the gate were forced by the real-workflow corpus of §12, where producer deletions and demand-order inversions arise naturally (hook results consumed by later steps) and where a \(V_1\)-relative frontier misses consumers that a reordered \(V_2\) invokes first.

4.1.0.2 Dynamic access and inference limits.

Access-path abstract interpretation reads statically visible member accesses; JavaScript offers several ways to hide them: computed access (payload[fieldName]), reflective access (Reflect.get), deep-path helpers (lodash.get), re-serialization boundaries (JSON.parse of a stringified payload), and aliasing through intermediate collections. The design response is uniform: any consumer slice whose demand cannot be bounded statically receives verdict unk on the entire payload of each producer it can reach, which the risk model treats as maximal demand—conservative, never unsound, and it degrades precision only for the changed slices the differential-demand lemma routes to inference in the first place. Downstream, an unk verdict is not a silent worst case: it enters the pooling of §6.3 as a maximal-demand factor with minimal confidence, so its wide Beta posterior inflates the credible interval, and the interval-based policy of §9 routes the affected runs to review rather than to silent migration or blanket pinning—the class whose diagnosis names the offending consumer slice. The confidence attached to an unk factor is an operator-tunable prior with two meaningful endpoints: uninformative (wide posterior, routes to review—the default, since unknown is not broken) and degenerate-pessimistic (certain violation, routes to pin); one tested implementation of the analyzer ships the pessimistic endpoint, which is strictly safer and strictly more expensive, and both are conformant. Two things bound the damage in practice: unchanged slices never need inference at all (their certification is historical, §4.1), and unk verdicts are exactly the places where a one-line developer annotation (an explicit field list) restores precision; surfacing them in the per-release verdict explanation makes the annotation a review-time action rather than archaeology. The evaluation of §12 deliberately evaluates the risk model given demands rather than the inference front-end, which is language- and engine-specific; an empirical study of inference precision on production JavaScript is future work and is flagged as such rather than assumed away.

5 The Risk Model↩︎

Upgrade risk for a run decomposes into a backward component—can the recorded history rehydrate under \(V_2\)?—and a forward component—will the remainder of the run traverse changed code? The components differ in kind: backward incompatibility is corruption (state loss, divergence, stranding), forward exposure is behavioral (a fresh execution of intentionally changed code).

5.1 Backward (rehydration) risk↩︎

Two boundary conditions matter, and both were surfaced by the synthetic evaluation of §12 before being incorporated here. First, the interface product ranges over \(k{+}1\) sites, not \(k\): replay of a complete prefix immediately invokes the frontier site, and constructing its arguments consumes recorded state, so a demand introduced at the frontier faults during replay, before any live execution. Second, the store against which a site’s demand is validated is the invocation-time store, not the end-of-prefix store: within a concurrency group, a producer’s completion may appear later in the log than a sibling consumer’s invocation, so a changed consumer that reaches across branches can fault even though the demanded payload exists somewhere in the prefix. Both are reconstructible from the log alone, since the protocol records pending invocations and completion order.

The structure is a survival product: rehydration requires every recorded event to be consumable, so a single incompatible site anywhere in history is fatal. Prefix validity captures failure mode (F1); the interface product captures (F2); the migration product captures serialized-state deserialization. In the exact regime the interface factors are indicators and \(R_{\mathrm{b}}(r) \in \{0,1\}\): backward risk is then not an estimate but a verdict. Because \(\theta_r\) is fully known (Assumption 2), no probabilistic approximation of history is ever necessary—runs may be bucketed by prefix hash so the computation is shared across runs with identical histories.

5.2 Forward (behavioral) risk↩︎

Forward risk requires a model of where the run will go. We estimate an absorbing Markov chain on \(G_1\)’s sites from the complete path histories in \(\mathcal{H}\).

The noisy-or composition treats changed sites as independent hazard sources; correlated changes (one logical edit touching several sites) should be grouped into a single hazard before composition. Severity is not assigned by judgment but estimated from telemetry and deployment history (§6.4); domain knowledge enters only as priors that data progressively displaces.

5.3 Aggregate score↩︎

Equivalently, aggregating over the frontier distribution \(\pi(\varphi) = \sum_r \omega_r \mathbb{1}\!\left[\varphi_r = \varphi\right]\) when per-run exactness is not needed: \(\mathrm{WUR}= \sum_{\varphi} \pi(\varphi)\,[\,1-(1-\bar R_{\mathrm{b}}(\varphi))(1-\alpha R_{\mathrm{f}}(\varphi))\,]\), where \(\bar R_{\mathrm{b}}(\varphi)\) averages backward risk over the prefixes observed at \(\varphi\).

6 Estimation from Telemetry↩︎

All quantities in §5 are estimated from persisted data; this section makes the uncertainty explicit so that \(\mathrm{WUR}\) is reported as a posterior, not a point.

6.1 Transition posterior↩︎

With Dirichlet prior \(\boldsymbol{\alpha}_u\) (default: symmetric, concentration \(1\) over \(G_1\)-feasible successors) and counts \(\boldsymbol{c}_u\), the posterior \(P(u,\cdot) \sim \mathrm{Dirichlet}(\boldsymbol{\alpha}_u + \boldsymbol{c}_u)\) has mean \(\hat{P}(u,w) = (\alpha_{uw} + c_{uw}) / (\alpha_{u\cdot} + c_{u\cdot})\). A branch observed a dozen times carries a visibly wide posterior; a branch never observed reverts to the prior—and is flagged (§9).

6.2 Interface posterior↩︎

For site \(v\) with \(n_v\) recorded payloads of which \(m_v\) violate \(D_2(\mu(v))\), \(\rho_\mathrm{I}(v) \sim \mathrm{Beta}(m_v + a,\, n_v - m_v + b)\) with a weak prior \((a,b)\). The distributional regime uses this posterior; the exact regime bypasses it per run.

6.3 Cross-axis pooling↩︎

Per-site axis scores \(\rho_\mathrm{P}, \rho_\mathrm{I}, \rho_\mathrm{M}\) with confidences \(w_\mathrm{P}, w_\mathrm{I}, w_\mathrm{M}\) (posterior precisions; deterministic axes get \(w = \infty\), dominating) are pooled in log-odds space: \[\label{eq:pool} \operatorname{logit} \rho(v) \;=\; \frac{\sum_a w_a \operatorname{logit} \rho_a(v)}{\sum_a w_a},\tag{8}\] with the convention that any axis at \(\rho_a = 1\) with certainty forces \(\rho(v) = 1\). Confidence-weighted log-odds pooling has the two properties the setting demands: independent weak signals compound, and a single certain signal dominates regardless of how many uncertain signals disagree.

6.4 Severity Estimation↩︎

Severity decomposes into three estimable factors, pooled by Equation 8 ; each carries a posterior, so severity uncertainty propagates into the \(\mathrm{WUR}\) interval like every other estimate.

6.4.0.1 Re-execution tolerance.

Durable engines retry failed steps automatically, so the event logs already contain natural re-execution experiments: every recorded retry of step \(s\) that subsequently completed, in a run that finished without an operator-visible incident, is a Bernoulli trial witnessing that an extra execution of \(s\) is tolerated. With \(t_s\) such benign re-executions and \(i_s\) incident-linked ones, \(\kappa(s) \sim \mathrm{Beta}(i_s + a,\, t_s + b)\) estimates the probability that re-executing \(s\) is harmful—an empirical idempotency measure requiring no annotation. Idempotency annotations, where present, enter as informative priors rather than overrides.

6.4.0.2 Blast radius.

The static count of downstream sites consuming \(v\)’s output (normalized by graph size) weights changes whose effects propagate; it is exact, carrying no posterior.

6.4.0.3 Class calibration.

Past releases are natural experiments at the change-class level. The operator’s own deployment history yields per-class \((\text{incident} \mid \text{exposure})\) records, from which empirical-Bayes Beta posteriors are estimated with shrinkage toward a cross-fleet prior. A team that has shipped fifty releases has, in effect, already labeled a severity training set; a team with none inherits the prior and sees correspondingly wider \(\mathrm{WUR}\) intervals—the cold-start cost is reported, not hidden.

6.5 Propagation↩︎

\(\mathrm{WUR}\)’s posterior is obtained by Monte Carlo: draw \(P^{(s)}, \rho^{(s)}\) from their posteriors, recompute 5 –7 , and report the posterior mean with a \(90\%\) credible interval. Because 5 is a sparse linear solve on a graph of tens of nodes, hundreds of draws cost milliseconds. A wide interval is itself an actionable output: insufficient telemetry to certify this migration.

7 Theoretical Properties↩︎

Workflow step graphs are small (\(n\) in the tens); the binding cost is payload validation, which is embarrassingly parallel and incremental (memoizable by prefix hash across candidate releases).

8 Algorithm↩︎

Figure 2 summarizes the functional design: a static lane that never executes anything, a telemetry lane that never inspects source, and a per-run join whose outputs feed the fleet-level coupling stage. Algorithm 3 gives the same structure operationally.

Algorithm 3 touches the world only through the protocol surface (run and event listings); it executes no workflow code and requires no sandbox. Its outputs are (i) the fleet score with credible interval, (ii) a per-run verdict vector, and (iii) per-change annotations—which edit induces which risk, at which sites, affecting how many runs—the explanation artifact an operator sees at deploy time.

8.0.0.1 Implementation notes.

The reference implementation used for §12 (a single-file Python analyzer consuming only run listings and event logs) realizes Algorithm 3 directly and hits the costs of Proposition 7 without tuning; its measured numbers appear in §12. One production optimization is worth recording because it changes the constant dramatically: \(R_{\mathrm{b}}\) depends only on the diff and the run’s (prefix content, frontier) pair, so runs sharing a frontier and trace-equivalent prefix share a verdict. Hashing the canonical normal form of each prefix (§7) and computing once per equivalence class turns per-run work into per-class work; production fleets concentrate mass on few frontiers (runs parked at the same timer or hook), so the class count is typically orders of magnitude below the run count. The per-run exact payload checks that do vary within a class (recorded field presence) reduce to a bitmask over the demanded fields, batched trivially. One scoping rule is soundness-relevant rather than an optimization: the matching of Definition 7 is defined over whole versions, so an analyzer whose diff covers less than every module contributing sites—a single-file diff cannot observe module-qualified renames, for instance—must surface out-of-scope sites as explicit warnings, never as silent certifications.

9 Migration Policy↩︎

The verdict partition follows from thresholds \(0 < \tau_{\mathrm{lo}} < \tau_{\mathrm{hi}} < 1\) on per-run scores:

Three policy consequences are worth stating.

9.0.0.1 The migrate action’s mechanics deserve the same scrutiny as its safety.

A migrate verdict presumes a working resume path: the parked run must actually wake and re-enter execution under the new deployment. Ground-truth testing of one stack found the wake endpoint promoting deferred step-queue messages while a current sleep parks the run behind a deferred workflow-queue message, so the vendor-documented “rerun on latest” recovery silently no-ops for sleeping runs. The model certifies that migration is safe; whether the migration mechanism fires is an orthogonal operational property that should be verified per stack, ideally by the same counterfactual testing the analyzer itself invites.

9.0.0.2 Pinning becomes a measured cost, not a default.

The expected drain time of the pinned population is computable from the same chain (expected absorption time from each frontier, dominated by residual timer durations, which the logs record exactly). A release that strands runs behind a 90-day sleep is now a quantified liability, informing the choice between pinning and authoring an explicit state-migration function for the \(R_{\mathrm{b}}> 0\) residue.

9.0.0.3 Uncertainty routes to review.

Runs whose credible interval straddles a threshold are classified by the interval’s upper bound (pessimistically) and surfaced with the diagnosis low-telemetry branch: the specific transitions whose posteriors are prior-dominated. The remedy—observe more runs, or add a synthetic traversal in staging—is concrete.

9.0.0.4 Release shaping.

By Proposition 6, \(\mathrm{WUR}\) is a sub-release-additive objective: a planned change set can be greedily split into a sequence of releases each below a risk budget, yielding an upgrade plan rather than a single go/no-go.

The thresholds above assume independent runs. When the coupling graph of §10 is nonempty, the partition is instead computed jointly (Theorem 9), and review is defined by label instability under posterior draws (Remark 10).

9.1 A Worked Example↩︎

The whole per-run pipeline fits in one small, fully computed scenario (numbers produced by the reference implementation). A linear order workflow validate \(\to\) charge \(\to\) sleep(24h) \(\to\) notify \(\to\) archive ships a \(V_2\) in which archive newly consumes charge.promoCode, a field present in \(56.7\%\) of the 120 completed historical runs. Four in-flight runs, one change, three different verdicts:

Every mechanism of the model is visible here. Backward risk is zero for all four: the change adds no demand inside any recorded prefix, and \(r_4\)’s completed archive validates against its recorded payload. The forward term does the discriminating, and it discriminates per run from recorded state: \(r_2\) and \(r_3\) sit at the identical frontier under the identical change, but \(r_3\)’s recorded charge payload lacks the demanded field, so its future fault is certain (\(R_{\mathrm{f}}= 1.0\): hitting probability \(1\) on a linear workflow times an exact per-run incompatibility of \(1\)), while \(r_2\)’s is impossible. Only \(r_1\), whose charge has not yet executed, is genuinely probabilistic—its \(0.43\) is the telemetry-estimated field absence rate, and its credible interval (not shown) is what routes it to review rather than a coin flip. Note where the exact/probabilistic boundary actually falls: not between backward and forward, but between recorded and unrecorded state. Only \(r_1\), whose demanded payload does not yet exist, carries probabilistic risk; \(r_2\)–\(r_4\) are decided exactly—\(r_4\) by the backward validation of Definition 11 and \(r_2\), \(r_3\) by a forward term whose incompatibility factor is an indicator over the invocation-time store (§5), exact even though the fault it predicts lies in the future. A rollout that pins \(r_3\), migrates \(r_2\) and \(r_4\), and holds \(r_1\) for review strands exactly one run behind the old deployment instead of the whole fleet.

10 Inter-Run Coupling and the Mixed-Version Window↩︎

This section is the operations layer of the roadmap in §1: everything above it produces per-run verdicts under an independence assumption, and everything in it exists because production fleets violate that assumption in two specific, telemetry-visible ways. Readers evaluating only the per-run model can skip it; operators cannot, because a partition that ignores coupling will split saga partners across versions and manufacture exactly the mixed-version failures it was meant to prevent.

One point of the timeline deserves stating plainly, because the phrase “mixed-version window” invites a misreading. The window is an output of the decision, not an input to it: the entire analysis runs before any \(V_2\) execution exists, on \(V_1\) telemetry and the static diff alone, and the window opens as a consequence of its verdict—migrated and fresh runs proceed on \(V_2\) while the pinned population drains on \(V_1\). No canary phase or A/B observation period is required to decide. What does happen during the window is re-decision, not first decision: \(V_2\) telemetry accrues and sharpens the posteriors (severity calibration across deployment history, §6.4, consumes it automatically), the review class resolves as intervals narrow—re-running the analyzer costs microseconds per run—and pinned runs are re-evaluated when an annotation, a rename map, or a state migration lands. The window closes when the pinned population drains, on the schedule the pinning cost of §9 already prices.

The aggregate of Definition 15 treats runs as independent. Two mechanisms violate this. First, failure contagion: runs coupled through shared external effects can fail because a peer failed, so individually certified runs are not jointly certified. Second—and specific to this problem—mixed-version interaction: any nontrivial migrate/pin partition creates a window in which coupled runs execute different code versions against shared channels. The partition itself manufactures a version-skew surface at the data layer, so a policy that ignores coupling can be individually optimal and jointly unsafe. This section models both, reusing the machinery already in place.

10.1 The Coupling Graph↩︎

The coupling graph \(K = (\mathcal{R}, C)\) has runs as nodes and channel instances as edges. Edges are estimated from three telemetry tiers of decreasing certainty:

1. Protocol edges. Hook dispatches, awaited events, and parent–child starts carry correlation tokens in the event logs themselves; signal and hierarchy edges are therefore deterministic (confidence \(1\)), and their payloads are fully recorded.

2. Resource fingerprints. Step instrumentation (trace-span attributes identifying tables, queues, endpoints) yields the resources each step touches and the access mode; two runs whose fingerprints intersect with at least one write induce a resource edge.

3. Key co-occurrence. Entity identifiers shared across runs’ recorded payloads (order, account, correlation keys) induce edge posteriors: a Beta-distributed existence probability driven by co-occurrence statistics, entering the model with proportionally low confidence.

10.2 Failure Contagion as a Least Fixpoint↩︎

Taking the least fixpoint is a semantic commitment: every failure must be grounded in a chain that bottoms out in endogenous risk. Self-supporting failure cycles—\(r\) fails because \(r'\) does, and vice versa, with no root cause—are excluded, in the spirit of well-founded derivations. The fleet score becomes \(\mathrm{WUR}= \sum_r \omega_r\, q^{*}_r\), and by monotonicity coupling can only increase it: independence was the optimistic bound.

10.3 Mixed-Version Channel Risk↩︎

A channel is an interface whose writer and reader may sit on different versions during the window. The machinery of §4 applies across the channel unchanged: with writer on version \(u\) and reader on version \(w\), \[\rho_{\times}(c;\, u\!\to\! w) \;=\; \mathbb{P}_{x \sim \Phi_c}\!\bigl[\,x \nvDash D_w(c)\,\bigr],\] where \(\Phi_c\) is the recorded payload distribution of the channel (signal payloads are fully logged; resource shapes come from fingerprint samples), and \(D_w\) is the reader-side demand. Lemma 1 transfers verbatim: channels whose reader and writer slices are both unchanged carry \(\rho_{\times} = 0\) with no inference at all.

Timestamps make the window quantitative. The channel’s event rate \(\lambda_c\) carries a Gamma posterior from inter-event times in \(\mathcal{H}\); the expected overlap duration \(T(a)\) under partition \(a\) is the drain time of the pinned side (absorption times plus residual timer durations, which the logs record exactly). Under Poisson arrivals, the mixed-window penalty \[\label{eq:penalty} \pi_c(a) \;=\; 1 - \exp\bigl(-\lambda_c\, T(a)\, \rho_{\times}(c)\bigr)\tag{10}\] is the probability of at least one incompatible cross-version interaction on \(c\) during the window.

10.4 The Coupling-Aware Partition Is a Minimum Cut↩︎

The migrate/pin decision is now a joint labeling \(a \in \{V_1, V_2\}^{\mathcal{R}}\) minimizing \[\label{eq:energy} E(a) \;=\; \sum_{r} \psi_r(a_r) \;+\; \sum_{c = (r, r') \in C} \pi_c \,\mathbb{1}\!\left[a_r \neq a_{r'}\right],\tag{11}\] where \(\psi_r(V_2)\) is the run’s migration risk (with \(R_{\mathrm{b}}(r) > 0 \Rightarrow \psi_r(V_2) = \infty\): hard pin) and \(\psi_r(V_1)\) is the pinning cost: stranding liability (expected drain time) plus forgone-fix exposure \(\beta_r\)—the probability that the run reaches the defect \(V_2\) repairs, which is itself a hitting probability \(h_{\mathrm{defect}}(\varphi_r)\) from the same linear solve as §5. The reason to upgrade and the risk of upgrading are computed by the same operator.

Figure 4 shows the construction on four runs: a coupled pair whose channel penalty exceeds either run’s assignment cost stays on one side of the cut together, which is exactly the mixed-version-window discipline the penalty encodes.

Computationally the extension is light: the fixpoint iteration costs \(O(\mathrm{iters} \cdot |C|)\) with fast convergence in practice (coupling graphs are sparse and shallow), and the cut is one max-flow on \(|\mathcal{R}|\) nodes—both dominated by the payload validation already in Proposition 7.

11 Limitations and Extensions↩︎

Behavioral semantics. \(R_{\mathrm{f}}\) measures exposure to changed code, not whether the change is desirable—an intentional bug fix and an accidental regression score identically. Severity calibration (§6.4) weights exposure by empirical harm, but cannot distinguish intent.

Unobserved paths. Branches never traversed in \(\mathcal{H}\) carry prior-dominated posteriors; new sites in \(V_2\) have no telemetry at all. The model is honest about this (wide intervals) but not clairvoyant.

The Markov assumption. The forward chain is first-order over sites; workflows whose routing depends on accumulated state (retry budgets, aggregated results) have history-dependent transitions the chain averages over. The hitting probabilities remain unbiased in aggregate but can misrank individual runs; conditioning the chain on frontier payload features (a semi-Markov or feature-augmented chain) is a mechanical extension the estimation machinery of §6 already supports, at the cost of thinner per-state telemetry.

Cold start and priors. Until history accumulates, severity and transition posteriors are prior-dominated; the honest behavior is wide intervals routing to review, not confident verdicts from invented constants. Teams that must act before telemetry exists should set deliberately conservative priors per change class and let the credible-interval width report the cost of ignorance transparently; the cold-start measurements of §12 show the distributional regime becoming informative within tens of completed runs.

Cyclic coupling. On dense coupling cycles the contagion fixpoint overestimates (§12), always in the safe direction; tighter cyclic estimates via mean-field corrections or loopy belief propagation with convergence guarantees are future work.

Production validation. The evaluation demonstrates soundness against verified semantics and relevance on the reference repository’s own workflow corpus; it does not yet include production fleets, because the telemetry the model consumes—run listings, event logs, recorded payloads at fleet scale—is exactly the surface only a platform operator holds. This is a structural property of the approach, not an accident of the study: the model is designed to run where the protocol data already lives. Validating it against a production deployment history (releases with known outcomes, replayed through the analyzer counterfactually) requires operator collaboration and is the single highest-value next step.

Order-observed concurrency. Promise.race/any and incremental awaiting retain order semantics by construction (Definition 5); permutation sensitivity there is real, not spurious, so such regions are simply less migrate-eligible. This is a correct restriction, not an unsoundness, but it does reduce the migrate class in racy workflows.

Dynamic demand. Computed property accesses and reflective consumption widen verdicts to unk (§4.1), exerting review pressure in heavily dynamic code. Lemma 1 confines this to changed slices, but a release that rewrites a reflective consumer will legitimately resist certification.

Cold start. Severity class calibration requires deployment history; a fresh installation inherits cross-fleet priors and wide intervals until its own releases accumulate.

Unobserved channels. Coupling through systems that neither the protocol nor step instrumentation observes is invisible; the coupling graph is a lower bound on true coupling, and 9 correspondingly a lower bound on joint risk. Instrumentation coverage is thus a direct input to certification strength.

Transmission estimates. \(\tau\) is the weakest posterior in the model: incidents are rare, so priors dominate for long. Conservative per-kind defaults inflate review, never migrate.

Many concurrent versions. The exact partition is binary; \(k > 2\) live versions require approximate multiway optimization (§10).

12 Evaluation↩︎

We evaluate a reference implementation of the model against a synthetic suite built around a ground-truth oracle that reproduces the verified replay semantics of Remark 1: one identifier sequence shared by all site kinds, ordinal-plus-name matching, in-order log consumption, invocation-time demand evaluation, hard divergence on unmatched events. A single scheduler drives both run simulation and oracle replay, so replaying any log against its own version is safe by construction (verified on 1,500 runs). The analyzer sees only the static diff and telemetry; it never executes \(V'\) against a log. All code and experiment configurations accompany the paper.

12.1 Scenario suite↩︎

Eleven controlled scenarios cover the change classes of §4 over a fixed workflow with a parallel group, a branch, timers, and partial-presence payload fields; each scenario is evaluated against 400 in-flight runs suspended at uniformly random frontiers, with the ground truth given by oracle replay of every run:

The exact-regime verdict agrees with the oracle perfectly on all structural scenarios, including the case Remark 1 makes identity-sensitive: reordering the branches of a join-observed parallel group (S8) is runtime-fatal for every run whose prefix reaches the group, and the analyzer classifies each of the 194 identically. S4 versus S5 shows the prefix rule at its tightest: an insertion at the head invalidates every non-empty prefix, while the same insertion at the tail invalidates none. The two predicate scenarios exhibit the designed conservatism of syntactic matching: a semantic threshold change (S9) is flagged for all 86 runs that crossed the branch while 33 truly diverge, and a pure refactor (S10, identical semantics, different syntax) is flagged for the same 86 while none diverge. No scenario produces a false negative.

12.2 Mutation study↩︎

We generated 120 random workflows (nested parallel groups, branches, timers, hooks, partial-presence fields) and applied every applicable mutation operator from a pool of ten covering all change classes, including producer deletions, producer–consumer order inversions, and reorders of both join-observed and race branches, yielding 1,082 mutations evaluated against 60 in-flight runs each (64,920 run-level verdicts):

Recall is exactly \(1.0\)—zero false negatives across all 64,920 verdicts. The epistemic status of this number deserves precision: it validates that the implementation satisfies Theorem 2 against an oracle enforcing the verified replay semantics; it is a soundness check of the model against its own semantics, not a claim that the model catches failures outside its scope (violated determinism contracts, inference front-end errors on dynamic access, or non-protocol side effects; see §11). One class is outside the oracle’s observable surface by construction: the silent result-crossing of Definition 7’s same-label swap replays as safe—that is what silent means—so evaluating its detection requires a semantic oracle comparing final states against fresh \(V_2\) execution, which we leave as future work; the fingerprint requirement that flags it statically is stated but not exercised by this suite. Within scope, perfect recall is not surprising—it is what the theorem requires, and a single false negative would be an implementation bug, as three found during development were. Precision is \(0.815\), and every false positive has an attributable cause: syntactic predicate matching (86%), demands whose satisfiability crosses conditional-arm or race-branch boundaries the scope analysis cannot prove (13%), and the conservative certainly-precedes prefix rule (2%)—i.e., the deliberate conservatism analyzed in §11, not the model. Precision has a direct operational reading: \(1 - \mathrm{precision}\) is the fraction of fatal verdicts that needlessly pin a run, and its cost is exactly the stranding liability and forgone-fix exposure that §9 prices—so the conservatism is not free, but it is measured, and every attributable cause above is also an annotation target (predicate-equivalence hints alone would remove 86% of it). Notably, demand-growth mutations include consumers that reach across parallel branches; catching these requires the invocation-time store of Definition 11, and validating against the end-of-prefix store instead produces false negatives (an error mode this suite caught in an earlier revision of the model).

12.3 Real-workflow corpus↩︎

Synthetic topologies establish soundness; real ones establish relevance. The corpus is the workflow code shipped in the reference implementation’s own repository, github.com/vercel/workflow at commit 39673b7 (2026-07-08): every function carrying the ’use workflow’ directive under workbench/vitest/workflows (including the cookbook suite of documented canonical patterns) and under workbench/example/workflows files 0–10, excluding only the load/e2e stress files (97–100) whose hundred-odd micro-workflows exercise the runtime rather than represent applications. This yields 45 workflow functions; the model corpus has 44 entries (one thin child-spawning wrapper is folded into its parent as the step invocation it is), of which 41 contain at least one durable site, totaling 126 sites.

“Hand-translated” means the following mechanical procedure, whose output is a reviewable artifact (one annotated constructor per workflow, keyed by source path, in real_corpus.py accompanying the paper). (1) Each ’use step’ call maps to a step whose payload schema is the step body’s actual return-object fields; TypeScript-optional or conditionally assigned fields get partial presence probabilities, all others presence 1. (2) sleep() maps to a timer; createWebhook() or hook.create() followed by await maps to a payload-bearing hook. (3) Promise.all and allSettled map to join-observed parallel groups with branches in source-array order (order is identity); Promise.race maps to a race group with the verified semantics of Remark 1—branches invoked in fork order, the continuation resumed at the first completion in log order, losers left pending, consumable if their completions appear later in the log and dropped at workflow return otherwise. A background invocation awaited after intervening work is an additional branch at its invocation point. (4) if/else on step or hook results maps to a branch whose predicate reads the recorded payload field the source reads; try/catch compensation (the saga pattern) maps to a branch into the compensation sequence in unwind order. (5) Data-flow demand edges are placed exactly where the source passes one site’s result into another call’s arguments. (6) Loops with source-fixed bounds are unrolled at those bounds. Two mechanical checks validate the translations: every one of 1,320 prefixes of simulated runs replays safe against its own topology under the oracle, and the race workflows exhibit all four log shapes the runtime can record (winner only, winner then loser, loser interleaved after post-race sites, either branch winning). Consumers reaching into race branches are treated by the scope analysis as never-guaranteed, since a loser may never complete. The known approximations are stated rather than hidden: loop unrolling fixes iteration counts, and winner-dependent orchestrator transforms (.then mappings on race results) are deterministic orchestrator code, not payload demands, so they carry no demand edge.

The corpus spans the patterns the vendor documents as canonical: sagas, fan-out, human-in-the-loop approval, parent–child workflows over completion hooks, content routing, batching with inter-batch timers, webhooks, and durable agents.

Applying the mutation pool to this corpus yields 227 mutations and 18,160 run-level verdicts (80 in-flight runs per workflow): recall is again exactly \(1.0\), precision \(0.933\).

Precision is higher than on the synthetic suite because real topologies are shorter and their prefixes more often provably unaffected. The corpus also improved the model: producer deletion and producer–consumer order inversion—natural here, where hook payloads feed later steps—produced false negatives in an earlier revision, forcing the demand-satisfiability rule and the \(V_2\)-side invocation gate of §4.1. The residual false positives are again fully attributable: syntactic predicate matching (74%, concentrated in the router and single-statement control-flow workflows), demand scope across conditional arms and race branches (24%), and the certainly-precedes rule on branch reorders (2%).

12.4 Calibration of distributional interface risk↩︎

For 400 trials with the demanded field’s presence probability drawn uniformly from \([0.05, 0.95]\), the distributional-regime \(R_{\mathrm{b}}\) estimated from historical presence telemetry was compared with the empirical replay-failure rate among affected in-flight runs. Expected calibration error over ten bins is \(0.016\), Pearson correlation \(0.92\), mean absolute error \(0.087\)—consistent with the claim that when payloads are not retained, presence frequencies alone give a well-calibrated risk.

12.5 Contagion fixpoint versus simulated cascades↩︎

We compared the least-fixpoint estimate 9 against Monte-Carlo cascade simulation (20,000 samples per graph) on random coupling graphs, five graphs per configuration, reporting the signed error \(q^* - \hat{q}_{\mathrm{MC}}\) per node:

The “worst under” column never drops below \(-0.009\), which is within Monte-Carlo noise at 20,000 samples: empirically the fixpoint is a one-sided, conservative estimate, consistent with the positive association of percolation-style cascade events (Harris/FKG), under which the noisy-or independence assumption can only overestimate. On acyclic coupling the bound is tight; on cyclic coupling, feedback echo inflates the estimate, worst where a sparse cycle concentrates the echo. Overestimation moves runs from migrate toward review/pin, never the reverse, so the approximation errs in the safe direction; tighter cyclic estimates are future work.

12.6 Partition optimality and cost↩︎

Across 200 random instances of 12 runs with dense coupling, the min-cut partition of §10 attains exactly the brute-force minimum energy (maximum gap \(0.0\) over all \(2^{12}\) labelings per instance), as Theorem 9 requires. One implementation note: computing the partition side of the cut with floating-point capacities corrupted residual reachability in a standard max-flow library; integer-scaled capacities restore exactness.

Backward risk in the exact regime costs 9–15 \(\mu\)s per run in a pure Python reference implementation (single core): a fleet of 50,000 in-flight runs is classified in \(0.72\) s, three orders of magnitude inside the per-release budget of Proposition 7, before any of the prefix-hash deduplication that production fleets admit. Scaling in workflow size is linear in prefix length, as Proposition 7 predicts: per-run \(R_{\mathrm{b}}\) grows from \(4\,\mu\)s at 10 sites to \(3.6\) ms at a pathological 2,000 sites (with the one-time static diff at \(0.5\) s), so even a fleet of 10,000 runs of thousand-step workflows classifies in under a minute on one core. Telemetry volume matters least where one might fear it most: the distributional regime’s error against ground truth falls from MAE \(0.15\) with only ten completed historical runs to \(0.09\) at three hundred, at which point the residual is the binomial noise of the affected-run sample rather than the estimator—useful predictions begin at tens of runs, not thousands.

13 Conclusion↩︎

Durable workflow engines already pay the storage cost of complete execution histories; this paper converts that cost into an analytical asset. Because the event log is the protocol, upgrade risk in this domain splits cleanly into a component that can be computed exactly from recorded prefixes and payloads, and a component that is genuinely probabilistic and estimable, with honest uncertainty, from complete path histories. The resulting \(\mathrm{WUR}\) score turns version-skew handling from a uniformly pessimistic mechanism into a measured decision: migrate what is provably safe, review what is uncertain, pin what is provably not—and know, in advance, what each release will cost the fleet.

13.0.0.1 Availability.

The reference implementation (a single-file analyzer consuming only runs.list and events.list), the hand-translated real-workflow corpus keyed to source paths at the stated commit, the full experiment suite, and the raw results accompany this paper. We invite platform operators holding production deployment histories to collaborate on counterfactual validation—replaying past releases with known outcomes through the analyzer—which is the highest-value experiment this paper cannot run alone; contact the authors.

References↩︎