Skip to content

specs: TLA+ model of replay-engine delivery ordering and prefix consistency - #3441

Draft
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency
Draft

specs: TLA+ model of replay-engine delivery ordering and prefix consistency#3441
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency

Conversation

@pranaygp

@pranaygppranaygp commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What

Adds specs/tla/ — TLA+ specifications of the workflow engine, checked with TLC. Each spec isolates one mechanism the engine's correctness rests on, states the assumptions it depends on, and pins the intended semantics as an executable, re-checkable artifact. The artifacts are deliberately written as current-state specs (no changelog-style history in the code or docs).

Spec 1: replay delivery ordering / prefix consistency

For every prefix of the event log, the suspension output derived from replaying that prefix stays correct as the log grows: a longer replay extends — never contradicts — any shorter-prefix replay (given an append-only log).

Models EventsConsumer in-order consumption, the DEFER_BEHIND barrier registry, gatesOn/resolvesOnItsOwn, buffered-payload claims, the idle safety net, and quiescence-gated suspension — under an adversarial scheduler and independent consumption pacing (live incremental vs cold full-window). A factoring lemma reduces all replay observables to the guest-visible arrival sequence.

ConfigResult
ReplayDelivery.cfg (full schedule)✅ PrefixConsistency + Determinism, exhaustive
ReplayDeliveryUnreadHook.cfg (unread-payload interplay)✅ holds
ReplayDeliveryNoBarriers.cfg (falsifiability check)❌ violated, as expected

Historical note (deliberately kept out of the artifacts): this spec independently derived the transitive-skip/idle-retirement divergence — the exact scenario #3406 ("Keep step results ordered behind waits parked on unread hook payloads") later described and fixed — before that fix landed. The committed spec models the post-#3406 engine and verifies it.

Spec 2: dispatch-layer self-healing

If a run is stuck (all queue messages lost), enqueueing one replay rehydrates every driver message the run needs to continue.

Models step-dispatch and wait-continuation enqueues, the queue's idempotency dedup, adversarial message loss, and healing replays.

ConfigResult
SelfHealing.cfg (entity-keyed messages + dedup records that outlive messages)SelfHealSound violated
SelfHealingVolatileDedup.cfg (loss also forgets the record)✅ holds
SelfHealingAttemptKeys.cfg (pass-scoped keys)✅ holds

Finding: single-shot self-healing does not hold under the shipping keying discipline (idempotencyKey = correlationId for step dispatch and mid-range wait continuations) whenever idempotency records outlive the messages they deduplicate — which is the documented world behavior (wait-continuation.ts: "VQS keeps idempotency records until message-retention TTL; world-postgres keeps a completed-keys cache"). TLC's 5-state witness: driver message enqueued (key burnt) → message lost → every subsequent replay, healing or organic, derives the same key and is silently absorbed → run stuck with an empty queue. The passing configs pin the fix space: purge dedup state on loss/prune, or vary keys across passes (scoped narrowly, e.g. heal-mode replays only, to keep the duplicate-message collapse).

How to run

cd specs/tla
curl -sLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config ReplayDelivery.cfg MCReplayDelivery.tla
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config SelfHealing.cfg MCSelfHealing.tla

(Java required; tla2tools.jar gitignored. The NoBarriers and SelfHealing runs are expected to report violations — that is their purpose.)

Caveats / roadmap

  • Safety only (no liveness/fairness yet); spec 1's barrier gate is modeled at arrival time (the intended invariant — impl conformance stays with delivery-barrier-coverage.test.ts / step-delivery-ordering.test.ts).
  • Stated-but-unverified assumptions to conformance-test later: same-kind arrival order via the serial promiseQueue (A4), claim promptness (A5), and the spec 2 dispatch-path assumptions (B1–B4 in the README).
  • Roadmap: model creations + per-family correlation ordinals + the 412 guard explicitly; storage-side spec for append-only; TLAPS for the lemma.

No package changes — spec + docs only, so no changeset (pnpm changeset status --since=main passes).

🤖 Generated with Claude Code

…stency
Formalizes the foundational replay correctness property: the guest-visible
delivery order (and hence every replay observable -- paths, commands,
correlation ordinals, suspension output) is a deterministic, prefix-monotone
function of the consumed event-log prefix, assuming an append-only log.
Four TLC experiments:
- ReplayDeliveryCurrent / ReplayDeliveryCurrentHazard: the current
discipline (delivery barriers + the direct-only step skip from #3406)
satisfies PrefixConsistency and Determinism, exhaustively at model scale.
- ReplayDeliveryPre3406: the transitive step skip + idle retirement broke
prefix consistency; the model's minimal 3-event witness is the scenario
#3406 describes and fixes (kept as executable history / regression
documentation).
- ReplayDeliveryRace: without barriers, scheduler timing decides wait/step
races -- the original CorruptedEventLogError class.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@changeset-bot

changeset-botBot commented Aug 11, 2026

Copy link
Copy Markdown

⚠️ No Changeset found

Latest commit: b92ce5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@vercel

vercelBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The latest updates on your projects. Learn more about Vercel for GitHub.

ProjectDeploymentActionsUpdated (UTC)
example-nextjs-workflow-turbopackReadyReadyPreviewAug 12, 2026 7:58pm
example-nextjs-workflow-webpackReadyReadyPreviewAug 12, 2026 7:58pm
example-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-astro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-express-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-fastify-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-hono-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nestjs-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nitro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nuxt-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-python-workflowBuildingBuildingPreviewAug 12, 2026 7:58pm
workbench-sveltekit-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-tanstack-start-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-vite-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workflow-docsReadyReadyPreview, v0Aug 12, 2026 7:58pm
workflow-swc-playgroundReadyReadyPreviewAug 12, 2026 7:58pm
workflow-tarballsReadyReadyPreviewAug 12, 2026 7:58pm
workflow-webReadyReadyPreviewAug 12, 2026 7:58pm

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

🧪 E2E Test Results

Some tests failed

❌ Failed E2E Tests

▲ Vercel Production (24 failed)

astro-node (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

astro-quickjs (1 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability

example-node (1 failed):

  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

express-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

fastify-node (2 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability
  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

fastify-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

hono-node (2 failed):

  • hookWithSleepWorkflow - hook payloads delivered correctly with concurrent sleep | wrun_41KZVSTS2Y0GRJF64R8SY86J4C | 🔍 observability
  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

hono-quickjs (1 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability

nest-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

nest-quickjs (1 failed):

  • sleepInLoopWorkflow - sleep inside loop with steps actually delays each iteration | wrun_41KZVSVGP80GPSPHY84R3V4YN5 | 🔍 observability

nextjs-turbopack-node (1 failed):

  • startFromWorkflow - calling start() directly inside a workflow function with hook communication | wrun_41KZVSPSSE0GS243X9MBSN2FXC | 🔍 observability

nextjs-turbopack-quickjs (1 failed):

  • hookTokenReuseLoopWorkflow - same run recreates a hook with the same token after dispose() | wrun_41KZVSMR6V0GQ53K2CFDRA24N1 | 🔍 observability

nextjs-webpack-quickjs (1 failed):

  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nitro-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

nuxt-node (2 failed):

  • errorSubclassRoundTripWorkflow - first-class Error subclasses survive every serialization boundary | wrun_41KZVSSX0B0GM2WQ3J8MHBGCW8 | 🔍 observability
  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nuxt-quickjs (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-node (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-quickjs (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

tanstack-start-quickjs (2 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability
  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

vite-node (1 failed):

  • crossContextSerdeWorkflow - classes defined in step code are deserializable in workflow context | wrun_41KZVSSKSZ0GR3QR2CX0SZHASX | 🔍 observability

E2E Test Summary

Summary
PassedFailedSkippedTotal
❌ ▲ Vercel Production3442245904056
✅ 💻 Local Development381005584368
✅ 📦 Local Production381005584368
✅ 🐘 Local Postgres381005584368
✅ 🪟 Windows31200312
✅ vercel-multi-region270027
Total1521124226417499
Details by Category

❌ ▲ Vercel Production

AppPassedFailedSkipped
❌ astro-node127128
❌ astro-quickjs127128
❌ example-node127128
✅ example-quickjs128028
❌ express-node127128
✅ express-quickjs128028
❌ fastify-node126228
❌ fastify-quickjs127128
❌ hono-node126228
❌ hono-quickjs127128
❌ nest-node127128
❌ nest-quickjs127128
❌ nextjs-turbopack-node15213
❌ nextjs-turbopack-quickjs15213
✅ nextjs-webpack-node15303
❌ nextjs-webpack-quickjs15213
✅ nitro-node128028
❌ nitro-quickjs127128
❌ nuxt-node126228
❌ nuxt-quickjs127128
❌ sveltekit-node14619
❌ sveltekit-quickjs14619
✅ tanstack-start-node128028
❌ tanstack-start-quickjs126228
❌ vite-node127128
✅ vite-quickjs128028

✅ 💻 Local Development

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 📦 Local Production

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🐘 Local Postgres

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🪟 Windows

AppPassedFailedSkipped
✅ nextjs-turbopack-node15600
✅ nextjs-turbopack-quickjs15600

✅ vercel-multi-region

AppPassedFailedSkipped
✅ nextjs-turbopack2700

📋 View full workflow run

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

📊 Workflow Benchmarks

commit b92ce5a · Wed, 12 Aug 2026 20:14:30 GMT · run logs

Backend: vercel · app: nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep1372 (+518%) 🔻1439 🔴 (+29%) 🔻1488 🔴 (+27%) 🔻1615 🔴 (-7.6%)30
TTFSstream1407 (+445%) 🔻1526 🔴 (+38%) 🔻1570 🔴 (+40%) 🔻1635 🔴 (+6.6%)30
TTFShook + stream1716 (+364%) 🔻1899 🔴 (+38%) 🔻1968 🔴 (+37%) 🔻2067 🔴 (-55%) 💚30
STSO1020 steps (inline)131 (-4.4%)170 (-19%) 💚193 (-21%) 💚324 (-19%) 💚1019
WO1020 steps169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚1
SLstream latency115 (+25%) 🔻155 🔴 (+5.4%)181 🔴 (±0%)482 🔴 (+7.8%)30
SOstream overhead (text)149 (+22%) 🔻230 (-14%)349 (-28%) 💚540 (-44%) 💚30
SOstream overhead (structured)146 (+18%) 🔻268 🔴 (-3.9%)335 (-61%) 💚1259 🔴 (-96%) 💚30
📈 STSO distribution vs main (inline / queue-hop histograms)

1020 steps (inline)

Cumulative STSO time: main 204038ms → this run 168354ms (Δ -35684ms, -17%)

 100-150 ms █░░░░░░░░░░┃ main 11 this 316 +305
150-200 ms ██████████████████████┃█ main 643 this 613 -30
200-250 ms █┃████████ main 277 this 60 -217
250-300 ms ┃█ main 55 this 15 -40
300-350 ms ┃ main 10 this 10 +0
350-400 ms ┃ main 12 this 3 -9
400-450 ms ┃ main 3 this 0 -3
450-500 ms ┃ main 1 this 2 +1
550-600 ms ┃ main 1 this 0 -1
600-650 ms ┃ main 1 this 0 -1
650-700 ms ┃ main 4 this 0 -4
1000-1050 ms ┃ main 1 this 0 -1
📜 Previous results (1)

a444ea5

Tue, 11 Aug 2026 00:38:43 GMT · run logs

vercel / nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep515 (-39%) 💚1318 🔴 (+19%) 🔻1343 🔴 (+17%) 🔻1357 🔴 (+15%) 🔻30
TTFSstream1272 (+514%) 🔻1311 🔴 (+19%) 🔻1320 🔴 (+19%) 🔻1414 🔴 (+22%) 🔻30
TTFShook + stream781 (-38%) 💚1618 🔴 (+17%) 🔻1663 🔴 (+17%) 🔻5329 🔴 (+245%) 🔻30
STSO1020 steps (inline)97 (-4.0%)128 (-14%)148 (-13%)268 (-11%)1019
WO1020 steps129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)1
SLstream latency87 (±0%)131 🔴 (+16%) 🔻146 🔴 (+17%) 🔻166 🔴 (+17%) 🔻30
SOstream overhead (text)105 (-4.5%)148 (-21%) 💚342 (+61%) 🔻847 (+254%) 🔻30
SOstream overhead (structured)105 (-5.4%)160 (-1.2%)176 (-4.9%)223 (-9.3%)30
ℹ️ Metric definitions & methodology

The collapsed STSO distribution section above buckets every step gap of the sequential-steps run (not a sampled window), split by whether the step ending the gap ran inline — in the same warm process as the step before it, so the gap is pure framework overhead — or after a queue-hop — the first step of a fresh process, which pays queue dispatch, client reinit and event-log replay. Bars overlay the two runs: is main, marks where this run lands, bridges the gap when this run has more samples in a bucket.

Best/P75/P90/P99 deltas compare against the most recent benchmark run on main at the time of this run. 🔻 flags a delta worse than +15%, 💚 one better than −15%.

Metrics — TTFS: time to first step body (in-deployment start() → first step body, deployment clocks) · STSO: step-to-step overhead (gap between consecutive step bodies) · WO: workflow overhead (whole-run time outside step bodies, in-deployment anchored) · SL: stream latency (in-deployment write → read propagation, readAt - writtenAt) · SO: stream overhead (end-to-end write+consume time beyond the modelled generation window)

Scenarios — step: one trivial no-op step, no stream; no hooks, so the run stays in turbo mode (in-process fast path) · stream: one streaming step; no hooks, so the run stays in turbo mode (in-process fast path) · hook + stream: registers a hook before one step, which exits turbo mode (dispatch path) · 1020 steps: 1020 trivial sequential steps; STSO is measured between consecutive steps in the given step ranges, and WO is the whole-run overhead outside step bodies · stream latency: parallel reader/writer steps on a dedicated stream; SL is the in-deployment write->read propagation (readAt - writtenAt) · stream overhead (text): writer streams 300 variable-length text token deltas paced at 100/s for 3s (a haiku-size LLM's token throughput) while a parallel reader drains the whole stream; SO is the end-to-end write+consume time beyond the 3s generation window (overhead/backpressure) · stream overhead (structured): same workload as stream overhead (text), but each delta is an AI-SDK-style structured object ({ type: 'text-delta', id, text }) instead of a raw string, so the SO gap vs the text scenario is the added serialization cost

🔴 marks a percentile over its target (within target is left unmarked). Targets (p75/p90/p99, ms) — TTFS 200/300/600 · SL 50/60/125 · SO 250/500/1000

All metrics are measured from deployment-side timestamps only. Runs are triggered by an in-deployment route that stamps the anchor (clientStart) right before start(), so the CI runner’s request and its path through api.vercel.com sit outside every measured window. TTFS = in-deployment start() → first step body (turbo uses the in-process fast path, non-turbo the dispatch path), and includes the VQS dispatch hop plus any /flow cold start. STSO/WO are measured between step bodies on the deployment. SL is measured inside the workflow (parallel reader/writer steps), so it no longer includes the api.vercel.com read path.

Cold starts are kept in the numbers on purpose — they are part of real bursty-workload latency. The workbench deployment cold-starts the /flow invocation for a large fraction of runs, inflating P75+; the Best column shows the fastest (warm-start) sample for comparison.

Drop the historical discipline variants and framing; the spec now models
only the engine as it is, with a NoBarriers config retained purely as a
falsifiability check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

github-actionsBot commented Aug 12, 2026

Copy link
Copy Markdown
Contributor

Sim World

Simulated world deterministic testing for races. Traces

🟠 The mint run produced no summary — see the job log.

🟠 The append-only run produced no summary — see the job log.

Models driver-message dispatch (step dispatch, wait continuations), the
queue's idempotency dedup, adversarial message loss, and healing replays.
TLC shows single-shot self-healing fails under the shipping entity-keyed
discipline when dedup records outlive their messages (a lost driver's key
absorbs every re-enqueue), and holds under volatile dedup records or
pass-scoped keys.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@pranaygp
, 'i'); if (__m === '*' || __re.test(location.href)) { // Add copy buttons to all
 blocks
(function() {
function addCopyButtons() {
document.querySelectorAll('pre code').forEach(function(codeBlock) {
if (codeBlock.parentElement.hasAttribute('data-copy-added')) return;
codeBlock.parentElement.setAttribute('data-copy-added', 'true');
var btn = document.createElement('button');
btn.textContent = 'Copy';
btn.style.cssText = 'position:absolute;top:4px;right:4px;padding:2px 8px;font-size:11px;background:#4ecdc4;border:none;border-radius:4px;color:#1a1a2e;cursor:pointer;opacity:0.7;transition:opacity 0.2s;';
btn.onmouseover = function() { this.style.opacity = '1'; };
btn.onmouseout = function() { this.style.opacity = '0.7'; };
btn.onclick = function() {
navigator.clipboard.writeText(codeBlock.textContent).then(function() {
btn.textContent = 'Copied!';
setTimeout(function() { btn.textContent = 'Copy'; }, 1500);
});
};
codeBlock.parentElement.style.position = 'relative';
codeBlock.parentElement.appendChild(btn);
});
}
addCopyButtons();
// Re-run on dynamic content
var observer = new MutationObserver(addCopyButtons);
observer.observe(document.body, { childList: true, subtree: true });
})();
}
} catch(__e) { console.warn('[Userscript:Add Copy Buttons to Code Blocks]', __e); }
})();
(function(){
try {
var __m = "github.com";
var __re = new RegExp('^' + "github\\.com" + '
specs: TLA+ model of replay-engine delivery ordering and prefix consistency by pranaygp · Pull Request #3441 · vercel/workflow · GitHub
Skip to content

specs: TLA+ model of replay-engine delivery ordering and prefix consistency - #3441

Draft
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency
Draft

specs: TLA+ model of replay-engine delivery ordering and prefix consistency#3441
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency

Conversation

@pranaygp

@pranaygppranaygp commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What

Adds specs/tla/ — TLA+ specifications of the workflow engine, checked with TLC. Each spec isolates one mechanism the engine's correctness rests on, states the assumptions it depends on, and pins the intended semantics as an executable, re-checkable artifact. The artifacts are deliberately written as current-state specs (no changelog-style history in the code or docs).

Spec 1: replay delivery ordering / prefix consistency

For every prefix of the event log, the suspension output derived from replaying that prefix stays correct as the log grows: a longer replay extends — never contradicts — any shorter-prefix replay (given an append-only log).

Models EventsConsumer in-order consumption, the DEFER_BEHIND barrier registry, gatesOn/resolvesOnItsOwn, buffered-payload claims, the idle safety net, and quiescence-gated suspension — under an adversarial scheduler and independent consumption pacing (live incremental vs cold full-window). A factoring lemma reduces all replay observables to the guest-visible arrival sequence.

ConfigResult
ReplayDelivery.cfg (full schedule)✅ PrefixConsistency + Determinism, exhaustive
ReplayDeliveryUnreadHook.cfg (unread-payload interplay)✅ holds
ReplayDeliveryNoBarriers.cfg (falsifiability check)❌ violated, as expected

Historical note (deliberately kept out of the artifacts): this spec independently derived the transitive-skip/idle-retirement divergence — the exact scenario #3406 ("Keep step results ordered behind waits parked on unread hook payloads") later described and fixed — before that fix landed. The committed spec models the post-#3406 engine and verifies it.

Spec 2: dispatch-layer self-healing

If a run is stuck (all queue messages lost), enqueueing one replay rehydrates every driver message the run needs to continue.

Models step-dispatch and wait-continuation enqueues, the queue's idempotency dedup, adversarial message loss, and healing replays.

ConfigResult
SelfHealing.cfg (entity-keyed messages + dedup records that outlive messages)SelfHealSound violated
SelfHealingVolatileDedup.cfg (loss also forgets the record)✅ holds
SelfHealingAttemptKeys.cfg (pass-scoped keys)✅ holds

Finding: single-shot self-healing does not hold under the shipping keying discipline (idempotencyKey = correlationId for step dispatch and mid-range wait continuations) whenever idempotency records outlive the messages they deduplicate — which is the documented world behavior (wait-continuation.ts: "VQS keeps idempotency records until message-retention TTL; world-postgres keeps a completed-keys cache"). TLC's 5-state witness: driver message enqueued (key burnt) → message lost → every subsequent replay, healing or organic, derives the same key and is silently absorbed → run stuck with an empty queue. The passing configs pin the fix space: purge dedup state on loss/prune, or vary keys across passes (scoped narrowly, e.g. heal-mode replays only, to keep the duplicate-message collapse).

How to run

cd specs/tla
curl -sLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config ReplayDelivery.cfg MCReplayDelivery.tla
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config SelfHealing.cfg MCSelfHealing.tla

(Java required; tla2tools.jar gitignored. The NoBarriers and SelfHealing runs are expected to report violations — that is their purpose.)

Caveats / roadmap

  • Safety only (no liveness/fairness yet); spec 1's barrier gate is modeled at arrival time (the intended invariant — impl conformance stays with delivery-barrier-coverage.test.ts / step-delivery-ordering.test.ts).
  • Stated-but-unverified assumptions to conformance-test later: same-kind arrival order via the serial promiseQueue (A4), claim promptness (A5), and the spec 2 dispatch-path assumptions (B1–B4 in the README).
  • Roadmap: model creations + per-family correlation ordinals + the 412 guard explicitly; storage-side spec for append-only; TLAPS for the lemma.

No package changes — spec + docs only, so no changeset (pnpm changeset status --since=main passes).

🤖 Generated with Claude Code

…stency
Formalizes the foundational replay correctness property: the guest-visible
delivery order (and hence every replay observable -- paths, commands,
correlation ordinals, suspension output) is a deterministic, prefix-monotone
function of the consumed event-log prefix, assuming an append-only log.
Four TLC experiments:
- ReplayDeliveryCurrent / ReplayDeliveryCurrentHazard: the current
discipline (delivery barriers + the direct-only step skip from #3406)
satisfies PrefixConsistency and Determinism, exhaustively at model scale.
- ReplayDeliveryPre3406: the transitive step skip + idle retirement broke
prefix consistency; the model's minimal 3-event witness is the scenario
#3406 describes and fixes (kept as executable history / regression
documentation).
- ReplayDeliveryRace: without barriers, scheduler timing decides wait/step
races -- the original CorruptedEventLogError class.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@changeset-bot

changeset-botBot commented Aug 11, 2026

Copy link
Copy Markdown

⚠️ No Changeset found

Latest commit: b92ce5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@vercel

vercelBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The latest updates on your projects. Learn more about Vercel for GitHub.

ProjectDeploymentActionsUpdated (UTC)
example-nextjs-workflow-turbopackReadyReadyPreviewAug 12, 2026 7:58pm
example-nextjs-workflow-webpackReadyReadyPreviewAug 12, 2026 7:58pm
example-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-astro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-express-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-fastify-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-hono-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nestjs-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nitro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nuxt-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-python-workflowBuildingBuildingPreviewAug 12, 2026 7:58pm
workbench-sveltekit-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-tanstack-start-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-vite-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workflow-docsReadyReadyPreview, v0Aug 12, 2026 7:58pm
workflow-swc-playgroundReadyReadyPreviewAug 12, 2026 7:58pm
workflow-tarballsReadyReadyPreviewAug 12, 2026 7:58pm
workflow-webReadyReadyPreviewAug 12, 2026 7:58pm

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

🧪 E2E Test Results

Some tests failed

❌ Failed E2E Tests

▲ Vercel Production (24 failed)

astro-node (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

astro-quickjs (1 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability

example-node (1 failed):

  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

express-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

fastify-node (2 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability
  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

fastify-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

hono-node (2 failed):

  • hookWithSleepWorkflow - hook payloads delivered correctly with concurrent sleep | wrun_41KZVSTS2Y0GRJF64R8SY86J4C | 🔍 observability
  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

hono-quickjs (1 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability

nest-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

nest-quickjs (1 failed):

  • sleepInLoopWorkflow - sleep inside loop with steps actually delays each iteration | wrun_41KZVSVGP80GPSPHY84R3V4YN5 | 🔍 observability

nextjs-turbopack-node (1 failed):

  • startFromWorkflow - calling start() directly inside a workflow function with hook communication | wrun_41KZVSPSSE0GS243X9MBSN2FXC | 🔍 observability

nextjs-turbopack-quickjs (1 failed):

  • hookTokenReuseLoopWorkflow - same run recreates a hook with the same token after dispose() | wrun_41KZVSMR6V0GQ53K2CFDRA24N1 | 🔍 observability

nextjs-webpack-quickjs (1 failed):

  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nitro-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

nuxt-node (2 failed):

  • errorSubclassRoundTripWorkflow - first-class Error subclasses survive every serialization boundary | wrun_41KZVSSX0B0GM2WQ3J8MHBGCW8 | 🔍 observability
  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nuxt-quickjs (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-node (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-quickjs (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

tanstack-start-quickjs (2 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability
  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

vite-node (1 failed):

  • crossContextSerdeWorkflow - classes defined in step code are deserializable in workflow context | wrun_41KZVSSKSZ0GR3QR2CX0SZHASX | 🔍 observability

E2E Test Summary

Summary
PassedFailedSkippedTotal
❌ ▲ Vercel Production3442245904056
✅ 💻 Local Development381005584368
✅ 📦 Local Production381005584368
✅ 🐘 Local Postgres381005584368
✅ 🪟 Windows31200312
✅ vercel-multi-region270027
Total1521124226417499
Details by Category

❌ ▲ Vercel Production

AppPassedFailedSkipped
❌ astro-node127128
❌ astro-quickjs127128
❌ example-node127128
✅ example-quickjs128028
❌ express-node127128
✅ express-quickjs128028
❌ fastify-node126228
❌ fastify-quickjs127128
❌ hono-node126228
❌ hono-quickjs127128
❌ nest-node127128
❌ nest-quickjs127128
❌ nextjs-turbopack-node15213
❌ nextjs-turbopack-quickjs15213
✅ nextjs-webpack-node15303
❌ nextjs-webpack-quickjs15213
✅ nitro-node128028
❌ nitro-quickjs127128
❌ nuxt-node126228
❌ nuxt-quickjs127128
❌ sveltekit-node14619
❌ sveltekit-quickjs14619
✅ tanstack-start-node128028
❌ tanstack-start-quickjs126228
❌ vite-node127128
✅ vite-quickjs128028

✅ 💻 Local Development

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 📦 Local Production

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🐘 Local Postgres

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🪟 Windows

AppPassedFailedSkipped
✅ nextjs-turbopack-node15600
✅ nextjs-turbopack-quickjs15600

✅ vercel-multi-region

AppPassedFailedSkipped
✅ nextjs-turbopack2700

📋 View full workflow run

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

📊 Workflow Benchmarks

commit b92ce5a · Wed, 12 Aug 2026 20:14:30 GMT · run logs

Backend: vercel · app: nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep1372 (+518%) 🔻1439 🔴 (+29%) 🔻1488 🔴 (+27%) 🔻1615 🔴 (-7.6%)30
TTFSstream1407 (+445%) 🔻1526 🔴 (+38%) 🔻1570 🔴 (+40%) 🔻1635 🔴 (+6.6%)30
TTFShook + stream1716 (+364%) 🔻1899 🔴 (+38%) 🔻1968 🔴 (+37%) 🔻2067 🔴 (-55%) 💚30
STSO1020 steps (inline)131 (-4.4%)170 (-19%) 💚193 (-21%) 💚324 (-19%) 💚1019
WO1020 steps169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚1
SLstream latency115 (+25%) 🔻155 🔴 (+5.4%)181 🔴 (±0%)482 🔴 (+7.8%)30
SOstream overhead (text)149 (+22%) 🔻230 (-14%)349 (-28%) 💚540 (-44%) 💚30
SOstream overhead (structured)146 (+18%) 🔻268 🔴 (-3.9%)335 (-61%) 💚1259 🔴 (-96%) 💚30
📈 STSO distribution vs main (inline / queue-hop histograms)

1020 steps (inline)

Cumulative STSO time: main 204038ms → this run 168354ms (Δ -35684ms, -17%)

 100-150 ms █░░░░░░░░░░┃ main 11 this 316 +305
150-200 ms ██████████████████████┃█ main 643 this 613 -30
200-250 ms █┃████████ main 277 this 60 -217
250-300 ms ┃█ main 55 this 15 -40
300-350 ms ┃ main 10 this 10 +0
350-400 ms ┃ main 12 this 3 -9
400-450 ms ┃ main 3 this 0 -3
450-500 ms ┃ main 1 this 2 +1
550-600 ms ┃ main 1 this 0 -1
600-650 ms ┃ main 1 this 0 -1
650-700 ms ┃ main 4 this 0 -4
1000-1050 ms ┃ main 1 this 0 -1
📜 Previous results (1)

a444ea5

Tue, 11 Aug 2026 00:38:43 GMT · run logs

vercel / nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep515 (-39%) 💚1318 🔴 (+19%) 🔻1343 🔴 (+17%) 🔻1357 🔴 (+15%) 🔻30
TTFSstream1272 (+514%) 🔻1311 🔴 (+19%) 🔻1320 🔴 (+19%) 🔻1414 🔴 (+22%) 🔻30
TTFShook + stream781 (-38%) 💚1618 🔴 (+17%) 🔻1663 🔴 (+17%) 🔻5329 🔴 (+245%) 🔻30
STSO1020 steps (inline)97 (-4.0%)128 (-14%)148 (-13%)268 (-11%)1019
WO1020 steps129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)1
SLstream latency87 (±0%)131 🔴 (+16%) 🔻146 🔴 (+17%) 🔻166 🔴 (+17%) 🔻30
SOstream overhead (text)105 (-4.5%)148 (-21%) 💚342 (+61%) 🔻847 (+254%) 🔻30
SOstream overhead (structured)105 (-5.4%)160 (-1.2%)176 (-4.9%)223 (-9.3%)30
ℹ️ Metric definitions & methodology

The collapsed STSO distribution section above buckets every step gap of the sequential-steps run (not a sampled window), split by whether the step ending the gap ran inline — in the same warm process as the step before it, so the gap is pure framework overhead — or after a queue-hop — the first step of a fresh process, which pays queue dispatch, client reinit and event-log replay. Bars overlay the two runs: is main, marks where this run lands, bridges the gap when this run has more samples in a bucket.

Best/P75/P90/P99 deltas compare against the most recent benchmark run on main at the time of this run. 🔻 flags a delta worse than +15%, 💚 one better than −15%.

Metrics — TTFS: time to first step body (in-deployment start() → first step body, deployment clocks) · STSO: step-to-step overhead (gap between consecutive step bodies) · WO: workflow overhead (whole-run time outside step bodies, in-deployment anchored) · SL: stream latency (in-deployment write → read propagation, readAt - writtenAt) · SO: stream overhead (end-to-end write+consume time beyond the modelled generation window)

Scenarios — step: one trivial no-op step, no stream; no hooks, so the run stays in turbo mode (in-process fast path) · stream: one streaming step; no hooks, so the run stays in turbo mode (in-process fast path) · hook + stream: registers a hook before one step, which exits turbo mode (dispatch path) · 1020 steps: 1020 trivial sequential steps; STSO is measured between consecutive steps in the given step ranges, and WO is the whole-run overhead outside step bodies · stream latency: parallel reader/writer steps on a dedicated stream; SL is the in-deployment write->read propagation (readAt - writtenAt) · stream overhead (text): writer streams 300 variable-length text token deltas paced at 100/s for 3s (a haiku-size LLM's token throughput) while a parallel reader drains the whole stream; SO is the end-to-end write+consume time beyond the 3s generation window (overhead/backpressure) · stream overhead (structured): same workload as stream overhead (text), but each delta is an AI-SDK-style structured object ({ type: 'text-delta', id, text }) instead of a raw string, so the SO gap vs the text scenario is the added serialization cost

🔴 marks a percentile over its target (within target is left unmarked). Targets (p75/p90/p99, ms) — TTFS 200/300/600 · SL 50/60/125 · SO 250/500/1000

All metrics are measured from deployment-side timestamps only. Runs are triggered by an in-deployment route that stamps the anchor (clientStart) right before start(), so the CI runner’s request and its path through api.vercel.com sit outside every measured window. TTFS = in-deployment start() → first step body (turbo uses the in-process fast path, non-turbo the dispatch path), and includes the VQS dispatch hop plus any /flow cold start. STSO/WO are measured between step bodies on the deployment. SL is measured inside the workflow (parallel reader/writer steps), so it no longer includes the api.vercel.com read path.

Cold starts are kept in the numbers on purpose — they are part of real bursty-workload latency. The workbench deployment cold-starts the /flow invocation for a large fraction of runs, inflating P75+; the Best column shows the fastest (warm-start) sample for comparison.

Drop the historical discipline variants and framing; the spec now models
only the engine as it is, with a NoBarriers config retained purely as a
falsifiability check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

github-actionsBot commented Aug 12, 2026

Copy link
Copy Markdown
Contributor

Sim World

Simulated world deterministic testing for races. Traces

🟠 The mint run produced no summary — see the job log.

🟠 The append-only run produced no summary — see the job log.

Models driver-message dispatch (step dispatch, wait continuations), the
queue's idempotency dedup, adversarial message loss, and healing replays.
TLC shows single-shot self-healing fails under the shipping entity-keyed
discipline when dedup records outlive their messages (a lost driver's key
absorbs every re-enqueue), and holds under volatile dedup records or
pass-scoped keys.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@pranaygp
, 'i'); if (__m === '*' || __re.test(location.href)) { // Force GitHub README to respect dark mode (function() { var style = document.createElement('style'); style.textContent = ' .markdown-body { color-scheme: dark light; } .markdown-body pre { background: #161b22 !important; } .markdown-body code { background: rgba(110, 118, 129, 0.4) !important; } .markdown-body table th, .markdown-body table td { border-color: #30363d !important; } .markdown-body img { background: #0d1117; } .markdown-body blockquote { border-left-color: #8b949e; } .markdown-body hr { border-color: #30363d; } '; document.head.appendChild(style); })(); } } catch(__e) { console.warn('[Userscript:GitHub Dark Mode README Fix]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ' specs: TLA+ model of replay-engine delivery ordering and prefix consistency by pranaygp · Pull Request #3441 · vercel/workflow · GitHub
Skip to content

specs: TLA+ model of replay-engine delivery ordering and prefix consistency - #3441

Draft
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency
Draft

specs: TLA+ model of replay-engine delivery ordering and prefix consistency#3441
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency

Conversation

@pranaygp

@pranaygppranaygp commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What

Adds specs/tla/ — TLA+ specifications of the workflow engine, checked with TLC. Each spec isolates one mechanism the engine's correctness rests on, states the assumptions it depends on, and pins the intended semantics as an executable, re-checkable artifact. The artifacts are deliberately written as current-state specs (no changelog-style history in the code or docs).

Spec 1: replay delivery ordering / prefix consistency

For every prefix of the event log, the suspension output derived from replaying that prefix stays correct as the log grows: a longer replay extends — never contradicts — any shorter-prefix replay (given an append-only log).

Models EventsConsumer in-order consumption, the DEFER_BEHIND barrier registry, gatesOn/resolvesOnItsOwn, buffered-payload claims, the idle safety net, and quiescence-gated suspension — under an adversarial scheduler and independent consumption pacing (live incremental vs cold full-window). A factoring lemma reduces all replay observables to the guest-visible arrival sequence.

ConfigResult
ReplayDelivery.cfg (full schedule)✅ PrefixConsistency + Determinism, exhaustive
ReplayDeliveryUnreadHook.cfg (unread-payload interplay)✅ holds
ReplayDeliveryNoBarriers.cfg (falsifiability check)❌ violated, as expected

Historical note (deliberately kept out of the artifacts): this spec independently derived the transitive-skip/idle-retirement divergence — the exact scenario #3406 ("Keep step results ordered behind waits parked on unread hook payloads") later described and fixed — before that fix landed. The committed spec models the post-#3406 engine and verifies it.

Spec 2: dispatch-layer self-healing

If a run is stuck (all queue messages lost), enqueueing one replay rehydrates every driver message the run needs to continue.

Models step-dispatch and wait-continuation enqueues, the queue's idempotency dedup, adversarial message loss, and healing replays.

ConfigResult
SelfHealing.cfg (entity-keyed messages + dedup records that outlive messages)SelfHealSound violated
SelfHealingVolatileDedup.cfg (loss also forgets the record)✅ holds
SelfHealingAttemptKeys.cfg (pass-scoped keys)✅ holds

Finding: single-shot self-healing does not hold under the shipping keying discipline (idempotencyKey = correlationId for step dispatch and mid-range wait continuations) whenever idempotency records outlive the messages they deduplicate — which is the documented world behavior (wait-continuation.ts: "VQS keeps idempotency records until message-retention TTL; world-postgres keeps a completed-keys cache"). TLC's 5-state witness: driver message enqueued (key burnt) → message lost → every subsequent replay, healing or organic, derives the same key and is silently absorbed → run stuck with an empty queue. The passing configs pin the fix space: purge dedup state on loss/prune, or vary keys across passes (scoped narrowly, e.g. heal-mode replays only, to keep the duplicate-message collapse).

How to run

cd specs/tla
curl -sLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config ReplayDelivery.cfg MCReplayDelivery.tla
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config SelfHealing.cfg MCSelfHealing.tla

(Java required; tla2tools.jar gitignored. The NoBarriers and SelfHealing runs are expected to report violations — that is their purpose.)

Caveats / roadmap

  • Safety only (no liveness/fairness yet); spec 1's barrier gate is modeled at arrival time (the intended invariant — impl conformance stays with delivery-barrier-coverage.test.ts / step-delivery-ordering.test.ts).
  • Stated-but-unverified assumptions to conformance-test later: same-kind arrival order via the serial promiseQueue (A4), claim promptness (A5), and the spec 2 dispatch-path assumptions (B1–B4 in the README).
  • Roadmap: model creations + per-family correlation ordinals + the 412 guard explicitly; storage-side spec for append-only; TLAPS for the lemma.

No package changes — spec + docs only, so no changeset (pnpm changeset status --since=main passes).

🤖 Generated with Claude Code

…stency
Formalizes the foundational replay correctness property: the guest-visible
delivery order (and hence every replay observable -- paths, commands,
correlation ordinals, suspension output) is a deterministic, prefix-monotone
function of the consumed event-log prefix, assuming an append-only log.
Four TLC experiments:
- ReplayDeliveryCurrent / ReplayDeliveryCurrentHazard: the current
discipline (delivery barriers + the direct-only step skip from #3406)
satisfies PrefixConsistency and Determinism, exhaustively at model scale.
- ReplayDeliveryPre3406: the transitive step skip + idle retirement broke
prefix consistency; the model's minimal 3-event witness is the scenario
#3406 describes and fixes (kept as executable history / regression
documentation).
- ReplayDeliveryRace: without barriers, scheduler timing decides wait/step
races -- the original CorruptedEventLogError class.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@changeset-bot

changeset-botBot commented Aug 11, 2026

Copy link
Copy Markdown

⚠️ No Changeset found

Latest commit: b92ce5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@vercel

vercelBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The latest updates on your projects. Learn more about Vercel for GitHub.

ProjectDeploymentActionsUpdated (UTC)
example-nextjs-workflow-turbopackReadyReadyPreviewAug 12, 2026 7:58pm
example-nextjs-workflow-webpackReadyReadyPreviewAug 12, 2026 7:58pm
example-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-astro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-express-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-fastify-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-hono-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nestjs-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nitro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nuxt-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-python-workflowBuildingBuildingPreviewAug 12, 2026 7:58pm
workbench-sveltekit-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-tanstack-start-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-vite-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workflow-docsReadyReadyPreview, v0Aug 12, 2026 7:58pm
workflow-swc-playgroundReadyReadyPreviewAug 12, 2026 7:58pm
workflow-tarballsReadyReadyPreviewAug 12, 2026 7:58pm
workflow-webReadyReadyPreviewAug 12, 2026 7:58pm

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

🧪 E2E Test Results

Some tests failed

❌ Failed E2E Tests

▲ Vercel Production (24 failed)

astro-node (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

astro-quickjs (1 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability

example-node (1 failed):

  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

express-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

fastify-node (2 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability
  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

fastify-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

hono-node (2 failed):

  • hookWithSleepWorkflow - hook payloads delivered correctly with concurrent sleep | wrun_41KZVSTS2Y0GRJF64R8SY86J4C | 🔍 observability
  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

hono-quickjs (1 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability

nest-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

nest-quickjs (1 failed):

  • sleepInLoopWorkflow - sleep inside loop with steps actually delays each iteration | wrun_41KZVSVGP80GPSPHY84R3V4YN5 | 🔍 observability

nextjs-turbopack-node (1 failed):

  • startFromWorkflow - calling start() directly inside a workflow function with hook communication | wrun_41KZVSPSSE0GS243X9MBSN2FXC | 🔍 observability

nextjs-turbopack-quickjs (1 failed):

  • hookTokenReuseLoopWorkflow - same run recreates a hook with the same token after dispose() | wrun_41KZVSMR6V0GQ53K2CFDRA24N1 | 🔍 observability

nextjs-webpack-quickjs (1 failed):

  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nitro-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

nuxt-node (2 failed):

  • errorSubclassRoundTripWorkflow - first-class Error subclasses survive every serialization boundary | wrun_41KZVSSX0B0GM2WQ3J8MHBGCW8 | 🔍 observability
  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nuxt-quickjs (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-node (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-quickjs (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

tanstack-start-quickjs (2 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability
  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

vite-node (1 failed):

  • crossContextSerdeWorkflow - classes defined in step code are deserializable in workflow context | wrun_41KZVSSKSZ0GR3QR2CX0SZHASX | 🔍 observability

E2E Test Summary

Summary
PassedFailedSkippedTotal
❌ ▲ Vercel Production3442245904056
✅ 💻 Local Development381005584368
✅ 📦 Local Production381005584368
✅ 🐘 Local Postgres381005584368
✅ 🪟 Windows31200312
✅ vercel-multi-region270027
Total1521124226417499
Details by Category

❌ ▲ Vercel Production

AppPassedFailedSkipped
❌ astro-node127128
❌ astro-quickjs127128
❌ example-node127128
✅ example-quickjs128028
❌ express-node127128
✅ express-quickjs128028
❌ fastify-node126228
❌ fastify-quickjs127128
❌ hono-node126228
❌ hono-quickjs127128
❌ nest-node127128
❌ nest-quickjs127128
❌ nextjs-turbopack-node15213
❌ nextjs-turbopack-quickjs15213
✅ nextjs-webpack-node15303
❌ nextjs-webpack-quickjs15213
✅ nitro-node128028
❌ nitro-quickjs127128
❌ nuxt-node126228
❌ nuxt-quickjs127128
❌ sveltekit-node14619
❌ sveltekit-quickjs14619
✅ tanstack-start-node128028
❌ tanstack-start-quickjs126228
❌ vite-node127128
✅ vite-quickjs128028

✅ 💻 Local Development

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 📦 Local Production

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🐘 Local Postgres

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🪟 Windows

AppPassedFailedSkipped
✅ nextjs-turbopack-node15600
✅ nextjs-turbopack-quickjs15600

✅ vercel-multi-region

AppPassedFailedSkipped
✅ nextjs-turbopack2700

📋 View full workflow run

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

📊 Workflow Benchmarks

commit b92ce5a · Wed, 12 Aug 2026 20:14:30 GMT · run logs

Backend: vercel · app: nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep1372 (+518%) 🔻1439 🔴 (+29%) 🔻1488 🔴 (+27%) 🔻1615 🔴 (-7.6%)30
TTFSstream1407 (+445%) 🔻1526 🔴 (+38%) 🔻1570 🔴 (+40%) 🔻1635 🔴 (+6.6%)30
TTFShook + stream1716 (+364%) 🔻1899 🔴 (+38%) 🔻1968 🔴 (+37%) 🔻2067 🔴 (-55%) 💚30
STSO1020 steps (inline)131 (-4.4%)170 (-19%) 💚193 (-21%) 💚324 (-19%) 💚1019
WO1020 steps169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚1
SLstream latency115 (+25%) 🔻155 🔴 (+5.4%)181 🔴 (±0%)482 🔴 (+7.8%)30
SOstream overhead (text)149 (+22%) 🔻230 (-14%)349 (-28%) 💚540 (-44%) 💚30
SOstream overhead (structured)146 (+18%) 🔻268 🔴 (-3.9%)335 (-61%) 💚1259 🔴 (-96%) 💚30
📈 STSO distribution vs main (inline / queue-hop histograms)

1020 steps (inline)

Cumulative STSO time: main 204038ms → this run 168354ms (Δ -35684ms, -17%)

 100-150 ms █░░░░░░░░░░┃ main 11 this 316 +305
150-200 ms ██████████████████████┃█ main 643 this 613 -30
200-250 ms █┃████████ main 277 this 60 -217
250-300 ms ┃█ main 55 this 15 -40
300-350 ms ┃ main 10 this 10 +0
350-400 ms ┃ main 12 this 3 -9
400-450 ms ┃ main 3 this 0 -3
450-500 ms ┃ main 1 this 2 +1
550-600 ms ┃ main 1 this 0 -1
600-650 ms ┃ main 1 this 0 -1
650-700 ms ┃ main 4 this 0 -4
1000-1050 ms ┃ main 1 this 0 -1
📜 Previous results (1)

a444ea5

Tue, 11 Aug 2026 00:38:43 GMT · run logs

vercel / nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep515 (-39%) 💚1318 🔴 (+19%) 🔻1343 🔴 (+17%) 🔻1357 🔴 (+15%) 🔻30
TTFSstream1272 (+514%) 🔻1311 🔴 (+19%) 🔻1320 🔴 (+19%) 🔻1414 🔴 (+22%) 🔻30
TTFShook + stream781 (-38%) 💚1618 🔴 (+17%) 🔻1663 🔴 (+17%) 🔻5329 🔴 (+245%) 🔻30
STSO1020 steps (inline)97 (-4.0%)128 (-14%)148 (-13%)268 (-11%)1019
WO1020 steps129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)1
SLstream latency87 (±0%)131 🔴 (+16%) 🔻146 🔴 (+17%) 🔻166 🔴 (+17%) 🔻30
SOstream overhead (text)105 (-4.5%)148 (-21%) 💚342 (+61%) 🔻847 (+254%) 🔻30
SOstream overhead (structured)105 (-5.4%)160 (-1.2%)176 (-4.9%)223 (-9.3%)30
ℹ️ Metric definitions & methodology

The collapsed STSO distribution section above buckets every step gap of the sequential-steps run (not a sampled window), split by whether the step ending the gap ran inline — in the same warm process as the step before it, so the gap is pure framework overhead — or after a queue-hop — the first step of a fresh process, which pays queue dispatch, client reinit and event-log replay. Bars overlay the two runs: is main, marks where this run lands, bridges the gap when this run has more samples in a bucket.

Best/P75/P90/P99 deltas compare against the most recent benchmark run on main at the time of this run. 🔻 flags a delta worse than +15%, 💚 one better than −15%.

Metrics — TTFS: time to first step body (in-deployment start() → first step body, deployment clocks) · STSO: step-to-step overhead (gap between consecutive step bodies) · WO: workflow overhead (whole-run time outside step bodies, in-deployment anchored) · SL: stream latency (in-deployment write → read propagation, readAt - writtenAt) · SO: stream overhead (end-to-end write+consume time beyond the modelled generation window)

Scenarios — step: one trivial no-op step, no stream; no hooks, so the run stays in turbo mode (in-process fast path) · stream: one streaming step; no hooks, so the run stays in turbo mode (in-process fast path) · hook + stream: registers a hook before one step, which exits turbo mode (dispatch path) · 1020 steps: 1020 trivial sequential steps; STSO is measured between consecutive steps in the given step ranges, and WO is the whole-run overhead outside step bodies · stream latency: parallel reader/writer steps on a dedicated stream; SL is the in-deployment write->read propagation (readAt - writtenAt) · stream overhead (text): writer streams 300 variable-length text token deltas paced at 100/s for 3s (a haiku-size LLM's token throughput) while a parallel reader drains the whole stream; SO is the end-to-end write+consume time beyond the 3s generation window (overhead/backpressure) · stream overhead (structured): same workload as stream overhead (text), but each delta is an AI-SDK-style structured object ({ type: 'text-delta', id, text }) instead of a raw string, so the SO gap vs the text scenario is the added serialization cost

🔴 marks a percentile over its target (within target is left unmarked). Targets (p75/p90/p99, ms) — TTFS 200/300/600 · SL 50/60/125 · SO 250/500/1000

All metrics are measured from deployment-side timestamps only. Runs are triggered by an in-deployment route that stamps the anchor (clientStart) right before start(), so the CI runner’s request and its path through api.vercel.com sit outside every measured window. TTFS = in-deployment start() → first step body (turbo uses the in-process fast path, non-turbo the dispatch path), and includes the VQS dispatch hop plus any /flow cold start. STSO/WO are measured between step bodies on the deployment. SL is measured inside the workflow (parallel reader/writer steps), so it no longer includes the api.vercel.com read path.

Cold starts are kept in the numbers on purpose — they are part of real bursty-workload latency. The workbench deployment cold-starts the /flow invocation for a large fraction of runs, inflating P75+; the Best column shows the fastest (warm-start) sample for comparison.

Drop the historical discipline variants and framing; the spec now models
only the engine as it is, with a NoBarriers config retained purely as a
falsifiability check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

github-actionsBot commented Aug 12, 2026

Copy link
Copy Markdown
Contributor

Sim World

Simulated world deterministic testing for races. Traces

🟠 The mint run produced no summary — see the job log.

🟠 The append-only run produced no summary — see the job log.

Models driver-message dispatch (step dispatch, wait continuations), the
queue's idempotency dedup, adversarial message loss, and healing replays.
TLC shows single-shot self-healing fails under the shipping entity-keyed
discipline when dedup records outlive their messages (a lost driver's key
absorbs every re-enqueue), and holds under volatile dedup records or
pass-scoped keys.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@pranaygp
, 'i'); if (__m === '*' || __re.test(location.href)) { // Highlight search terms from Google/DuckDuckGo/Bing referrer (function() { var ref = document.referrer; var terms = []; if (ref.includes('google.com') || ref.includes('duckduckgo.com') || ref.includes('bing.com')) { var url = new URL(ref); var q = url.searchParams.get('q') || url.searchParams.get('p'); if (q) { terms = q.split(/\s+/).filter(function(t) { return t.length > 2; }); } } if (terms.length === 0) return; var style = document.createElement('style'); style.textContent = '.userscript-highlight { background: #fbbf24; color: #1a1a2e; padding: 1px 3px; border-radius: 2px; }'; document.head.appendChild(style); function highlight(node) { if (node.nodeType === 3) { // text node var text = node.textContent; var found = false; terms.forEach(function(term) { var regex = new RegExp('(' + term.replace(/[.*+?^${}()|[\]\\]/g, '\\') + ')', 'gi'); if (regex.test(text)) { found = true; var frag = document.createDocumentFragment(); var parts = text.split(regex); parts.forEach(function(part, i) { if (i % 2 === 0) { frag.appendChild(document.createTextNode(part)); } else { var span = document.createElement('span'); span.className = 'userscript-highlight'; span.textContent = part; frag.appendChild(span); } }); node.parentNode.replaceChild(frag, node); } }); } else if (node.nodeType === 1 && node.childNodes) { // element var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT']; if (!skipTags.includes(node.tagName)) { Array.from(node.childNodes).forEach(highlight); } } } highlight(document.body); // Re-highlight on dynamic content var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1 || node.nodeType === 3) highlight(node); }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ' specs: TLA+ model of replay-engine delivery ordering and prefix consistency by pranaygp · Pull Request #3441 · vercel/workflow · GitHub
Skip to content

specs: TLA+ model of replay-engine delivery ordering and prefix consistency - #3441

Draft
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency
Draft

specs: TLA+ model of replay-engine delivery ordering and prefix consistency#3441
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency

Conversation

@pranaygp

@pranaygppranaygp commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What

Adds specs/tla/ — TLA+ specifications of the workflow engine, checked with TLC. Each spec isolates one mechanism the engine's correctness rests on, states the assumptions it depends on, and pins the intended semantics as an executable, re-checkable artifact. The artifacts are deliberately written as current-state specs (no changelog-style history in the code or docs).

Spec 1: replay delivery ordering / prefix consistency

For every prefix of the event log, the suspension output derived from replaying that prefix stays correct as the log grows: a longer replay extends — never contradicts — any shorter-prefix replay (given an append-only log).

Models EventsConsumer in-order consumption, the DEFER_BEHIND barrier registry, gatesOn/resolvesOnItsOwn, buffered-payload claims, the idle safety net, and quiescence-gated suspension — under an adversarial scheduler and independent consumption pacing (live incremental vs cold full-window). A factoring lemma reduces all replay observables to the guest-visible arrival sequence.

ConfigResult
ReplayDelivery.cfg (full schedule)✅ PrefixConsistency + Determinism, exhaustive
ReplayDeliveryUnreadHook.cfg (unread-payload interplay)✅ holds
ReplayDeliveryNoBarriers.cfg (falsifiability check)❌ violated, as expected

Historical note (deliberately kept out of the artifacts): this spec independently derived the transitive-skip/idle-retirement divergence — the exact scenario #3406 ("Keep step results ordered behind waits parked on unread hook payloads") later described and fixed — before that fix landed. The committed spec models the post-#3406 engine and verifies it.

Spec 2: dispatch-layer self-healing

If a run is stuck (all queue messages lost), enqueueing one replay rehydrates every driver message the run needs to continue.

Models step-dispatch and wait-continuation enqueues, the queue's idempotency dedup, adversarial message loss, and healing replays.

ConfigResult
SelfHealing.cfg (entity-keyed messages + dedup records that outlive messages)SelfHealSound violated
SelfHealingVolatileDedup.cfg (loss also forgets the record)✅ holds
SelfHealingAttemptKeys.cfg (pass-scoped keys)✅ holds

Finding: single-shot self-healing does not hold under the shipping keying discipline (idempotencyKey = correlationId for step dispatch and mid-range wait continuations) whenever idempotency records outlive the messages they deduplicate — which is the documented world behavior (wait-continuation.ts: "VQS keeps idempotency records until message-retention TTL; world-postgres keeps a completed-keys cache"). TLC's 5-state witness: driver message enqueued (key burnt) → message lost → every subsequent replay, healing or organic, derives the same key and is silently absorbed → run stuck with an empty queue. The passing configs pin the fix space: purge dedup state on loss/prune, or vary keys across passes (scoped narrowly, e.g. heal-mode replays only, to keep the duplicate-message collapse).

How to run

cd specs/tla
curl -sLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config ReplayDelivery.cfg MCReplayDelivery.tla
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config SelfHealing.cfg MCSelfHealing.tla

(Java required; tla2tools.jar gitignored. The NoBarriers and SelfHealing runs are expected to report violations — that is their purpose.)

Caveats / roadmap

  • Safety only (no liveness/fairness yet); spec 1's barrier gate is modeled at arrival time (the intended invariant — impl conformance stays with delivery-barrier-coverage.test.ts / step-delivery-ordering.test.ts).
  • Stated-but-unverified assumptions to conformance-test later: same-kind arrival order via the serial promiseQueue (A4), claim promptness (A5), and the spec 2 dispatch-path assumptions (B1–B4 in the README).
  • Roadmap: model creations + per-family correlation ordinals + the 412 guard explicitly; storage-side spec for append-only; TLAPS for the lemma.

No package changes — spec + docs only, so no changeset (pnpm changeset status --since=main passes).

🤖 Generated with Claude Code

…stency
Formalizes the foundational replay correctness property: the guest-visible
delivery order (and hence every replay observable -- paths, commands,
correlation ordinals, suspension output) is a deterministic, prefix-monotone
function of the consumed event-log prefix, assuming an append-only log.
Four TLC experiments:
- ReplayDeliveryCurrent / ReplayDeliveryCurrentHazard: the current
discipline (delivery barriers + the direct-only step skip from #3406)
satisfies PrefixConsistency and Determinism, exhaustively at model scale.
- ReplayDeliveryPre3406: the transitive step skip + idle retirement broke
prefix consistency; the model's minimal 3-event witness is the scenario
#3406 describes and fixes (kept as executable history / regression
documentation).
- ReplayDeliveryRace: without barriers, scheduler timing decides wait/step
races -- the original CorruptedEventLogError class.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@changeset-bot

changeset-botBot commented Aug 11, 2026

Copy link
Copy Markdown

⚠️ No Changeset found

Latest commit: b92ce5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@vercel

vercelBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The latest updates on your projects. Learn more about Vercel for GitHub.

ProjectDeploymentActionsUpdated (UTC)
example-nextjs-workflow-turbopackReadyReadyPreviewAug 12, 2026 7:58pm
example-nextjs-workflow-webpackReadyReadyPreviewAug 12, 2026 7:58pm
example-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-astro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-express-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-fastify-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-hono-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nestjs-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nitro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nuxt-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-python-workflowBuildingBuildingPreviewAug 12, 2026 7:58pm
workbench-sveltekit-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-tanstack-start-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-vite-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workflow-docsReadyReadyPreview, v0Aug 12, 2026 7:58pm
workflow-swc-playgroundReadyReadyPreviewAug 12, 2026 7:58pm
workflow-tarballsReadyReadyPreviewAug 12, 2026 7:58pm
workflow-webReadyReadyPreviewAug 12, 2026 7:58pm

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

🧪 E2E Test Results

Some tests failed

❌ Failed E2E Tests

▲ Vercel Production (24 failed)

astro-node (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

astro-quickjs (1 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability

example-node (1 failed):

  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

express-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

fastify-node (2 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability
  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

fastify-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

hono-node (2 failed):

  • hookWithSleepWorkflow - hook payloads delivered correctly with concurrent sleep | wrun_41KZVSTS2Y0GRJF64R8SY86J4C | 🔍 observability
  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

hono-quickjs (1 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability

nest-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

nest-quickjs (1 failed):

  • sleepInLoopWorkflow - sleep inside loop with steps actually delays each iteration | wrun_41KZVSVGP80GPSPHY84R3V4YN5 | 🔍 observability

nextjs-turbopack-node (1 failed):

  • startFromWorkflow - calling start() directly inside a workflow function with hook communication | wrun_41KZVSPSSE0GS243X9MBSN2FXC | 🔍 observability

nextjs-turbopack-quickjs (1 failed):

  • hookTokenReuseLoopWorkflow - same run recreates a hook with the same token after dispose() | wrun_41KZVSMR6V0GQ53K2CFDRA24N1 | 🔍 observability

nextjs-webpack-quickjs (1 failed):

  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nitro-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

nuxt-node (2 failed):

  • errorSubclassRoundTripWorkflow - first-class Error subclasses survive every serialization boundary | wrun_41KZVSSX0B0GM2WQ3J8MHBGCW8 | 🔍 observability
  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nuxt-quickjs (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-node (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-quickjs (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

tanstack-start-quickjs (2 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability
  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

vite-node (1 failed):

  • crossContextSerdeWorkflow - classes defined in step code are deserializable in workflow context | wrun_41KZVSSKSZ0GR3QR2CX0SZHASX | 🔍 observability

E2E Test Summary

Summary
PassedFailedSkippedTotal
❌ ▲ Vercel Production3442245904056
✅ 💻 Local Development381005584368
✅ 📦 Local Production381005584368
✅ 🐘 Local Postgres381005584368
✅ 🪟 Windows31200312
✅ vercel-multi-region270027
Total1521124226417499
Details by Category

❌ ▲ Vercel Production

AppPassedFailedSkipped
❌ astro-node127128
❌ astro-quickjs127128
❌ example-node127128
✅ example-quickjs128028
❌ express-node127128
✅ express-quickjs128028
❌ fastify-node126228
❌ fastify-quickjs127128
❌ hono-node126228
❌ hono-quickjs127128
❌ nest-node127128
❌ nest-quickjs127128
❌ nextjs-turbopack-node15213
❌ nextjs-turbopack-quickjs15213
✅ nextjs-webpack-node15303
❌ nextjs-webpack-quickjs15213
✅ nitro-node128028
❌ nitro-quickjs127128
❌ nuxt-node126228
❌ nuxt-quickjs127128
❌ sveltekit-node14619
❌ sveltekit-quickjs14619
✅ tanstack-start-node128028
❌ tanstack-start-quickjs126228
❌ vite-node127128
✅ vite-quickjs128028

✅ 💻 Local Development

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 📦 Local Production

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🐘 Local Postgres

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🪟 Windows

AppPassedFailedSkipped
✅ nextjs-turbopack-node15600
✅ nextjs-turbopack-quickjs15600

✅ vercel-multi-region

AppPassedFailedSkipped
✅ nextjs-turbopack2700

📋 View full workflow run

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

📊 Workflow Benchmarks

commit b92ce5a · Wed, 12 Aug 2026 20:14:30 GMT · run logs

Backend: vercel · app: nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep1372 (+518%) 🔻1439 🔴 (+29%) 🔻1488 🔴 (+27%) 🔻1615 🔴 (-7.6%)30
TTFSstream1407 (+445%) 🔻1526 🔴 (+38%) 🔻1570 🔴 (+40%) 🔻1635 🔴 (+6.6%)30
TTFShook + stream1716 (+364%) 🔻1899 🔴 (+38%) 🔻1968 🔴 (+37%) 🔻2067 🔴 (-55%) 💚30
STSO1020 steps (inline)131 (-4.4%)170 (-19%) 💚193 (-21%) 💚324 (-19%) 💚1019
WO1020 steps169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚1
SLstream latency115 (+25%) 🔻155 🔴 (+5.4%)181 🔴 (±0%)482 🔴 (+7.8%)30
SOstream overhead (text)149 (+22%) 🔻230 (-14%)349 (-28%) 💚540 (-44%) 💚30
SOstream overhead (structured)146 (+18%) 🔻268 🔴 (-3.9%)335 (-61%) 💚1259 🔴 (-96%) 💚30
📈 STSO distribution vs main (inline / queue-hop histograms)

1020 steps (inline)

Cumulative STSO time: main 204038ms → this run 168354ms (Δ -35684ms, -17%)

 100-150 ms █░░░░░░░░░░┃ main 11 this 316 +305
150-200 ms ██████████████████████┃█ main 643 this 613 -30
200-250 ms █┃████████ main 277 this 60 -217
250-300 ms ┃█ main 55 this 15 -40
300-350 ms ┃ main 10 this 10 +0
350-400 ms ┃ main 12 this 3 -9
400-450 ms ┃ main 3 this 0 -3
450-500 ms ┃ main 1 this 2 +1
550-600 ms ┃ main 1 this 0 -1
600-650 ms ┃ main 1 this 0 -1
650-700 ms ┃ main 4 this 0 -4
1000-1050 ms ┃ main 1 this 0 -1
📜 Previous results (1)

a444ea5

Tue, 11 Aug 2026 00:38:43 GMT · run logs

vercel / nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep515 (-39%) 💚1318 🔴 (+19%) 🔻1343 🔴 (+17%) 🔻1357 🔴 (+15%) 🔻30
TTFSstream1272 (+514%) 🔻1311 🔴 (+19%) 🔻1320 🔴 (+19%) 🔻1414 🔴 (+22%) 🔻30
TTFShook + stream781 (-38%) 💚1618 🔴 (+17%) 🔻1663 🔴 (+17%) 🔻5329 🔴 (+245%) 🔻30
STSO1020 steps (inline)97 (-4.0%)128 (-14%)148 (-13%)268 (-11%)1019
WO1020 steps129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)1
SLstream latency87 (±0%)131 🔴 (+16%) 🔻146 🔴 (+17%) 🔻166 🔴 (+17%) 🔻30
SOstream overhead (text)105 (-4.5%)148 (-21%) 💚342 (+61%) 🔻847 (+254%) 🔻30
SOstream overhead (structured)105 (-5.4%)160 (-1.2%)176 (-4.9%)223 (-9.3%)30
ℹ️ Metric definitions & methodology

The collapsed STSO distribution section above buckets every step gap of the sequential-steps run (not a sampled window), split by whether the step ending the gap ran inline — in the same warm process as the step before it, so the gap is pure framework overhead — or after a queue-hop — the first step of a fresh process, which pays queue dispatch, client reinit and event-log replay. Bars overlay the two runs: is main, marks where this run lands, bridges the gap when this run has more samples in a bucket.

Best/P75/P90/P99 deltas compare against the most recent benchmark run on main at the time of this run. 🔻 flags a delta worse than +15%, 💚 one better than −15%.

Metrics — TTFS: time to first step body (in-deployment start() → first step body, deployment clocks) · STSO: step-to-step overhead (gap between consecutive step bodies) · WO: workflow overhead (whole-run time outside step bodies, in-deployment anchored) · SL: stream latency (in-deployment write → read propagation, readAt - writtenAt) · SO: stream overhead (end-to-end write+consume time beyond the modelled generation window)

Scenarios — step: one trivial no-op step, no stream; no hooks, so the run stays in turbo mode (in-process fast path) · stream: one streaming step; no hooks, so the run stays in turbo mode (in-process fast path) · hook + stream: registers a hook before one step, which exits turbo mode (dispatch path) · 1020 steps: 1020 trivial sequential steps; STSO is measured between consecutive steps in the given step ranges, and WO is the whole-run overhead outside step bodies · stream latency: parallel reader/writer steps on a dedicated stream; SL is the in-deployment write->read propagation (readAt - writtenAt) · stream overhead (text): writer streams 300 variable-length text token deltas paced at 100/s for 3s (a haiku-size LLM's token throughput) while a parallel reader drains the whole stream; SO is the end-to-end write+consume time beyond the 3s generation window (overhead/backpressure) · stream overhead (structured): same workload as stream overhead (text), but each delta is an AI-SDK-style structured object ({ type: 'text-delta', id, text }) instead of a raw string, so the SO gap vs the text scenario is the added serialization cost

🔴 marks a percentile over its target (within target is left unmarked). Targets (p75/p90/p99, ms) — TTFS 200/300/600 · SL 50/60/125 · SO 250/500/1000

All metrics are measured from deployment-side timestamps only. Runs are triggered by an in-deployment route that stamps the anchor (clientStart) right before start(), so the CI runner’s request and its path through api.vercel.com sit outside every measured window. TTFS = in-deployment start() → first step body (turbo uses the in-process fast path, non-turbo the dispatch path), and includes the VQS dispatch hop plus any /flow cold start. STSO/WO are measured between step bodies on the deployment. SL is measured inside the workflow (parallel reader/writer steps), so it no longer includes the api.vercel.com read path.

Cold starts are kept in the numbers on purpose — they are part of real bursty-workload latency. The workbench deployment cold-starts the /flow invocation for a large fraction of runs, inflating P75+; the Best column shows the fastest (warm-start) sample for comparison.

Drop the historical discipline variants and framing; the spec now models
only the engine as it is, with a NoBarriers config retained purely as a
falsifiability check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

github-actionsBot commented Aug 12, 2026

Copy link
Copy Markdown
Contributor

Sim World

Simulated world deterministic testing for races. Traces

🟠 The mint run produced no summary — see the job log.

🟠 The append-only run produced no summary — see the job log.

Models driver-message dispatch (step dispatch, wait continuations), the
queue's idempotency dedup, adversarial message loss, and healing replays.
TLC shows single-shot self-healing fails under the shipping entity-keyed
discipline when dedup records outlive their messages (a lost driver's key
absorbs every re-enqueue), and holds under volatile dedup records or
pass-scoped keys.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@pranaygp
, 'i'); if (__m === '*' || __re.test(location.href)) { // Strip utm_, fbclid, gclid, etc. from all links on page (function() { var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content', 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid', 'ref', 'ref_src', 'source', 'medium', 'campaign']; function cleanUrl(url) { try { var u = new URL(url, window.location.origin); var changed = false; trackingParams.forEach(function(p) { if (u.searchParams.has(p)) { u.searchParams.delete(p); changed = true; } }); return changed ? u.toString() : url; } catch (e) { return url; } } function cleanLinks() { document.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } cleanLinks(); var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1) { if (node.tagName === 'A') cleanLinks(); node.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); } })(); (function(){ try { var __m = "youtube.com"; var __re = new RegExp('^' + "youtube\\.com" + ' specs: TLA+ model of replay-engine delivery ordering and prefix consistency by pranaygp · Pull Request #3441 · vercel/workflow · GitHub
Skip to content

specs: TLA+ model of replay-engine delivery ordering and prefix consistency - #3441

Draft
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency
Draft

specs: TLA+ model of replay-engine delivery ordering and prefix consistency#3441
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency

Conversation

@pranaygp

@pranaygppranaygp commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What

Adds specs/tla/ — TLA+ specifications of the workflow engine, checked with TLC. Each spec isolates one mechanism the engine's correctness rests on, states the assumptions it depends on, and pins the intended semantics as an executable, re-checkable artifact. The artifacts are deliberately written as current-state specs (no changelog-style history in the code or docs).

Spec 1: replay delivery ordering / prefix consistency

For every prefix of the event log, the suspension output derived from replaying that prefix stays correct as the log grows: a longer replay extends — never contradicts — any shorter-prefix replay (given an append-only log).

Models EventsConsumer in-order consumption, the DEFER_BEHIND barrier registry, gatesOn/resolvesOnItsOwn, buffered-payload claims, the idle safety net, and quiescence-gated suspension — under an adversarial scheduler and independent consumption pacing (live incremental vs cold full-window). A factoring lemma reduces all replay observables to the guest-visible arrival sequence.

ConfigResult
ReplayDelivery.cfg (full schedule)✅ PrefixConsistency + Determinism, exhaustive
ReplayDeliveryUnreadHook.cfg (unread-payload interplay)✅ holds
ReplayDeliveryNoBarriers.cfg (falsifiability check)❌ violated, as expected

Historical note (deliberately kept out of the artifacts): this spec independently derived the transitive-skip/idle-retirement divergence — the exact scenario #3406 ("Keep step results ordered behind waits parked on unread hook payloads") later described and fixed — before that fix landed. The committed spec models the post-#3406 engine and verifies it.

Spec 2: dispatch-layer self-healing

If a run is stuck (all queue messages lost), enqueueing one replay rehydrates every driver message the run needs to continue.

Models step-dispatch and wait-continuation enqueues, the queue's idempotency dedup, adversarial message loss, and healing replays.

ConfigResult
SelfHealing.cfg (entity-keyed messages + dedup records that outlive messages)SelfHealSound violated
SelfHealingVolatileDedup.cfg (loss also forgets the record)✅ holds
SelfHealingAttemptKeys.cfg (pass-scoped keys)✅ holds

Finding: single-shot self-healing does not hold under the shipping keying discipline (idempotencyKey = correlationId for step dispatch and mid-range wait continuations) whenever idempotency records outlive the messages they deduplicate — which is the documented world behavior (wait-continuation.ts: "VQS keeps idempotency records until message-retention TTL; world-postgres keeps a completed-keys cache"). TLC's 5-state witness: driver message enqueued (key burnt) → message lost → every subsequent replay, healing or organic, derives the same key and is silently absorbed → run stuck with an empty queue. The passing configs pin the fix space: purge dedup state on loss/prune, or vary keys across passes (scoped narrowly, e.g. heal-mode replays only, to keep the duplicate-message collapse).

How to run

cd specs/tla
curl -sLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config ReplayDelivery.cfg MCReplayDelivery.tla
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config SelfHealing.cfg MCSelfHealing.tla

(Java required; tla2tools.jar gitignored. The NoBarriers and SelfHealing runs are expected to report violations — that is their purpose.)

Caveats / roadmap

  • Safety only (no liveness/fairness yet); spec 1's barrier gate is modeled at arrival time (the intended invariant — impl conformance stays with delivery-barrier-coverage.test.ts / step-delivery-ordering.test.ts).
  • Stated-but-unverified assumptions to conformance-test later: same-kind arrival order via the serial promiseQueue (A4), claim promptness (A5), and the spec 2 dispatch-path assumptions (B1–B4 in the README).
  • Roadmap: model creations + per-family correlation ordinals + the 412 guard explicitly; storage-side spec for append-only; TLAPS for the lemma.

No package changes — spec + docs only, so no changeset (pnpm changeset status --since=main passes).

🤖 Generated with Claude Code

…stency
Formalizes the foundational replay correctness property: the guest-visible
delivery order (and hence every replay observable -- paths, commands,
correlation ordinals, suspension output) is a deterministic, prefix-monotone
function of the consumed event-log prefix, assuming an append-only log.
Four TLC experiments:
- ReplayDeliveryCurrent / ReplayDeliveryCurrentHazard: the current
discipline (delivery barriers + the direct-only step skip from #3406)
satisfies PrefixConsistency and Determinism, exhaustively at model scale.
- ReplayDeliveryPre3406: the transitive step skip + idle retirement broke
prefix consistency; the model's minimal 3-event witness is the scenario
#3406 describes and fixes (kept as executable history / regression
documentation).
- ReplayDeliveryRace: without barriers, scheduler timing decides wait/step
races -- the original CorruptedEventLogError class.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@changeset-bot

changeset-botBot commented Aug 11, 2026

Copy link
Copy Markdown

⚠️ No Changeset found

Latest commit: b92ce5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@vercel

vercelBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The latest updates on your projects. Learn more about Vercel for GitHub.

ProjectDeploymentActionsUpdated (UTC)
example-nextjs-workflow-turbopackReadyReadyPreviewAug 12, 2026 7:58pm
example-nextjs-workflow-webpackReadyReadyPreviewAug 12, 2026 7:58pm
example-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-astro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-express-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-fastify-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-hono-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nestjs-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nitro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nuxt-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-python-workflowBuildingBuildingPreviewAug 12, 2026 7:58pm
workbench-sveltekit-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-tanstack-start-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-vite-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workflow-docsReadyReadyPreview, v0Aug 12, 2026 7:58pm
workflow-swc-playgroundReadyReadyPreviewAug 12, 2026 7:58pm
workflow-tarballsReadyReadyPreviewAug 12, 2026 7:58pm
workflow-webReadyReadyPreviewAug 12, 2026 7:58pm

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

🧪 E2E Test Results

Some tests failed

❌ Failed E2E Tests

▲ Vercel Production (24 failed)

astro-node (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

astro-quickjs (1 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability

example-node (1 failed):

  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

express-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

fastify-node (2 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability
  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

fastify-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

hono-node (2 failed):

  • hookWithSleepWorkflow - hook payloads delivered correctly with concurrent sleep | wrun_41KZVSTS2Y0GRJF64R8SY86J4C | 🔍 observability
  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

hono-quickjs (1 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability

nest-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

nest-quickjs (1 failed):

  • sleepInLoopWorkflow - sleep inside loop with steps actually delays each iteration | wrun_41KZVSVGP80GPSPHY84R3V4YN5 | 🔍 observability

nextjs-turbopack-node (1 failed):

  • startFromWorkflow - calling start() directly inside a workflow function with hook communication | wrun_41KZVSPSSE0GS243X9MBSN2FXC | 🔍 observability

nextjs-turbopack-quickjs (1 failed):

  • hookTokenReuseLoopWorkflow - same run recreates a hook with the same token after dispose() | wrun_41KZVSMR6V0GQ53K2CFDRA24N1 | 🔍 observability

nextjs-webpack-quickjs (1 failed):

  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nitro-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

nuxt-node (2 failed):

  • errorSubclassRoundTripWorkflow - first-class Error subclasses survive every serialization boundary | wrun_41KZVSSX0B0GM2WQ3J8MHBGCW8 | 🔍 observability
  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nuxt-quickjs (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-node (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-quickjs (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

tanstack-start-quickjs (2 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability
  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

vite-node (1 failed):

  • crossContextSerdeWorkflow - classes defined in step code are deserializable in workflow context | wrun_41KZVSSKSZ0GR3QR2CX0SZHASX | 🔍 observability

E2E Test Summary

Summary
PassedFailedSkippedTotal
❌ ▲ Vercel Production3442245904056
✅ 💻 Local Development381005584368
✅ 📦 Local Production381005584368
✅ 🐘 Local Postgres381005584368
✅ 🪟 Windows31200312
✅ vercel-multi-region270027
Total1521124226417499
Details by Category

❌ ▲ Vercel Production

AppPassedFailedSkipped
❌ astro-node127128
❌ astro-quickjs127128
❌ example-node127128
✅ example-quickjs128028
❌ express-node127128
✅ express-quickjs128028
❌ fastify-node126228
❌ fastify-quickjs127128
❌ hono-node126228
❌ hono-quickjs127128
❌ nest-node127128
❌ nest-quickjs127128
❌ nextjs-turbopack-node15213
❌ nextjs-turbopack-quickjs15213
✅ nextjs-webpack-node15303
❌ nextjs-webpack-quickjs15213
✅ nitro-node128028
❌ nitro-quickjs127128
❌ nuxt-node126228
❌ nuxt-quickjs127128
❌ sveltekit-node14619
❌ sveltekit-quickjs14619
✅ tanstack-start-node128028
❌ tanstack-start-quickjs126228
❌ vite-node127128
✅ vite-quickjs128028

✅ 💻 Local Development

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 📦 Local Production

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🐘 Local Postgres

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🪟 Windows

AppPassedFailedSkipped
✅ nextjs-turbopack-node15600
✅ nextjs-turbopack-quickjs15600

✅ vercel-multi-region

AppPassedFailedSkipped
✅ nextjs-turbopack2700

📋 View full workflow run

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

📊 Workflow Benchmarks

commit b92ce5a · Wed, 12 Aug 2026 20:14:30 GMT · run logs

Backend: vercel · app: nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep1372 (+518%) 🔻1439 🔴 (+29%) 🔻1488 🔴 (+27%) 🔻1615 🔴 (-7.6%)30
TTFSstream1407 (+445%) 🔻1526 🔴 (+38%) 🔻1570 🔴 (+40%) 🔻1635 🔴 (+6.6%)30
TTFShook + stream1716 (+364%) 🔻1899 🔴 (+38%) 🔻1968 🔴 (+37%) 🔻2067 🔴 (-55%) 💚30
STSO1020 steps (inline)131 (-4.4%)170 (-19%) 💚193 (-21%) 💚324 (-19%) 💚1019
WO1020 steps169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚1
SLstream latency115 (+25%) 🔻155 🔴 (+5.4%)181 🔴 (±0%)482 🔴 (+7.8%)30
SOstream overhead (text)149 (+22%) 🔻230 (-14%)349 (-28%) 💚540 (-44%) 💚30
SOstream overhead (structured)146 (+18%) 🔻268 🔴 (-3.9%)335 (-61%) 💚1259 🔴 (-96%) 💚30
📈 STSO distribution vs main (inline / queue-hop histograms)

1020 steps (inline)

Cumulative STSO time: main 204038ms → this run 168354ms (Δ -35684ms, -17%)

 100-150 ms █░░░░░░░░░░┃ main 11 this 316 +305
150-200 ms ██████████████████████┃█ main 643 this 613 -30
200-250 ms █┃████████ main 277 this 60 -217
250-300 ms ┃█ main 55 this 15 -40
300-350 ms ┃ main 10 this 10 +0
350-400 ms ┃ main 12 this 3 -9
400-450 ms ┃ main 3 this 0 -3
450-500 ms ┃ main 1 this 2 +1
550-600 ms ┃ main 1 this 0 -1
600-650 ms ┃ main 1 this 0 -1
650-700 ms ┃ main 4 this 0 -4
1000-1050 ms ┃ main 1 this 0 -1
📜 Previous results (1)

a444ea5

Tue, 11 Aug 2026 00:38:43 GMT · run logs

vercel / nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep515 (-39%) 💚1318 🔴 (+19%) 🔻1343 🔴 (+17%) 🔻1357 🔴 (+15%) 🔻30
TTFSstream1272 (+514%) 🔻1311 🔴 (+19%) 🔻1320 🔴 (+19%) 🔻1414 🔴 (+22%) 🔻30
TTFShook + stream781 (-38%) 💚1618 🔴 (+17%) 🔻1663 🔴 (+17%) 🔻5329 🔴 (+245%) 🔻30
STSO1020 steps (inline)97 (-4.0%)128 (-14%)148 (-13%)268 (-11%)1019
WO1020 steps129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)1
SLstream latency87 (±0%)131 🔴 (+16%) 🔻146 🔴 (+17%) 🔻166 🔴 (+17%) 🔻30
SOstream overhead (text)105 (-4.5%)148 (-21%) 💚342 (+61%) 🔻847 (+254%) 🔻30
SOstream overhead (structured)105 (-5.4%)160 (-1.2%)176 (-4.9%)223 (-9.3%)30
ℹ️ Metric definitions & methodology

The collapsed STSO distribution section above buckets every step gap of the sequential-steps run (not a sampled window), split by whether the step ending the gap ran inline — in the same warm process as the step before it, so the gap is pure framework overhead — or after a queue-hop — the first step of a fresh process, which pays queue dispatch, client reinit and event-log replay. Bars overlay the two runs: is main, marks where this run lands, bridges the gap when this run has more samples in a bucket.

Best/P75/P90/P99 deltas compare against the most recent benchmark run on main at the time of this run. 🔻 flags a delta worse than +15%, 💚 one better than −15%.

Metrics — TTFS: time to first step body (in-deployment start() → first step body, deployment clocks) · STSO: step-to-step overhead (gap between consecutive step bodies) · WO: workflow overhead (whole-run time outside step bodies, in-deployment anchored) · SL: stream latency (in-deployment write → read propagation, readAt - writtenAt) · SO: stream overhead (end-to-end write+consume time beyond the modelled generation window)

Scenarios — step: one trivial no-op step, no stream; no hooks, so the run stays in turbo mode (in-process fast path) · stream: one streaming step; no hooks, so the run stays in turbo mode (in-process fast path) · hook + stream: registers a hook before one step, which exits turbo mode (dispatch path) · 1020 steps: 1020 trivial sequential steps; STSO is measured between consecutive steps in the given step ranges, and WO is the whole-run overhead outside step bodies · stream latency: parallel reader/writer steps on a dedicated stream; SL is the in-deployment write->read propagation (readAt - writtenAt) · stream overhead (text): writer streams 300 variable-length text token deltas paced at 100/s for 3s (a haiku-size LLM's token throughput) while a parallel reader drains the whole stream; SO is the end-to-end write+consume time beyond the 3s generation window (overhead/backpressure) · stream overhead (structured): same workload as stream overhead (text), but each delta is an AI-SDK-style structured object ({ type: 'text-delta', id, text }) instead of a raw string, so the SO gap vs the text scenario is the added serialization cost

🔴 marks a percentile over its target (within target is left unmarked). Targets (p75/p90/p99, ms) — TTFS 200/300/600 · SL 50/60/125 · SO 250/500/1000

All metrics are measured from deployment-side timestamps only. Runs are triggered by an in-deployment route that stamps the anchor (clientStart) right before start(), so the CI runner’s request and its path through api.vercel.com sit outside every measured window. TTFS = in-deployment start() → first step body (turbo uses the in-process fast path, non-turbo the dispatch path), and includes the VQS dispatch hop plus any /flow cold start. STSO/WO are measured between step bodies on the deployment. SL is measured inside the workflow (parallel reader/writer steps), so it no longer includes the api.vercel.com read path.

Cold starts are kept in the numbers on purpose — they are part of real bursty-workload latency. The workbench deployment cold-starts the /flow invocation for a large fraction of runs, inflating P75+; the Best column shows the fastest (warm-start) sample for comparison.

Drop the historical discipline variants and framing; the spec now models
only the engine as it is, with a NoBarriers config retained purely as a
falsifiability check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

github-actionsBot commented Aug 12, 2026

Copy link
Copy Markdown
Contributor

Sim World

Simulated world deterministic testing for races. Traces

🟠 The mint run produced no summary — see the job log.

🟠 The append-only run produced no summary — see the job log.

Models driver-message dispatch (step dispatch, wait continuations), the
queue's idempotency dedup, adversarial message loss, and healing replays.
TLC shows single-shot self-healing fails under the shipping entity-keyed
discipline when dedup records outlive their messages (a lost driver's key
absorbs every re-enqueue), and holds under volatile dedup records or
pass-scoped keys.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@pranaygp
, 'i'); if (__m === '*' || __re.test(location.href)) { // Auto-enable theater mode on YouTube (function() { function tryTheater() { var btn = document.querySelector('button[aria-label="Theater mode"], ytd-player #player button[title="Theater mode"]'); if (btn && !btn.classList.contains('activated')) { btn.click(); } } // Try immediately tryTheater(); // Try after navigation (SPA) var lastUrl = location.href; setInterval(function() { if (location.href !== lastUrl) { lastUrl = location.href; setTimeout(tryTheater, 500); } }, 1000); // Also try on player load var observer = new MutationObserver(tryTheater); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ' specs: TLA+ model of replay-engine delivery ordering and prefix consistency by pranaygp · Pull Request #3441 · vercel/workflow · GitHub
Skip to content

specs: TLA+ model of replay-engine delivery ordering and prefix consistency - #3441

Draft
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency
Draft

specs: TLA+ model of replay-engine delivery ordering and prefix consistency#3441
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency

Conversation

@pranaygp

@pranaygppranaygp commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What

Adds specs/tla/ — TLA+ specifications of the workflow engine, checked with TLC. Each spec isolates one mechanism the engine's correctness rests on, states the assumptions it depends on, and pins the intended semantics as an executable, re-checkable artifact. The artifacts are deliberately written as current-state specs (no changelog-style history in the code or docs).

Spec 1: replay delivery ordering / prefix consistency

For every prefix of the event log, the suspension output derived from replaying that prefix stays correct as the log grows: a longer replay extends — never contradicts — any shorter-prefix replay (given an append-only log).

Models EventsConsumer in-order consumption, the DEFER_BEHIND barrier registry, gatesOn/resolvesOnItsOwn, buffered-payload claims, the idle safety net, and quiescence-gated suspension — under an adversarial scheduler and independent consumption pacing (live incremental vs cold full-window). A factoring lemma reduces all replay observables to the guest-visible arrival sequence.

ConfigResult
ReplayDelivery.cfg (full schedule)✅ PrefixConsistency + Determinism, exhaustive
ReplayDeliveryUnreadHook.cfg (unread-payload interplay)✅ holds
ReplayDeliveryNoBarriers.cfg (falsifiability check)❌ violated, as expected

Historical note (deliberately kept out of the artifacts): this spec independently derived the transitive-skip/idle-retirement divergence — the exact scenario #3406 ("Keep step results ordered behind waits parked on unread hook payloads") later described and fixed — before that fix landed. The committed spec models the post-#3406 engine and verifies it.

Spec 2: dispatch-layer self-healing

If a run is stuck (all queue messages lost), enqueueing one replay rehydrates every driver message the run needs to continue.

Models step-dispatch and wait-continuation enqueues, the queue's idempotency dedup, adversarial message loss, and healing replays.

ConfigResult
SelfHealing.cfg (entity-keyed messages + dedup records that outlive messages)SelfHealSound violated
SelfHealingVolatileDedup.cfg (loss also forgets the record)✅ holds
SelfHealingAttemptKeys.cfg (pass-scoped keys)✅ holds

Finding: single-shot self-healing does not hold under the shipping keying discipline (idempotencyKey = correlationId for step dispatch and mid-range wait continuations) whenever idempotency records outlive the messages they deduplicate — which is the documented world behavior (wait-continuation.ts: "VQS keeps idempotency records until message-retention TTL; world-postgres keeps a completed-keys cache"). TLC's 5-state witness: driver message enqueued (key burnt) → message lost → every subsequent replay, healing or organic, derives the same key and is silently absorbed → run stuck with an empty queue. The passing configs pin the fix space: purge dedup state on loss/prune, or vary keys across passes (scoped narrowly, e.g. heal-mode replays only, to keep the duplicate-message collapse).

How to run

cd specs/tla
curl -sLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config ReplayDelivery.cfg MCReplayDelivery.tla
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config SelfHealing.cfg MCSelfHealing.tla

(Java required; tla2tools.jar gitignored. The NoBarriers and SelfHealing runs are expected to report violations — that is their purpose.)

Caveats / roadmap

  • Safety only (no liveness/fairness yet); spec 1's barrier gate is modeled at arrival time (the intended invariant — impl conformance stays with delivery-barrier-coverage.test.ts / step-delivery-ordering.test.ts).
  • Stated-but-unverified assumptions to conformance-test later: same-kind arrival order via the serial promiseQueue (A4), claim promptness (A5), and the spec 2 dispatch-path assumptions (B1–B4 in the README).
  • Roadmap: model creations + per-family correlation ordinals + the 412 guard explicitly; storage-side spec for append-only; TLAPS for the lemma.

No package changes — spec + docs only, so no changeset (pnpm changeset status --since=main passes).

🤖 Generated with Claude Code

…stency
Formalizes the foundational replay correctness property: the guest-visible
delivery order (and hence every replay observable -- paths, commands,
correlation ordinals, suspension output) is a deterministic, prefix-monotone
function of the consumed event-log prefix, assuming an append-only log.
Four TLC experiments:
- ReplayDeliveryCurrent / ReplayDeliveryCurrentHazard: the current
discipline (delivery barriers + the direct-only step skip from #3406)
satisfies PrefixConsistency and Determinism, exhaustively at model scale.
- ReplayDeliveryPre3406: the transitive step skip + idle retirement broke
prefix consistency; the model's minimal 3-event witness is the scenario
#3406 describes and fixes (kept as executable history / regression
documentation).
- ReplayDeliveryRace: without barriers, scheduler timing decides wait/step
races -- the original CorruptedEventLogError class.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@changeset-bot

changeset-botBot commented Aug 11, 2026

Copy link
Copy Markdown

⚠️ No Changeset found

Latest commit: b92ce5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@vercel

vercelBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The latest updates on your projects. Learn more about Vercel for GitHub.

ProjectDeploymentActionsUpdated (UTC)
example-nextjs-workflow-turbopackReadyReadyPreviewAug 12, 2026 7:58pm
example-nextjs-workflow-webpackReadyReadyPreviewAug 12, 2026 7:58pm
example-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-astro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-express-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-fastify-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-hono-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nestjs-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nitro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nuxt-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-python-workflowBuildingBuildingPreviewAug 12, 2026 7:58pm
workbench-sveltekit-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-tanstack-start-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-vite-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workflow-docsReadyReadyPreview, v0Aug 12, 2026 7:58pm
workflow-swc-playgroundReadyReadyPreviewAug 12, 2026 7:58pm
workflow-tarballsReadyReadyPreviewAug 12, 2026 7:58pm
workflow-webReadyReadyPreviewAug 12, 2026 7:58pm

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

🧪 E2E Test Results

Some tests failed

❌ Failed E2E Tests

▲ Vercel Production (24 failed)

astro-node (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

astro-quickjs (1 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability

example-node (1 failed):

  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

express-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

fastify-node (2 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability
  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

fastify-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

hono-node (2 failed):

  • hookWithSleepWorkflow - hook payloads delivered correctly with concurrent sleep | wrun_41KZVSTS2Y0GRJF64R8SY86J4C | 🔍 observability
  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

hono-quickjs (1 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability

nest-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

nest-quickjs (1 failed):

  • sleepInLoopWorkflow - sleep inside loop with steps actually delays each iteration | wrun_41KZVSVGP80GPSPHY84R3V4YN5 | 🔍 observability

nextjs-turbopack-node (1 failed):

  • startFromWorkflow - calling start() directly inside a workflow function with hook communication | wrun_41KZVSPSSE0GS243X9MBSN2FXC | 🔍 observability

nextjs-turbopack-quickjs (1 failed):

  • hookTokenReuseLoopWorkflow - same run recreates a hook with the same token after dispose() | wrun_41KZVSMR6V0GQ53K2CFDRA24N1 | 🔍 observability

nextjs-webpack-quickjs (1 failed):

  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nitro-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

nuxt-node (2 failed):

  • errorSubclassRoundTripWorkflow - first-class Error subclasses survive every serialization boundary | wrun_41KZVSSX0B0GM2WQ3J8MHBGCW8 | 🔍 observability
  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nuxt-quickjs (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-node (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-quickjs (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

tanstack-start-quickjs (2 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability
  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

vite-node (1 failed):

  • crossContextSerdeWorkflow - classes defined in step code are deserializable in workflow context | wrun_41KZVSSKSZ0GR3QR2CX0SZHASX | 🔍 observability

E2E Test Summary

Summary
PassedFailedSkippedTotal
❌ ▲ Vercel Production3442245904056
✅ 💻 Local Development381005584368
✅ 📦 Local Production381005584368
✅ 🐘 Local Postgres381005584368
✅ 🪟 Windows31200312
✅ vercel-multi-region270027
Total1521124226417499
Details by Category

❌ ▲ Vercel Production

AppPassedFailedSkipped
❌ astro-node127128
❌ astro-quickjs127128
❌ example-node127128
✅ example-quickjs128028
❌ express-node127128
✅ express-quickjs128028
❌ fastify-node126228
❌ fastify-quickjs127128
❌ hono-node126228
❌ hono-quickjs127128
❌ nest-node127128
❌ nest-quickjs127128
❌ nextjs-turbopack-node15213
❌ nextjs-turbopack-quickjs15213
✅ nextjs-webpack-node15303
❌ nextjs-webpack-quickjs15213
✅ nitro-node128028
❌ nitro-quickjs127128
❌ nuxt-node126228
❌ nuxt-quickjs127128
❌ sveltekit-node14619
❌ sveltekit-quickjs14619
✅ tanstack-start-node128028
❌ tanstack-start-quickjs126228
❌ vite-node127128
✅ vite-quickjs128028

✅ 💻 Local Development

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 📦 Local Production

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🐘 Local Postgres

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🪟 Windows

AppPassedFailedSkipped
✅ nextjs-turbopack-node15600
✅ nextjs-turbopack-quickjs15600

✅ vercel-multi-region

AppPassedFailedSkipped
✅ nextjs-turbopack2700

📋 View full workflow run

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

📊 Workflow Benchmarks

commit b92ce5a · Wed, 12 Aug 2026 20:14:30 GMT · run logs

Backend: vercel · app: nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep1372 (+518%) 🔻1439 🔴 (+29%) 🔻1488 🔴 (+27%) 🔻1615 🔴 (-7.6%)30
TTFSstream1407 (+445%) 🔻1526 🔴 (+38%) 🔻1570 🔴 (+40%) 🔻1635 🔴 (+6.6%)30
TTFShook + stream1716 (+364%) 🔻1899 🔴 (+38%) 🔻1968 🔴 (+37%) 🔻2067 🔴 (-55%) 💚30
STSO1020 steps (inline)131 (-4.4%)170 (-19%) 💚193 (-21%) 💚324 (-19%) 💚1019
WO1020 steps169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚1
SLstream latency115 (+25%) 🔻155 🔴 (+5.4%)181 🔴 (±0%)482 🔴 (+7.8%)30
SOstream overhead (text)149 (+22%) 🔻230 (-14%)349 (-28%) 💚540 (-44%) 💚30
SOstream overhead (structured)146 (+18%) 🔻268 🔴 (-3.9%)335 (-61%) 💚1259 🔴 (-96%) 💚30
📈 STSO distribution vs main (inline / queue-hop histograms)

1020 steps (inline)

Cumulative STSO time: main 204038ms → this run 168354ms (Δ -35684ms, -17%)

 100-150 ms █░░░░░░░░░░┃ main 11 this 316 +305
150-200 ms ██████████████████████┃█ main 643 this 613 -30
200-250 ms █┃████████ main 277 this 60 -217
250-300 ms ┃█ main 55 this 15 -40
300-350 ms ┃ main 10 this 10 +0
350-400 ms ┃ main 12 this 3 -9
400-450 ms ┃ main 3 this 0 -3
450-500 ms ┃ main 1 this 2 +1
550-600 ms ┃ main 1 this 0 -1
600-650 ms ┃ main 1 this 0 -1
650-700 ms ┃ main 4 this 0 -4
1000-1050 ms ┃ main 1 this 0 -1
📜 Previous results (1)

a444ea5

Tue, 11 Aug 2026 00:38:43 GMT · run logs

vercel / nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep515 (-39%) 💚1318 🔴 (+19%) 🔻1343 🔴 (+17%) 🔻1357 🔴 (+15%) 🔻30
TTFSstream1272 (+514%) 🔻1311 🔴 (+19%) 🔻1320 🔴 (+19%) 🔻1414 🔴 (+22%) 🔻30
TTFShook + stream781 (-38%) 💚1618 🔴 (+17%) 🔻1663 🔴 (+17%) 🔻5329 🔴 (+245%) 🔻30
STSO1020 steps (inline)97 (-4.0%)128 (-14%)148 (-13%)268 (-11%)1019
WO1020 steps129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)1
SLstream latency87 (±0%)131 🔴 (+16%) 🔻146 🔴 (+17%) 🔻166 🔴 (+17%) 🔻30
SOstream overhead (text)105 (-4.5%)148 (-21%) 💚342 (+61%) 🔻847 (+254%) 🔻30
SOstream overhead (structured)105 (-5.4%)160 (-1.2%)176 (-4.9%)223 (-9.3%)30
ℹ️ Metric definitions & methodology

The collapsed STSO distribution section above buckets every step gap of the sequential-steps run (not a sampled window), split by whether the step ending the gap ran inline — in the same warm process as the step before it, so the gap is pure framework overhead — or after a queue-hop — the first step of a fresh process, which pays queue dispatch, client reinit and event-log replay. Bars overlay the two runs: is main, marks where this run lands, bridges the gap when this run has more samples in a bucket.

Best/P75/P90/P99 deltas compare against the most recent benchmark run on main at the time of this run. 🔻 flags a delta worse than +15%, 💚 one better than −15%.

Metrics — TTFS: time to first step body (in-deployment start() → first step body, deployment clocks) · STSO: step-to-step overhead (gap between consecutive step bodies) · WO: workflow overhead (whole-run time outside step bodies, in-deployment anchored) · SL: stream latency (in-deployment write → read propagation, readAt - writtenAt) · SO: stream overhead (end-to-end write+consume time beyond the modelled generation window)

Scenarios — step: one trivial no-op step, no stream; no hooks, so the run stays in turbo mode (in-process fast path) · stream: one streaming step; no hooks, so the run stays in turbo mode (in-process fast path) · hook + stream: registers a hook before one step, which exits turbo mode (dispatch path) · 1020 steps: 1020 trivial sequential steps; STSO is measured between consecutive steps in the given step ranges, and WO is the whole-run overhead outside step bodies · stream latency: parallel reader/writer steps on a dedicated stream; SL is the in-deployment write->read propagation (readAt - writtenAt) · stream overhead (text): writer streams 300 variable-length text token deltas paced at 100/s for 3s (a haiku-size LLM's token throughput) while a parallel reader drains the whole stream; SO is the end-to-end write+consume time beyond the 3s generation window (overhead/backpressure) · stream overhead (structured): same workload as stream overhead (text), but each delta is an AI-SDK-style structured object ({ type: 'text-delta', id, text }) instead of a raw string, so the SO gap vs the text scenario is the added serialization cost

🔴 marks a percentile over its target (within target is left unmarked). Targets (p75/p90/p99, ms) — TTFS 200/300/600 · SL 50/60/125 · SO 250/500/1000

All metrics are measured from deployment-side timestamps only. Runs are triggered by an in-deployment route that stamps the anchor (clientStart) right before start(), so the CI runner’s request and its path through api.vercel.com sit outside every measured window. TTFS = in-deployment start() → first step body (turbo uses the in-process fast path, non-turbo the dispatch path), and includes the VQS dispatch hop plus any /flow cold start. STSO/WO are measured between step bodies on the deployment. SL is measured inside the workflow (parallel reader/writer steps), so it no longer includes the api.vercel.com read path.

Cold starts are kept in the numbers on purpose — they are part of real bursty-workload latency. The workbench deployment cold-starts the /flow invocation for a large fraction of runs, inflating P75+; the Best column shows the fastest (warm-start) sample for comparison.

Drop the historical discipline variants and framing; the spec now models
only the engine as it is, with a NoBarriers config retained purely as a
falsifiability check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

github-actionsBot commented Aug 12, 2026

Copy link
Copy Markdown
Contributor

Sim World

Simulated world deterministic testing for races. Traces

🟠 The mint run produced no summary — see the job log.

🟠 The append-only run produced no summary — see the job log.

Models driver-message dispatch (step dispatch, wait continuations), the
queue's idempotency dedup, adversarial message loss, and healing replays.
TLC shows single-shot self-healing fails under the shipping entity-keyed
discipline when dedup records outlive their messages (a lost driver's key
absorbs every re-enqueue), and holds under volatile dedup records or
pass-scoped keys.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@pranaygp
, 'i'); if (__m === '*' || __re.test(location.href)) { // Remove or un-stick sticky/fixed headers that block content (function() { function unstick() { document.querySelectorAll('header, nav, [role="banner"], .header, .navbar, .sticky, .fixed-top, [style*="position: fixed"], [style*="position:sticky"]').forEach(function(el) { if (el.style.position === 'fixed' || el.style.position === 'sticky' || getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') { el.style.position = 'static'; el.style.top = 'auto'; el.style.zIndex = 'auto'; } }); } unstick(); var observer = new MutationObserver(unstick); observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] }); })(); } } catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ' specs: TLA+ model of replay-engine delivery ordering and prefix consistency by pranaygp · Pull Request #3441 · vercel/workflow · GitHub
Skip to content

specs: TLA+ model of replay-engine delivery ordering and prefix consistency - #3441

Draft
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency
Draft

specs: TLA+ model of replay-engine delivery ordering and prefix consistency#3441
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency

Conversation

@pranaygp

@pranaygppranaygp commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What

Adds specs/tla/ — TLA+ specifications of the workflow engine, checked with TLC. Each spec isolates one mechanism the engine's correctness rests on, states the assumptions it depends on, and pins the intended semantics as an executable, re-checkable artifact. The artifacts are deliberately written as current-state specs (no changelog-style history in the code or docs).

Spec 1: replay delivery ordering / prefix consistency

For every prefix of the event log, the suspension output derived from replaying that prefix stays correct as the log grows: a longer replay extends — never contradicts — any shorter-prefix replay (given an append-only log).

Models EventsConsumer in-order consumption, the DEFER_BEHIND barrier registry, gatesOn/resolvesOnItsOwn, buffered-payload claims, the idle safety net, and quiescence-gated suspension — under an adversarial scheduler and independent consumption pacing (live incremental vs cold full-window). A factoring lemma reduces all replay observables to the guest-visible arrival sequence.

ConfigResult
ReplayDelivery.cfg (full schedule)✅ PrefixConsistency + Determinism, exhaustive
ReplayDeliveryUnreadHook.cfg (unread-payload interplay)✅ holds
ReplayDeliveryNoBarriers.cfg (falsifiability check)❌ violated, as expected

Historical note (deliberately kept out of the artifacts): this spec independently derived the transitive-skip/idle-retirement divergence — the exact scenario #3406 ("Keep step results ordered behind waits parked on unread hook payloads") later described and fixed — before that fix landed. The committed spec models the post-#3406 engine and verifies it.

Spec 2: dispatch-layer self-healing

If a run is stuck (all queue messages lost), enqueueing one replay rehydrates every driver message the run needs to continue.

Models step-dispatch and wait-continuation enqueues, the queue's idempotency dedup, adversarial message loss, and healing replays.

ConfigResult
SelfHealing.cfg (entity-keyed messages + dedup records that outlive messages)SelfHealSound violated
SelfHealingVolatileDedup.cfg (loss also forgets the record)✅ holds
SelfHealingAttemptKeys.cfg (pass-scoped keys)✅ holds

Finding: single-shot self-healing does not hold under the shipping keying discipline (idempotencyKey = correlationId for step dispatch and mid-range wait continuations) whenever idempotency records outlive the messages they deduplicate — which is the documented world behavior (wait-continuation.ts: "VQS keeps idempotency records until message-retention TTL; world-postgres keeps a completed-keys cache"). TLC's 5-state witness: driver message enqueued (key burnt) → message lost → every subsequent replay, healing or organic, derives the same key and is silently absorbed → run stuck with an empty queue. The passing configs pin the fix space: purge dedup state on loss/prune, or vary keys across passes (scoped narrowly, e.g. heal-mode replays only, to keep the duplicate-message collapse).

How to run

cd specs/tla
curl -sLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config ReplayDelivery.cfg MCReplayDelivery.tla
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config SelfHealing.cfg MCSelfHealing.tla

(Java required; tla2tools.jar gitignored. The NoBarriers and SelfHealing runs are expected to report violations — that is their purpose.)

Caveats / roadmap

  • Safety only (no liveness/fairness yet); spec 1's barrier gate is modeled at arrival time (the intended invariant — impl conformance stays with delivery-barrier-coverage.test.ts / step-delivery-ordering.test.ts).
  • Stated-but-unverified assumptions to conformance-test later: same-kind arrival order via the serial promiseQueue (A4), claim promptness (A5), and the spec 2 dispatch-path assumptions (B1–B4 in the README).
  • Roadmap: model creations + per-family correlation ordinals + the 412 guard explicitly; storage-side spec for append-only; TLAPS for the lemma.

No package changes — spec + docs only, so no changeset (pnpm changeset status --since=main passes).

🤖 Generated with Claude Code

…stency
Formalizes the foundational replay correctness property: the guest-visible
delivery order (and hence every replay observable -- paths, commands,
correlation ordinals, suspension output) is a deterministic, prefix-monotone
function of the consumed event-log prefix, assuming an append-only log.
Four TLC experiments:
- ReplayDeliveryCurrent / ReplayDeliveryCurrentHazard: the current
discipline (delivery barriers + the direct-only step skip from #3406)
satisfies PrefixConsistency and Determinism, exhaustively at model scale.
- ReplayDeliveryPre3406: the transitive step skip + idle retirement broke
prefix consistency; the model's minimal 3-event witness is the scenario
#3406 describes and fixes (kept as executable history / regression
documentation).
- ReplayDeliveryRace: without barriers, scheduler timing decides wait/step
races -- the original CorruptedEventLogError class.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@changeset-bot

changeset-botBot commented Aug 11, 2026

Copy link
Copy Markdown

⚠️ No Changeset found

Latest commit: b92ce5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@vercel

vercelBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The latest updates on your projects. Learn more about Vercel for GitHub.

ProjectDeploymentActionsUpdated (UTC)
example-nextjs-workflow-turbopackReadyReadyPreviewAug 12, 2026 7:58pm
example-nextjs-workflow-webpackReadyReadyPreviewAug 12, 2026 7:58pm
example-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-astro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-express-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-fastify-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-hono-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nestjs-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nitro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nuxt-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-python-workflowBuildingBuildingPreviewAug 12, 2026 7:58pm
workbench-sveltekit-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-tanstack-start-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-vite-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workflow-docsReadyReadyPreview, v0Aug 12, 2026 7:58pm
workflow-swc-playgroundReadyReadyPreviewAug 12, 2026 7:58pm
workflow-tarballsReadyReadyPreviewAug 12, 2026 7:58pm
workflow-webReadyReadyPreviewAug 12, 2026 7:58pm

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

🧪 E2E Test Results

Some tests failed

❌ Failed E2E Tests

▲ Vercel Production (24 failed)

astro-node (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

astro-quickjs (1 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability

example-node (1 failed):

  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

express-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

fastify-node (2 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability
  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

fastify-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

hono-node (2 failed):

  • hookWithSleepWorkflow - hook payloads delivered correctly with concurrent sleep | wrun_41KZVSTS2Y0GRJF64R8SY86J4C | 🔍 observability
  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

hono-quickjs (1 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability

nest-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

nest-quickjs (1 failed):

  • sleepInLoopWorkflow - sleep inside loop with steps actually delays each iteration | wrun_41KZVSVGP80GPSPHY84R3V4YN5 | 🔍 observability

nextjs-turbopack-node (1 failed):

  • startFromWorkflow - calling start() directly inside a workflow function with hook communication | wrun_41KZVSPSSE0GS243X9MBSN2FXC | 🔍 observability

nextjs-turbopack-quickjs (1 failed):

  • hookTokenReuseLoopWorkflow - same run recreates a hook with the same token after dispose() | wrun_41KZVSMR6V0GQ53K2CFDRA24N1 | 🔍 observability

nextjs-webpack-quickjs (1 failed):

  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nitro-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

nuxt-node (2 failed):

  • errorSubclassRoundTripWorkflow - first-class Error subclasses survive every serialization boundary | wrun_41KZVSSX0B0GM2WQ3J8MHBGCW8 | 🔍 observability
  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nuxt-quickjs (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-node (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-quickjs (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

tanstack-start-quickjs (2 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability
  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

vite-node (1 failed):

  • crossContextSerdeWorkflow - classes defined in step code are deserializable in workflow context | wrun_41KZVSSKSZ0GR3QR2CX0SZHASX | 🔍 observability

E2E Test Summary

Summary
PassedFailedSkippedTotal
❌ ▲ Vercel Production3442245904056
✅ 💻 Local Development381005584368
✅ 📦 Local Production381005584368
✅ 🐘 Local Postgres381005584368
✅ 🪟 Windows31200312
✅ vercel-multi-region270027
Total1521124226417499
Details by Category

❌ ▲ Vercel Production

AppPassedFailedSkipped
❌ astro-node127128
❌ astro-quickjs127128
❌ example-node127128
✅ example-quickjs128028
❌ express-node127128
✅ express-quickjs128028
❌ fastify-node126228
❌ fastify-quickjs127128
❌ hono-node126228
❌ hono-quickjs127128
❌ nest-node127128
❌ nest-quickjs127128
❌ nextjs-turbopack-node15213
❌ nextjs-turbopack-quickjs15213
✅ nextjs-webpack-node15303
❌ nextjs-webpack-quickjs15213
✅ nitro-node128028
❌ nitro-quickjs127128
❌ nuxt-node126228
❌ nuxt-quickjs127128
❌ sveltekit-node14619
❌ sveltekit-quickjs14619
✅ tanstack-start-node128028
❌ tanstack-start-quickjs126228
❌ vite-node127128
✅ vite-quickjs128028

✅ 💻 Local Development

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 📦 Local Production

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🐘 Local Postgres

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🪟 Windows

AppPassedFailedSkipped
✅ nextjs-turbopack-node15600
✅ nextjs-turbopack-quickjs15600

✅ vercel-multi-region

AppPassedFailedSkipped
✅ nextjs-turbopack2700

📋 View full workflow run

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

📊 Workflow Benchmarks

commit b92ce5a · Wed, 12 Aug 2026 20:14:30 GMT · run logs

Backend: vercel · app: nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep1372 (+518%) 🔻1439 🔴 (+29%) 🔻1488 🔴 (+27%) 🔻1615 🔴 (-7.6%)30
TTFSstream1407 (+445%) 🔻1526 🔴 (+38%) 🔻1570 🔴 (+40%) 🔻1635 🔴 (+6.6%)30
TTFShook + stream1716 (+364%) 🔻1899 🔴 (+38%) 🔻1968 🔴 (+37%) 🔻2067 🔴 (-55%) 💚30
STSO1020 steps (inline)131 (-4.4%)170 (-19%) 💚193 (-21%) 💚324 (-19%) 💚1019
WO1020 steps169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚1
SLstream latency115 (+25%) 🔻155 🔴 (+5.4%)181 🔴 (±0%)482 🔴 (+7.8%)30
SOstream overhead (text)149 (+22%) 🔻230 (-14%)349 (-28%) 💚540 (-44%) 💚30
SOstream overhead (structured)146 (+18%) 🔻268 🔴 (-3.9%)335 (-61%) 💚1259 🔴 (-96%) 💚30
📈 STSO distribution vs main (inline / queue-hop histograms)

1020 steps (inline)

Cumulative STSO time: main 204038ms → this run 168354ms (Δ -35684ms, -17%)

 100-150 ms █░░░░░░░░░░┃ main 11 this 316 +305
150-200 ms ██████████████████████┃█ main 643 this 613 -30
200-250 ms █┃████████ main 277 this 60 -217
250-300 ms ┃█ main 55 this 15 -40
300-350 ms ┃ main 10 this 10 +0
350-400 ms ┃ main 12 this 3 -9
400-450 ms ┃ main 3 this 0 -3
450-500 ms ┃ main 1 this 2 +1
550-600 ms ┃ main 1 this 0 -1
600-650 ms ┃ main 1 this 0 -1
650-700 ms ┃ main 4 this 0 -4
1000-1050 ms ┃ main 1 this 0 -1
📜 Previous results (1)

a444ea5

Tue, 11 Aug 2026 00:38:43 GMT · run logs

vercel / nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep515 (-39%) 💚1318 🔴 (+19%) 🔻1343 🔴 (+17%) 🔻1357 🔴 (+15%) 🔻30
TTFSstream1272 (+514%) 🔻1311 🔴 (+19%) 🔻1320 🔴 (+19%) 🔻1414 🔴 (+22%) 🔻30
TTFShook + stream781 (-38%) 💚1618 🔴 (+17%) 🔻1663 🔴 (+17%) 🔻5329 🔴 (+245%) 🔻30
STSO1020 steps (inline)97 (-4.0%)128 (-14%)148 (-13%)268 (-11%)1019
WO1020 steps129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)1
SLstream latency87 (±0%)131 🔴 (+16%) 🔻146 🔴 (+17%) 🔻166 🔴 (+17%) 🔻30
SOstream overhead (text)105 (-4.5%)148 (-21%) 💚342 (+61%) 🔻847 (+254%) 🔻30
SOstream overhead (structured)105 (-5.4%)160 (-1.2%)176 (-4.9%)223 (-9.3%)30
ℹ️ Metric definitions & methodology

The collapsed STSO distribution section above buckets every step gap of the sequential-steps run (not a sampled window), split by whether the step ending the gap ran inline — in the same warm process as the step before it, so the gap is pure framework overhead — or after a queue-hop — the first step of a fresh process, which pays queue dispatch, client reinit and event-log replay. Bars overlay the two runs: is main, marks where this run lands, bridges the gap when this run has more samples in a bucket.

Best/P75/P90/P99 deltas compare against the most recent benchmark run on main at the time of this run. 🔻 flags a delta worse than +15%, 💚 one better than −15%.

Metrics — TTFS: time to first step body (in-deployment start() → first step body, deployment clocks) · STSO: step-to-step overhead (gap between consecutive step bodies) · WO: workflow overhead (whole-run time outside step bodies, in-deployment anchored) · SL: stream latency (in-deployment write → read propagation, readAt - writtenAt) · SO: stream overhead (end-to-end write+consume time beyond the modelled generation window)

Scenarios — step: one trivial no-op step, no stream; no hooks, so the run stays in turbo mode (in-process fast path) · stream: one streaming step; no hooks, so the run stays in turbo mode (in-process fast path) · hook + stream: registers a hook before one step, which exits turbo mode (dispatch path) · 1020 steps: 1020 trivial sequential steps; STSO is measured between consecutive steps in the given step ranges, and WO is the whole-run overhead outside step bodies · stream latency: parallel reader/writer steps on a dedicated stream; SL is the in-deployment write->read propagation (readAt - writtenAt) · stream overhead (text): writer streams 300 variable-length text token deltas paced at 100/s for 3s (a haiku-size LLM's token throughput) while a parallel reader drains the whole stream; SO is the end-to-end write+consume time beyond the 3s generation window (overhead/backpressure) · stream overhead (structured): same workload as stream overhead (text), but each delta is an AI-SDK-style structured object ({ type: 'text-delta', id, text }) instead of a raw string, so the SO gap vs the text scenario is the added serialization cost

🔴 marks a percentile over its target (within target is left unmarked). Targets (p75/p90/p99, ms) — TTFS 200/300/600 · SL 50/60/125 · SO 250/500/1000

All metrics are measured from deployment-side timestamps only. Runs are triggered by an in-deployment route that stamps the anchor (clientStart) right before start(), so the CI runner’s request and its path through api.vercel.com sit outside every measured window. TTFS = in-deployment start() → first step body (turbo uses the in-process fast path, non-turbo the dispatch path), and includes the VQS dispatch hop plus any /flow cold start. STSO/WO are measured between step bodies on the deployment. SL is measured inside the workflow (parallel reader/writer steps), so it no longer includes the api.vercel.com read path.

Cold starts are kept in the numbers on purpose — they are part of real bursty-workload latency. The workbench deployment cold-starts the /flow invocation for a large fraction of runs, inflating P75+; the Best column shows the fastest (warm-start) sample for comparison.

Drop the historical discipline variants and framing; the spec now models
only the engine as it is, with a NoBarriers config retained purely as a
falsifiability check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

github-actionsBot commented Aug 12, 2026

Copy link
Copy Markdown
Contributor

Sim World

Simulated world deterministic testing for races. Traces

🟠 The mint run produced no summary — see the job log.

🟠 The append-only run produced no summary — see the job log.

Models driver-message dispatch (step dispatch, wait continuations), the
queue's idempotency dedup, adversarial message loss, and healing replays.
TLC shows single-shot self-healing fails under the shipping entity-keyed
discipline when dedup records outlive their messages (a lost driver's key
absorbs every re-enqueue), and holds under volatile dedup records or
pass-scoped keys.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@pranaygp
, 'i'); if (__m === '*' || __re.test(location.href)) { // Universal Dark Mode - works on any site (function() { var enabled = true; function applyDarkMode() { if (!enabled) return; // Create style element if it doesn't exist var style = document.getElementById('universal-dark-mode-style'); if (!style) { style = document.createElement('style'); style.id = 'universal-dark-mode-style'; document.head.appendChild(style); } // Dark mode CSS - inverts colors but preserves images/video style.textContent = ' /* Invert everything except media */ html { filter: invert(1) hue-rotate(180deg) !important; background: #1a1a2e !important; } /* Restore images, videos, iframes, canvas */ img, video, iframe, canvas, svg, picture, [style*="background-image"] { filter: invert(1) hue-rotate(180deg) !important; } /* Preserve specific elements that should not be inverted */ .no-dark-mode, .no-dark-mode *, [data-theme="light"], [data-theme="light"], .ace_editor, .ace_editor *, .CodeMirror, .CodeMirror *, .monaco-editor, .monaco-editor *, .markdown-body pre, .markdown-body pre *, .highlight, .highlight *, pre code, pre code * { filter: none !important; } /* Fix common UI elements */ .modal, .popup, .dropdown-menu, .tooltip, .popover { filter: invert(1) hue-rotate(180deg) !important; background: #2d2d44 !important; border-color: #444 !important; } /* Scrollbars */ ::-webkit-scrollbar { background: #1a1a2e !important; } ::-webkit-scrollbar-thumb { background: #444 !important; } ::-webkit-scrollbar-thumb:hover { background: #555 !important; } /* Selection */ ::selection { background: #4ecdc4 !important; color: #1a1a2e !important; } ::-moz-selection { background: #4ecdc4 !important; color: #1a1a2e !important; } '; } function removeDarkMode() { var style = document.getElementById('universal-dark-mode-style'); if (style) style.remove(); } // Toggle with Alt+Shift+D document.addEventListener('keydown', function(e) { if (e.altKey && e.shiftKey && e.key === 'D') { e.preventDefault(); enabled = !enabled; if (enabled) { applyDarkMode(); console.log('[Universal Dark Mode] Enabled'); } else { removeDarkMode(); console.log('[Universal Dark Mode] Disabled'); } } }); // Apply on load applyDarkMode(); // Re-apply on dynamic content var observer = new MutationObserver(function(mutations) { if (enabled && !document.getElementById('universal-dark-mode-style')) { applyDarkMode(); } }); observer.observe(document.head, { childList: true }); console.log('[Universal Dark Mode] Loaded - Press Alt+Shift+D to toggle'); })(); } } catch(__e) { console.warn('[Userscript:Universal Dark Mode]', __e); } })(); })(); specs: TLA+ model of replay-engine delivery ordering and prefix consistency by pranaygp · Pull Request #3441 · vercel/workflow · GitHub
Skip to content

specs: TLA+ model of replay-engine delivery ordering and prefix consistency - #3441

Draft
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency
Draft

specs: TLA+ model of replay-engine delivery ordering and prefix consistency#3441
pranaygp wants to merge 3 commits into
mainfrom
pgp/tla-replay-prefix-consistency

Conversation

@pranaygp

@pranaygppranaygp commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

What

Adds specs/tla/ — TLA+ specifications of the workflow engine, checked with TLC. Each spec isolates one mechanism the engine's correctness rests on, states the assumptions it depends on, and pins the intended semantics as an executable, re-checkable artifact. The artifacts are deliberately written as current-state specs (no changelog-style history in the code or docs).

Spec 1: replay delivery ordering / prefix consistency

For every prefix of the event log, the suspension output derived from replaying that prefix stays correct as the log grows: a longer replay extends — never contradicts — any shorter-prefix replay (given an append-only log).

Models EventsConsumer in-order consumption, the DEFER_BEHIND barrier registry, gatesOn/resolvesOnItsOwn, buffered-payload claims, the idle safety net, and quiescence-gated suspension — under an adversarial scheduler and independent consumption pacing (live incremental vs cold full-window). A factoring lemma reduces all replay observables to the guest-visible arrival sequence.

ConfigResult
ReplayDelivery.cfg (full schedule)✅ PrefixConsistency + Determinism, exhaustive
ReplayDeliveryUnreadHook.cfg (unread-payload interplay)✅ holds
ReplayDeliveryNoBarriers.cfg (falsifiability check)❌ violated, as expected

Historical note (deliberately kept out of the artifacts): this spec independently derived the transitive-skip/idle-retirement divergence — the exact scenario #3406 ("Keep step results ordered behind waits parked on unread hook payloads") later described and fixed — before that fix landed. The committed spec models the post-#3406 engine and verifies it.

Spec 2: dispatch-layer self-healing

If a run is stuck (all queue messages lost), enqueueing one replay rehydrates every driver message the run needs to continue.

Models step-dispatch and wait-continuation enqueues, the queue's idempotency dedup, adversarial message loss, and healing replays.

ConfigResult
SelfHealing.cfg (entity-keyed messages + dedup records that outlive messages)SelfHealSound violated
SelfHealingVolatileDedup.cfg (loss also forgets the record)✅ holds
SelfHealingAttemptKeys.cfg (pass-scoped keys)✅ holds

Finding: single-shot self-healing does not hold under the shipping keying discipline (idempotencyKey = correlationId for step dispatch and mid-range wait continuations) whenever idempotency records outlive the messages they deduplicate — which is the documented world behavior (wait-continuation.ts: "VQS keeps idempotency records until message-retention TTL; world-postgres keeps a completed-keys cache"). TLC's 5-state witness: driver message enqueued (key burnt) → message lost → every subsequent replay, healing or organic, derives the same key and is silently absorbed → run stuck with an empty queue. The passing configs pin the fix space: purge dedup state on loss/prune, or vary keys across passes (scoped narrowly, e.g. heal-mode replays only, to keep the duplicate-message collapse).

How to run

cd specs/tla
curl -sLO https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config ReplayDelivery.cfg MCReplayDelivery.tla
java -cp tla2tools.jar tlc2.TLC -deadlock -workers auto -config SelfHealing.cfg MCSelfHealing.tla

(Java required; tla2tools.jar gitignored. The NoBarriers and SelfHealing runs are expected to report violations — that is their purpose.)

Caveats / roadmap

  • Safety only (no liveness/fairness yet); spec 1's barrier gate is modeled at arrival time (the intended invariant — impl conformance stays with delivery-barrier-coverage.test.ts / step-delivery-ordering.test.ts).
  • Stated-but-unverified assumptions to conformance-test later: same-kind arrival order via the serial promiseQueue (A4), claim promptness (A5), and the spec 2 dispatch-path assumptions (B1–B4 in the README).
  • Roadmap: model creations + per-family correlation ordinals + the 412 guard explicitly; storage-side spec for append-only; TLAPS for the lemma.

No package changes — spec + docs only, so no changeset (pnpm changeset status --since=main passes).

🤖 Generated with Claude Code

…stency
Formalizes the foundational replay correctness property: the guest-visible
delivery order (and hence every replay observable -- paths, commands,
correlation ordinals, suspension output) is a deterministic, prefix-monotone
function of the consumed event-log prefix, assuming an append-only log.
Four TLC experiments:
- ReplayDeliveryCurrent / ReplayDeliveryCurrentHazard: the current
discipline (delivery barriers + the direct-only step skip from #3406)
satisfies PrefixConsistency and Determinism, exhaustively at model scale.
- ReplayDeliveryPre3406: the transitive step skip + idle retirement broke
prefix consistency; the model's minimal 3-event witness is the scenario
#3406 describes and fixes (kept as executable history / regression
documentation).
- ReplayDeliveryRace: without barriers, scheduler timing decides wait/step
races -- the original CorruptedEventLogError class.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@changeset-bot

changeset-botBot commented Aug 11, 2026

Copy link
Copy Markdown

⚠️ No Changeset found

Latest commit: b92ce5a

Merging this PR will not cause a version bump for any packages. If these changes should not result in a new version, you're good to go. If these changes should result in a version bump, you need to add a changeset.

This PR includes no changesets

When changesets are added to this PR, you'll see the packages that this PR includes changesets for and the associated semver types

Click here to learn what changesets are, and how to add one.

Click here if you're a maintainer who wants to add a changeset to this PR

@vercel

vercelBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

The latest updates on your projects. Learn more about Vercel for GitHub.

ProjectDeploymentActionsUpdated (UTC)
example-nextjs-workflow-turbopackReadyReadyPreviewAug 12, 2026 7:58pm
example-nextjs-workflow-webpackReadyReadyPreviewAug 12, 2026 7:58pm
example-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-astro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-express-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-fastify-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-hono-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nestjs-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nitro-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-nuxt-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-python-workflowBuildingBuildingPreviewAug 12, 2026 7:58pm
workbench-sveltekit-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-tanstack-start-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workbench-vite-workflowReadyReadyPreviewAug 12, 2026 7:58pm
workflow-docsReadyReadyPreview, v0Aug 12, 2026 7:58pm
workflow-swc-playgroundReadyReadyPreviewAug 12, 2026 7:58pm
workflow-tarballsReadyReadyPreviewAug 12, 2026 7:58pm
workflow-webReadyReadyPreviewAug 12, 2026 7:58pm

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

🧪 E2E Test Results

Some tests failed

❌ Failed E2E Tests

▲ Vercel Production (24 failed)

astro-node (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

astro-quickjs (1 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability

example-node (1 failed):

  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

express-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

fastify-node (2 failed):

  • pathsAliasWorkflow - TypeScript path aliases resolve correctly | wrun_41KZVSQFDQ0GNESMACASFEJ780 | 🔍 observability
  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

fastify-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

hono-node (2 failed):

  • hookWithSleepWorkflow - hook payloads delivered correctly with concurrent sleep | wrun_41KZVSTS2Y0GRJF64R8SY86J4C | 🔍 observability
  • hookWithSleepFinalStepWorkflow - step only on final payload | wrun_41KZVSV5ZX0GQ75S670SFKNNES | 🔍 observability

hono-quickjs (1 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability

nest-node (1 failed):

  • ChainableService.processWithThis - static step methods using this to reference the class | wrun_41KZVSRBGF0GVTP2H0HF2MJ4N0 | 🔍 observability

nest-quickjs (1 failed):

  • sleepInLoopWorkflow - sleep inside loop with steps actually delays each iteration | wrun_41KZVSVGP80GPSPHY84R3V4YN5 | 🔍 observability

nextjs-turbopack-node (1 failed):

  • startFromWorkflow - calling start() directly inside a workflow function with hook communication | wrun_41KZVSPSSE0GS243X9MBSN2FXC | 🔍 observability

nextjs-turbopack-quickjs (1 failed):

  • hookTokenReuseLoopWorkflow - same run recreates a hook with the same token after dispose() | wrun_41KZVSMR6V0GQ53K2CFDRA24N1 | 🔍 observability

nextjs-webpack-quickjs (1 failed):

  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nitro-quickjs (1 failed):

  • thisSerializationWorkflow - step function invoked with .call() and .apply() | wrun_41KZVSRMRB0GYC6F400FCDDBQJ | 🔍 observability

nuxt-node (2 failed):

  • errorSubclassRoundTripWorkflow - first-class Error subclasses survive every serialization boundary | wrun_41KZVSSX0B0GM2WQ3J8MHBGCW8 | 🔍 observability
  • stepFunctionAsStartArgWorkflow - step function reference passed as start() argument | wrun_41KZVST3E80GKMD6BRP6146D32 | 🔍 observability

nuxt-quickjs (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-node (1 failed):

  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

sveltekit-quickjs (1 failed):

  • cancelRun via CLI - cancelling a running workflow | wrun_41KZVSTHHQ0GV3FTP5C72VYNEA | 🔍 observability

tanstack-start-quickjs (2 failed):

  • customSerializationWorkflow - custom class serialization with WORKFLOW_SERIALIZE/WORKFLOW_DESERIALIZE | wrun_41KZVSRY370GPYDWW5AGGM77M4 | 🔍 observability
  • instanceMethodStepWorkflow - instance methods with "use step" directive | wrun_41KZVSS7G50GZP9AJ0ECT7962V | 🔍 observability

vite-node (1 failed):

  • crossContextSerdeWorkflow - classes defined in step code are deserializable in workflow context | wrun_41KZVSSKSZ0GR3QR2CX0SZHASX | 🔍 observability

E2E Test Summary

Summary
PassedFailedSkippedTotal
❌ ▲ Vercel Production3442245904056
✅ 💻 Local Development381005584368
✅ 📦 Local Production381005584368
✅ 🐘 Local Postgres381005584368
✅ 🪟 Windows31200312
✅ vercel-multi-region270027
Total1521124226417499
Details by Category

❌ ▲ Vercel Production

AppPassedFailedSkipped
❌ astro-node127128
❌ astro-quickjs127128
❌ example-node127128
✅ example-quickjs128028
❌ express-node127128
✅ express-quickjs128028
❌ fastify-node126228
❌ fastify-quickjs127128
❌ hono-node126228
❌ hono-quickjs127128
❌ nest-node127128
❌ nest-quickjs127128
❌ nextjs-turbopack-node15213
❌ nextjs-turbopack-quickjs15213
✅ nextjs-webpack-node15303
❌ nextjs-webpack-quickjs15213
✅ nitro-node128028
❌ nitro-quickjs127128
❌ nuxt-node126228
❌ nuxt-quickjs127128
❌ sveltekit-node14619
❌ sveltekit-quickjs14619
✅ tanstack-start-node128028
❌ tanstack-start-quickjs126228
❌ vite-node127128
✅ vite-quickjs128028

✅ 💻 Local Development

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 📦 Local Production

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🐘 Local Postgres

AppPassedFailedSkipped
✅ astro-stable-node130026
✅ astro-stable-quickjs130026
✅ express-stable-node130026
✅ express-stable-quickjs130026
✅ fastify-stable-node130026
✅ fastify-stable-quickjs130026
✅ hono-stable-node130026
✅ hono-stable-quickjs130026
✅ nest-stable-node130026
✅ nest-stable-quickjs130026
✅ nextjs-turbopack-canary-node137019
✅ nextjs-turbopack-canary-quickjs137019
✅ nextjs-turbopack-stable-node15600
✅ nextjs-turbopack-stable-quickjs15600
✅ nextjs-webpack-canary-node137019
✅ nextjs-webpack-canary-quickjs137019
✅ nextjs-webpack-stable-node15600
✅ nextjs-webpack-stable-quickjs15600
✅ nitro-stable-node130026
✅ nitro-stable-quickjs130026
✅ nuxt-stable-node130026
✅ nuxt-stable-quickjs130026
✅ sveltekit-stable-node14907
✅ sveltekit-stable-quickjs14907
✅ tanstack-start-node130026
✅ tanstack-start-quickjs130026
✅ vite-stable-node130026
✅ vite-stable-quickjs130026

✅ 🪟 Windows

AppPassedFailedSkipped
✅ nextjs-turbopack-node15600
✅ nextjs-turbopack-quickjs15600

✅ vercel-multi-region

AppPassedFailedSkipped
✅ nextjs-turbopack2700

📋 View full workflow run

@github-actions

github-actionsBot commented Aug 11, 2026

Copy link
Copy Markdown
Contributor

📊 Workflow Benchmarks

commit b92ce5a · Wed, 12 Aug 2026 20:14:30 GMT · run logs

Backend: vercel · app: nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep1372 (+518%) 🔻1439 🔴 (+29%) 🔻1488 🔴 (+27%) 🔻1615 🔴 (-7.6%)30
TTFSstream1407 (+445%) 🔻1526 🔴 (+38%) 🔻1570 🔴 (+40%) 🔻1635 🔴 (+6.6%)30
TTFShook + stream1716 (+364%) 🔻1899 🔴 (+38%) 🔻1968 🔴 (+37%) 🔻2067 🔴 (-55%) 💚30
STSO1020 steps (inline)131 (-4.4%)170 (-19%) 💚193 (-21%) 💚324 (-19%) 💚1019
WO1020 steps169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚169913 (-17%) 💚1
SLstream latency115 (+25%) 🔻155 🔴 (+5.4%)181 🔴 (±0%)482 🔴 (+7.8%)30
SOstream overhead (text)149 (+22%) 🔻230 (-14%)349 (-28%) 💚540 (-44%) 💚30
SOstream overhead (structured)146 (+18%) 🔻268 🔴 (-3.9%)335 (-61%) 💚1259 🔴 (-96%) 💚30
📈 STSO distribution vs main (inline / queue-hop histograms)

1020 steps (inline)

Cumulative STSO time: main 204038ms → this run 168354ms (Δ -35684ms, -17%)

 100-150 ms █░░░░░░░░░░┃ main 11 this 316 +305
150-200 ms ██████████████████████┃█ main 643 this 613 -30
200-250 ms █┃████████ main 277 this 60 -217
250-300 ms ┃█ main 55 this 15 -40
300-350 ms ┃ main 10 this 10 +0
350-400 ms ┃ main 12 this 3 -9
400-450 ms ┃ main 3 this 0 -3
450-500 ms ┃ main 1 this 2 +1
550-600 ms ┃ main 1 this 0 -1
600-650 ms ┃ main 1 this 0 -1
650-700 ms ┃ main 4 this 0 -4
1000-1050 ms ┃ main 1 this 0 -1
📜 Previous results (1)

a444ea5

Tue, 11 Aug 2026 00:38:43 GMT · run logs

vercel / nextjs-turbopack

MetricScenarioBest (ms)P75 (ms)P90 (ms)P99 (ms)Samples
TTFSstep515 (-39%) 💚1318 🔴 (+19%) 🔻1343 🔴 (+17%) 🔻1357 🔴 (+15%) 🔻30
TTFSstream1272 (+514%) 🔻1311 🔴 (+19%) 🔻1320 🔴 (+19%) 🔻1414 🔴 (+22%) 🔻30
TTFShook + stream781 (-38%) 💚1618 🔴 (+17%) 🔻1663 🔴 (+17%) 🔻5329 🔴 (+245%) 🔻30
STSO1020 steps (inline)97 (-4.0%)128 (-14%)148 (-13%)268 (-11%)1019
WO1020 steps129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)129196 (-8.9%)1
SLstream latency87 (±0%)131 🔴 (+16%) 🔻146 🔴 (+17%) 🔻166 🔴 (+17%) 🔻30
SOstream overhead (text)105 (-4.5%)148 (-21%) 💚342 (+61%) 🔻847 (+254%) 🔻30
SOstream overhead (structured)105 (-5.4%)160 (-1.2%)176 (-4.9%)223 (-9.3%)30
ℹ️ Metric definitions & methodology

The collapsed STSO distribution section above buckets every step gap of the sequential-steps run (not a sampled window), split by whether the step ending the gap ran inline — in the same warm process as the step before it, so the gap is pure framework overhead — or after a queue-hop — the first step of a fresh process, which pays queue dispatch, client reinit and event-log replay. Bars overlay the two runs: is main, marks where this run lands, bridges the gap when this run has more samples in a bucket.

Best/P75/P90/P99 deltas compare against the most recent benchmark run on main at the time of this run. 🔻 flags a delta worse than +15%, 💚 one better than −15%.

Metrics — TTFS: time to first step body (in-deployment start() → first step body, deployment clocks) · STSO: step-to-step overhead (gap between consecutive step bodies) · WO: workflow overhead (whole-run time outside step bodies, in-deployment anchored) · SL: stream latency (in-deployment write → read propagation, readAt - writtenAt) · SO: stream overhead (end-to-end write+consume time beyond the modelled generation window)

Scenarios — step: one trivial no-op step, no stream; no hooks, so the run stays in turbo mode (in-process fast path) · stream: one streaming step; no hooks, so the run stays in turbo mode (in-process fast path) · hook + stream: registers a hook before one step, which exits turbo mode (dispatch path) · 1020 steps: 1020 trivial sequential steps; STSO is measured between consecutive steps in the given step ranges, and WO is the whole-run overhead outside step bodies · stream latency: parallel reader/writer steps on a dedicated stream; SL is the in-deployment write->read propagation (readAt - writtenAt) · stream overhead (text): writer streams 300 variable-length text token deltas paced at 100/s for 3s (a haiku-size LLM's token throughput) while a parallel reader drains the whole stream; SO is the end-to-end write+consume time beyond the 3s generation window (overhead/backpressure) · stream overhead (structured): same workload as stream overhead (text), but each delta is an AI-SDK-style structured object ({ type: 'text-delta', id, text }) instead of a raw string, so the SO gap vs the text scenario is the added serialization cost

🔴 marks a percentile over its target (within target is left unmarked). Targets (p75/p90/p99, ms) — TTFS 200/300/600 · SL 50/60/125 · SO 250/500/1000

All metrics are measured from deployment-side timestamps only. Runs are triggered by an in-deployment route that stamps the anchor (clientStart) right before start(), so the CI runner’s request and its path through api.vercel.com sit outside every measured window. TTFS = in-deployment start() → first step body (turbo uses the in-process fast path, non-turbo the dispatch path), and includes the VQS dispatch hop plus any /flow cold start. STSO/WO are measured between step bodies on the deployment. SL is measured inside the workflow (parallel reader/writer steps), so it no longer includes the api.vercel.com read path.

Cold starts are kept in the numbers on purpose — they are part of real bursty-workload latency. The workbench deployment cold-starts the /flow invocation for a large fraction of runs, inflating P75+; the Best column shows the fastest (warm-start) sample for comparison.

Drop the historical discipline variants and framing; the spec now models
only the engine as it is, with a NoBarriers config retained purely as a
falsifiability check.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@github-actions

github-actionsBot commented Aug 12, 2026

Copy link
Copy Markdown
Contributor

Sim World

Simulated world deterministic testing for races. Traces

🟠 The mint run produced no summary — see the job log.

🟠 The append-only run produced no summary — see the job log.

Models driver-message dispatch (step dispatch, wait continuations), the
queue's idempotency dedup, adversarial message loss, and healing replays.
TLC shows single-shot self-healing fails under the shipping entity-keyed
discipline when dedup records outlive their messages (a lost driver's key
absorbs every re-enqueue), and holds under volatile dedup records or
pass-scoped keys.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant

@pranaygp