From cad19246ab412cd606b3497cbbd25209c4b2912b Mon Sep 17 00:00:00 2001
From: Lucas Carlson <lucas@carlson.net>
Date: Tue, 18 Aug 2026 08:58:52 -0700
Subject: [PATCH 1/4] fix: prove serialization by message, not by execution

The failure-recovery demo asserted the serialization control file held
exactly four events. A worker that loses its lease mid-operation leaves
the replacement to execute the same message again, so a slower machine
produces six, and the demo failed for the at-least-once behaviour the
library documents and the crash and fencing proofs rely on.

It failed five times on GitHub runners, on Node 24.15.0 as well as the
lower floor, and passed on rerun, so the assertion was reporting the
runner's speed rather than a durability property.

The proof now asserts what the runtime guarantees: executions never
overlap, every start has a matching finish, and exactly the two sent
messages ran. The committed state check is unchanged, and it is the one
that would catch a lost or doubled write.

assertSerializedExecution moves into its own module so it can be tested
at the lowest layer. The unit tests cover the retry, overlap, unfinished,
and lost-message cases, and each rejection case fails when the rule is
removed.

The lease timing stays as it was. proveCrashRecovery and proveFencing
depend on a short lease, so raising it to hide the retry would weaken
them.
---
 CHANGELOG.md                                | 11 +++++
 examples/failure-recovery/demo.ts           | 26 +---------
 examples/failure-recovery/serialization.ts  | 53 +++++++++++++++++++++
 test/failure-recovery-serialization.test.ts | 52 ++++++++++++++++++++
 4 files changed, 118 insertions(+), 24 deletions(-)
 create mode 100644 examples/failure-recovery/serialization.ts
 create mode 100644 test/failure-recovery-serialization.test.ts

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9c29d53..8242f8a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,5 +1,16 @@
 # Changelog
 
+## Unreleased
+
+- Make the failure-recovery demo's serialization proof count messages rather
+  than executions. A worker that loses its lease mid-operation leaves the
+  replacement to execute the same message again, which is the at-least-once
+  contract, so the proof failed on slower machines for behaviour it documents
+  elsewhere. It now asserts that executions never overlap, that every start has
+  a finish, and that exactly the two sent messages ran, with the committed state
+  check unchanged. `assertSerializedExecution` moved into its own module and has
+  unit coverage for the retry, overlap, unfinished, and lost-message cases.
+
 ## 0.13.2 - 2026-08-17
 
 - Accept a `key` on `schedule`, naming a reminder for the item it is waiting
diff --git a/examples/failure-recovery/demo.ts b/examples/failure-recovery/demo.ts
index 9ab5edd..2643261 100644
--- a/examples/failure-recovery/demo.ts
+++ b/examples/failure-recovery/demo.ts
@@ -8,6 +8,7 @@ import { fork, type ChildProcess } from "node:child_process"
 import { createRuntime, type ActorReference, type MessageReference } from "solid-objects"
 import { sqlite } from "solid-objects/database/sqlite"
 import { RecoveryCounter } from "./actor.ts"
+import { assertSerializedExecution, parseSerializationEvent } from "./serialization.ts"
 
 interface WorkerMessage {
   event: string
@@ -15,12 +16,6 @@ interface WorkerMessage {
   processed?: number
 }
 
-interface SerializationEvent {
-  event: "start" | "finish"
-  messageId: string
-  at: number
-}
-
 interface ExternalEffectEvent {
   messageId: string
   attempt: number
@@ -74,12 +69,7 @@ async function proveSerialization(): Promise<{ finalState: number; overlap: fals
     join(controlDirectory, "serialization.jsonl"),
     parseSerializationEvent,
   )
-  assert.equal(events.length, 4)
-  const starts = events.filter((event) => event.event === "start")
-  const finishes = events.filter((event) => event.event === "finish")
-  assert.equal(starts.length, 2)
-  assert.equal(finishes.length, 2)
-  assert(Number(starts[1]?.at) >= Number(finishes[0]?.at))
+  assertSerializedExecution(events, { messageCount: 2 })
   const snapshot = await reference.snapshot()
   assert.equal(snapshot.count, 2)
   return { finalState: snapshot.count, overlap: false }
@@ -200,18 +190,6 @@ async function readJsonLines<Value>(
   return (await readFile(path, "utf8")).trim().split("\n").filter(Boolean).map(parse)
 }
 
-function parseSerializationEvent(line: string): SerializationEvent {
-  const event = JSON.parse(line) as Partial<SerializationEvent>
-  if (
-    (event.event !== "start" && event.event !== "finish") ||
-    typeof event.messageId !== "string" ||
-    typeof event.at !== "number"
-  ) {
-    throw new TypeError("invalid serialization event")
-  }
-  return { event: event.event, messageId: event.messageId, at: event.at }
-}
-
 function parseExternalEffectEvent(line: string): ExternalEffectEvent {
   const event = JSON.parse(line) as Partial<ExternalEffectEvent>
   if (
diff --git a/examples/failure-recovery/serialization.ts b/examples/failure-recovery/serialization.ts
new file mode 100644
index 0000000..4bf390a
--- /dev/null
+++ b/examples/failure-recovery/serialization.ts
@@ -0,0 +1,53 @@
+import assert from "node:assert/strict"
+
+export interface SerializationEvent {
+  event: "start" | "finish"
+  messageId: string
+  at: number
+}
+
+export function parseSerializationEvent(line: string): SerializationEvent {
+  const event = JSON.parse(line) as Partial<SerializationEvent>
+  if (
+    (event.event !== "start" && event.event !== "finish") ||
+    typeof event.messageId !== "string" ||
+    typeof event.at !== "number"
+  ) {
+    throw new TypeError("invalid serialization event")
+  }
+  return { event: event.event, messageId: event.messageId, at: event.at }
+}
+
+// One identity executes one operation at a time. A worker that loses its lease
+// mid-operation leaves the replacement to execute the same message again, so
+// the proof counts the messages that ran and the executions that overlapped,
+// not the executions themselves.
+export function assertSerializedExecution(
+  events: readonly SerializationEvent[],
+  options: { messageCount: number },
+): void {
+  const ordered = [...events].sort((left, right) => left.at - right.at)
+
+  let open: string | undefined
+  for (const event of ordered) {
+    if (event.event === "start") {
+      assert.equal(
+        open,
+        undefined,
+        `execution of ${event.messageId} overlaps the open execution of ${open}`,
+      )
+      open = event.messageId
+      continue
+    }
+    assert.equal(event.messageId, open, `finish of ${event.messageId} has no matching start`)
+    open = undefined
+  }
+  assert.equal(open, undefined, `execution of ${open} never wrote a finish`)
+
+  const messageIds = new Set(ordered.map((event) => event.messageId))
+  assert.equal(
+    messageIds.size,
+    options.messageCount,
+    `expected ${options.messageCount} messages to run, saw ${messageIds.size}`,
+  )
+}
diff --git a/test/failure-recovery-serialization.test.ts b/test/failure-recovery-serialization.test.ts
new file mode 100644
index 0000000..4698b0e
--- /dev/null
+++ b/test/failure-recovery-serialization.test.ts
@@ -0,0 +1,52 @@
+import { describe, expect, it } from "vitest"
+import {
+  assertSerializedExecution,
+  type SerializationEvent,
+} from "../examples/failure-recovery/serialization.js"
+
+function execution(messageId: string, startedAt: number, finishedAt: number): SerializationEvent[] {
+  return [
+    { event: "start", messageId, at: startedAt },
+    { event: "finish", messageId, at: finishedAt },
+  ]
+}
+
+describe("serialization proof", () => {
+  it("accepts two executions that do not overlap", () => {
+    const events = [...execution("a", 10, 20), ...execution("b", 30, 40)]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).not.toThrow()
+  })
+
+  // A worker can lose its lease mid-operation, and the replacement executes the
+  // same message again. That is the at-least-once contract, so the proof counts
+  // messages rather than executions.
+  it("accepts a message that executes twice after a lost lease", () => {
+    const events = [...execution("a", 10, 20), ...execution("a", 30, 40), ...execution("b", 50, 60)]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).not.toThrow()
+  })
+
+  it("rejects executions that overlap", () => {
+    const events: SerializationEvent[] = [
+      { event: "start", messageId: "a", at: 10 },
+      { event: "start", messageId: "b", at: 15 },
+      { event: "finish", messageId: "a", at: 20 },
+      { event: "finish", messageId: "b", at: 25 },
+    ]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/overlap/)
+  })
+
+  it("rejects an execution that never finished", () => {
+    const events = [...execution("a", 10, 20), { event: "start", messageId: "b", at: 30 } as const]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/finish/)
+  })
+
+  it("rejects a run that lost one of the messages", () => {
+    const events = [...execution("a", 10, 20), ...execution("a", 30, 40)]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/message/)
+  })
+})

From fd29399b1ee9fd246e3ae77f03ffa7e5a4ce7c08 Mon Sep 17 00:00:00 2001
From: Lucas Carlson <lucas@carlson.net>
Date: Tue, 18 Aug 2026 09:11:04 -0700
Subject: [PATCH 2/4] fix: let a fenced attempt overlap its replacement

The first rule demanded strict alternation across the whole log, which
rejects the case it was written to accept. The attempt that loses its
lease is the one that was slow, so it is still running when the
replacement starts, and both write to the control file.

Overlap is now allowed only when a message ran more than once, which is
the only thing that produces a stale owner. Without a retry the proof
still demands strict serialization. The rule tracks open attempts per
message, so a message may be open twice.

The demo reports executions, retried, and overlapped instead of a
hardcoded overlap: false, so a run says what it actually saw.

Found by Greptile on the first commit. The stale-overlap case is now a
test, and it fails against the alternation rule.
---
 CHANGELOG.md                                | 11 +++--
 examples/failure-recovery/demo.ts           | 12 +++--
 examples/failure-recovery/serialization.ts  | 53 +++++++++++++++------
 test/failure-recovery-serialization.test.ts | 44 +++++++++++++++--
 4 files changed, 94 insertions(+), 26 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8242f8a..2b75528 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,10 +6,13 @@
   than executions. A worker that loses its lease mid-operation leaves the
   replacement to execute the same message again, which is the at-least-once
   contract, so the proof failed on slower machines for behaviour it documents
-  elsewhere. It now asserts that executions never overlap, that every start has
-  a finish, and that exactly the two sent messages ran, with the committed state
-  check unchanged. `assertSerializedExecution` moved into its own module and has
-  unit coverage for the retry, overlap, unfinished, and lost-message cases.
+  elsewhere. It now asserts that every start has a finish, that exactly the two
+  sent messages ran, and that executions overlap only when a lost lease explains
+  it, because the stale attempt keeps running until it notices. The committed
+  state check is unchanged, and the demo reports the executions it saw.
+  `assertSerializedExecution` moved into its own module with unit coverage for
+  the clean, retried, stale-overlap, unexplained-overlap, unfinished,
+  unmatched-finish, and lost-message cases.
 
 ## 0.13.2 - 2026-08-17
 
diff --git a/examples/failure-recovery/demo.ts b/examples/failure-recovery/demo.ts
index 2643261..ba0f3a7 100644
--- a/examples/failure-recovery/demo.ts
+++ b/examples/failure-recovery/demo.ts
@@ -8,7 +8,11 @@ import { fork, type ChildProcess } from "node:child_process"
 import { createRuntime, type ActorReference, type MessageReference } from "solid-objects"
 import { sqlite } from "solid-objects/database/sqlite"
 import { RecoveryCounter } from "./actor.ts"
-import { assertSerializedExecution, parseSerializationEvent } from "./serialization.ts"
+import {
+  assertSerializedExecution,
+  parseSerializationEvent,
+  type SerializationProof,
+} from "./serialization.ts"
 
 interface WorkerMessage {
   event: string
@@ -54,7 +58,7 @@ try {
 
 assert.equal(existsSync(directory), false)
 
-async function proveSerialization(): Promise<{ finalState: number; overlap: false }> {
+async function proveSerialization(): Promise<SerializationProof & { finalState: number }> {
   const controlDirectory = join(directory, "serialization")
   await mkdir(controlDirectory)
   const reference = runtime.ref(RecoveryCounter, "serialized")
@@ -69,10 +73,10 @@ async function proveSerialization(): Promise<{ finalState: number; overlap: fals
     join(controlDirectory, "serialization.jsonl"),
     parseSerializationEvent,
   )
-  assertSerializedExecution(events, { messageCount: 2 })
+  const proof = assertSerializedExecution(events, { messageCount: 2 })
   const snapshot = await reference.snapshot()
   assert.equal(snapshot.count, 2)
-  return { finalState: snapshot.count, overlap: false }
+  return { ...proof, finalState: snapshot.count }
 }
 
 async function proveCrashRecovery(): Promise<{
diff --git a/examples/failure-recovery/serialization.ts b/examples/failure-recovery/serialization.ts
index 4bf390a..d14444d 100644
--- a/examples/failure-recovery/serialization.ts
+++ b/examples/failure-recovery/serialization.ts
@@ -6,6 +6,12 @@ export interface SerializationEvent {
   at: number
 }
 
+export interface SerializationProof {
+  executions: number
+  retried: boolean
+  overlapped: boolean
+}
+
 export function parseSerializationEvent(line: string): SerializationEvent {
   const event = JSON.parse(line) as Partial<SerializationEvent>
   if (
@@ -18,31 +24,41 @@ export function parseSerializationEvent(line: string): SerializationEvent {
   return { event: event.event, messageId: event.messageId, at: event.at }
 }
 
-// One identity executes one operation at a time. A worker that loses its lease
-// mid-operation leaves the replacement to execute the same message again, so
-// the proof counts the messages that ran and the executions that overlapped,
-// not the executions themselves.
+// One identity commits one state transition at a time. The control file is
+// written outside the transaction, so it records execution attempts rather than
+// commits: a worker that loses its lease keeps running until it notices, and
+// its replacement executes the same message again. Those two attempts can
+// overlap in this log, and the fenced write is what stops them both counting.
+// The committed state is the assertion that proves it.
+//
+// Without a retry there is no stale owner, so nothing excuses an overlap and
+// the proof still demands strict serialization.
 export function assertSerializedExecution(
   events: readonly SerializationEvent[],
   options: { messageCount: number },
-): void {
+): SerializationProof {
   const ordered = [...events].sort((left, right) => left.at - right.at)
 
-  let open: string | undefined
+  const open = new Map<string, number>()
+  let running = 0
+  let concurrent = 0
+  let executions = 0
+
   for (const event of ordered) {
     if (event.event === "start") {
-      assert.equal(
-        open,
-        undefined,
-        `execution of ${event.messageId} overlaps the open execution of ${open}`,
-      )
-      open = event.messageId
+      open.set(event.messageId, (open.get(event.messageId) ?? 0) + 1)
+      executions += 1
+      running += 1
+      concurrent = Math.max(concurrent, running)
       continue
     }
-    assert.equal(event.messageId, open, `finish of ${event.messageId} has no matching start`)
-    open = undefined
+    const openForMessage = open.get(event.messageId) ?? 0
+    assert(openForMessage > 0, `finish of ${event.messageId} has no matching start`)
+    open.set(event.messageId, openForMessage - 1)
+    running -= 1
   }
-  assert.equal(open, undefined, `execution of ${open} never wrote a finish`)
+
+  assert.equal(running, 0, "an execution never wrote a finish")
 
   const messageIds = new Set(ordered.map((event) => event.messageId))
   assert.equal(
@@ -50,4 +66,11 @@ export function assertSerializedExecution(
     options.messageCount,
     `expected ${options.messageCount} messages to run, saw ${messageIds.size}`,
   )
+
+  const retried = executions > options.messageCount
+  if (!retried) {
+    assert.equal(concurrent, 1, "executions overlapped without a lost lease to explain it")
+  }
+
+  return { executions, retried, overlapped: concurrent > 1 }
 }
diff --git a/test/failure-recovery-serialization.test.ts b/test/failure-recovery-serialization.test.ts
index 4698b0e..1d86c49 100644
--- a/test/failure-recovery-serialization.test.ts
+++ b/test/failure-recovery-serialization.test.ts
@@ -15,7 +15,11 @@ describe("serialization proof", () => {
   it("accepts two executions that do not overlap", () => {
     const events = [...execution("a", 10, 20), ...execution("b", 30, 40)]
 
-    expect(() => assertSerializedExecution(events, { messageCount: 2 })).not.toThrow()
+    expect(assertSerializedExecution(events, { messageCount: 2 })).toEqual({
+      executions: 2,
+      retried: false,
+      overlapped: false,
+    })
   })
 
   // A worker can lose its lease mid-operation, and the replacement executes the
@@ -24,10 +28,34 @@ describe("serialization proof", () => {
   it("accepts a message that executes twice after a lost lease", () => {
     const events = [...execution("a", 10, 20), ...execution("a", 30, 40), ...execution("b", 50, 60)]
 
-    expect(() => assertSerializedExecution(events, { messageCount: 2 })).not.toThrow()
+    expect(assertSerializedExecution(events, { messageCount: 2 })).toEqual({
+      executions: 3,
+      retried: true,
+      overlapped: false,
+    })
   })
 
-  it("rejects executions that overlap", () => {
+  // The stale attempt is what lost the lease, so it is still running when the
+  // replacement starts. Its writes are fenced out, and the committed state is
+  // what proves that, so the log is allowed to interleave here.
+  it("accepts a stale attempt that is still running when its replacement starts", () => {
+    const events: SerializationEvent[] = [
+      { event: "start", messageId: "a", at: 10 },
+      { event: "start", messageId: "a", at: 20 },
+      { event: "finish", messageId: "a", at: 30 },
+      { event: "finish", messageId: "a", at: 40 },
+      ...execution("b", 50, 60),
+    ]
+
+    expect(assertSerializedExecution(events, { messageCount: 2 })).toEqual({
+      executions: 3,
+      retried: true,
+      overlapped: true,
+    })
+  })
+
+  // Without a retry there is no stale owner, so nothing excuses an overlap.
+  it("rejects executions that overlap when no message ran twice", () => {
     const events: SerializationEvent[] = [
       { event: "start", messageId: "a", at: 10 },
       { event: "start", messageId: "b", at: 15 },
@@ -44,6 +72,16 @@ describe("serialization proof", () => {
     expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/finish/)
   })
 
+  it("rejects a finish with no start", () => {
+    const events: SerializationEvent[] = [
+      ...execution("a", 10, 20),
+      { event: "finish", messageId: "b", at: 30 },
+      ...execution("b", 40, 50),
+    ]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/start/)
+  })
+
   it("rejects a run that lost one of the messages", () => {
     const events = [...execution("a", 10, 20), ...execution("a", 30, 40)]
 

From 59e4a4f32ec77cd8ea9eb1e3d77b06be1b6f01a5 Mon Sep 17 00:00:00 2001
From: Lucas Carlson <lucas@carlson.net>
Date: Tue, 18 Aug 2026 09:16:46 -0700
Subject: [PATCH 3/4] fix: excuse the superseded attempt, not the survivors

Treating any retry as a licence to overlap let a real violation through:
once one message retried, two different messages could run at the same
time and the proof still passed.

A retry excuses only the attempt it superseded. The rule now tracks which
attempt of each message is the last one started, and asserts that at most
one message has its surviving attempt open at any moment. Earlier
attempts may overlap anything, because their writes are fenced.

Found by Greptile on the previous commit. The case is now a test, and
removing the assertion fails it along with the no-retry overlap case.
---
 CHANGELOG.md                                |  9 +++--
 examples/failure-recovery/serialization.ts  | 45 ++++++++++++++-------
 test/failure-recovery-serialization.test.ts | 14 +++++++
 3 files changed, 49 insertions(+), 19 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b75528..402c3dc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,12 +7,13 @@
   replacement to execute the same message again, which is the at-least-once
   contract, so the proof failed on slower machines for behaviour it documents
   elsewhere. It now asserts that every start has a finish, that exactly the two
-  sent messages ran, and that executions overlap only when a lost lease explains
-  it, because the stale attempt keeps running until it notices. The committed
+  sent messages ran, and that the surviving attempt of each message had the
+  identity to itself. A superseded attempt may overlap, because it keeps running
+  until it notices the lost lease and its write is fenced out. The committed
   state check is unchanged, and the demo reports the executions it saw.
   `assertSerializedExecution` moved into its own module with unit coverage for
-  the clean, retried, stale-overlap, unexplained-overlap, unfinished,
-  unmatched-finish, and lost-message cases.
+  the clean, retried, stale-overlap, surviving-overlap, unexplained-overlap,
+  unfinished, unmatched-finish, and lost-message cases.
 
 ## 0.13.2 - 2026-08-17
 
diff --git a/examples/failure-recovery/serialization.ts b/examples/failure-recovery/serialization.ts
index d14444d..4296116 100644
--- a/examples/failure-recovery/serialization.ts
+++ b/examples/failure-recovery/serialization.ts
@@ -27,35 +27,51 @@ export function parseSerializationEvent(line: string): SerializationEvent {
 // One identity commits one state transition at a time. The control file is
 // written outside the transaction, so it records execution attempts rather than
 // commits: a worker that loses its lease keeps running until it notices, and
-// its replacement executes the same message again. Those two attempts can
-// overlap in this log, and the fenced write is what stops them both counting.
-// The committed state is the assertion that proves it.
+// its replacement executes the same message again. A superseded attempt may
+// therefore overlap anything, because its write is fenced out and the committed
+// state is what proves it.
 //
-// Without a retry there is no stale owner, so nothing excuses an overlap and
-// the proof still demands strict serialization.
+// The surviving attempts are the ones that count, so the last attempt of each
+// message must still have the identity to itself.
 export function assertSerializedExecution(
   events: readonly SerializationEvent[],
   options: { messageCount: number },
 ): SerializationProof {
   const ordered = [...events].sort((left, right) => left.at - right.at)
 
-  const open = new Map<string, number>()
+  const lastStartedAt = new Map<string, number>()
+  for (const event of ordered) {
+    if (event.event === "start") lastStartedAt.set(event.messageId, event.at)
+  }
+
+  const open = new Map<string, number[]>()
+  const surviving = new Set<string>()
   let running = 0
   let concurrent = 0
   let executions = 0
 
   for (const event of ordered) {
     if (event.event === "start") {
-      open.set(event.messageId, (open.get(event.messageId) ?? 0) + 1)
+      open.set(event.messageId, [...(open.get(event.messageId) ?? []), event.at])
       executions += 1
       running += 1
       concurrent = Math.max(concurrent, running)
+      if (event.at === lastStartedAt.get(event.messageId)) {
+        surviving.add(event.messageId)
+        assert.equal(
+          surviving.size,
+          1,
+          `${[...surviving].join(" and ")} overlap, and neither was superseded by a retry`,
+        )
+      }
       continue
     }
-    const openForMessage = open.get(event.messageId) ?? 0
-    assert(openForMessage > 0, `finish of ${event.messageId} has no matching start`)
-    open.set(event.messageId, openForMessage - 1)
+    const openForMessage = open.get(event.messageId) ?? []
+    assert(openForMessage.length > 0, `finish of ${event.messageId} has no matching start`)
+    const startedAt = openForMessage.pop()
+    open.set(event.messageId, openForMessage)
     running -= 1
+    if (startedAt === lastStartedAt.get(event.messageId)) surviving.delete(event.messageId)
   }
 
   assert.equal(running, 0, "an execution never wrote a finish")
@@ -67,10 +83,9 @@ export function assertSerializedExecution(
     `expected ${options.messageCount} messages to run, saw ${messageIds.size}`,
   )
 
-  const retried = executions > options.messageCount
-  if (!retried) {
-    assert.equal(concurrent, 1, "executions overlapped without a lost lease to explain it")
+  return {
+    executions,
+    retried: executions > options.messageCount,
+    overlapped: concurrent > 1,
   }
-
-  return { executions, retried, overlapped: concurrent > 1 }
 }
diff --git a/test/failure-recovery-serialization.test.ts b/test/failure-recovery-serialization.test.ts
index 1d86c49..9b6e8a3 100644
--- a/test/failure-recovery-serialization.test.ts
+++ b/test/failure-recovery-serialization.test.ts
@@ -54,6 +54,20 @@ describe("serialization proof", () => {
     })
   })
 
+  // A retry excuses the superseded attempt, not the surviving ones. Message a
+  // retries, and then the attempt that replaced it runs at the same time as b.
+  it("rejects overlap between the surviving attempts even after a retry", () => {
+    const events: SerializationEvent[] = [
+      ...execution("a", 10, 20),
+      { event: "start", messageId: "a", at: 30 },
+      { event: "start", messageId: "b", at: 35 },
+      { event: "finish", messageId: "a", at: 40 },
+      { event: "finish", messageId: "b", at: 45 },
+    ]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/overlap/)
+  })
+
   // Without a retry there is no stale owner, so nothing excuses an overlap.
   it("rejects executions that overlap when no message ran twice", () => {
     const events: SerializationEvent[] = [

From b201fe2d01387fc238541af6f8c9c74d8b5add47 Mon Sep 17 00:00:00 2001
From: Lucas Carlson <lucas@carlson.net>
Date: Tue, 18 Aug 2026 10:40:01 -0700
Subject: [PATCH 4/4] fix: pair each start with its own finish

Two attempts of the same message can both be writing to the control
file at once: the superseded attempt keeps running until it notices the
lost lease, and its finish can land after the replacement's start. The
previous rule paired a start with whichever finish came next, so that
late finish read as the replacement's, and a second message could then
overlap a replacement that was in fact still running.

Each event now carries the message's attempt and the writing process, so
a start pairs only with the finish of that same execution. The proof
still asserts one thing about the surviving attempts, that none of them
overlap another message's surviving attempt, and lets a superseded
attempt overlap anything, because its write is fenced out and the
committed state is the assertion that proves it.

Found by Greptile on the previous commit, and reproduced as a test: a
superseded attempt that finishes after its replacement starts, followed
by a second message that starts while the replacement is still running.
Removing the overlap assertion fails that case and the no-retry case.
---
 CHANGELOG.md                                |  19 +--
 examples/failure-recovery/actor.ts          |  14 +-
 examples/failure-recovery/serialization.ts  | 138 +++++++++++++-------
 test/failure-recovery-serialization.test.ts | 124 ++++++++++++------
 4 files changed, 191 insertions(+), 104 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 402c3dc..ed09695 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,14 +6,17 @@
   than executions. A worker that loses its lease mid-operation leaves the
   replacement to execute the same message again, which is the at-least-once
   contract, so the proof failed on slower machines for behaviour it documents
-  elsewhere. It now asserts that every start has a finish, that exactly the two
-  sent messages ran, and that the surviving attempt of each message had the
-  identity to itself. A superseded attempt may overlap, because it keeps running
-  until it notices the lost lease and its write is fenced out. The committed
-  state check is unchanged, and the demo reports the executions it saw.
-  `assertSerializedExecution` moved into its own module with unit coverage for
-  the clean, retried, stale-overlap, surviving-overlap, unexplained-overlap,
-  unfinished, unmatched-finish, and lost-message cases.
+  elsewhere. Each serialization event now carries its attempt and process, so a
+  start pairs with its own finish instead of with whichever finish came next.
+  The proof asserts that every start has its own finish, that exactly the two
+  sent messages ran, and that the surviving attempt of each message never
+  overlaps another message's surviving attempt; a superseded attempt may
+  overlap anything, because it keeps running until it notices the lost lease and
+  its write is fenced out. The committed state check is unchanged, and the demo
+  reports the executions it saw. `assertSerializedExecution` moved into its own
+  module with unit coverage for the clean, retried, superseded-overlap,
+  still-running-replacement, unexplained-overlap, boundary, unfinished,
+  unmatched-finish, double-start, restart-after-finish, and lost-message cases.
 
 ## 0.13.2 - 2026-08-17
 
diff --git a/examples/failure-recovery/actor.ts b/examples/failure-recovery/actor.ts
index a6235b1..c372732 100644
--- a/examples/failure-recovery/actor.ts
+++ b/examples/failure-recovery/actor.ts
@@ -25,16 +25,14 @@ export class RecoveryCounter extends Actor {
   async serialize({ controlDirectory }: { controlDirectory: string }): Promise<number> {
     const message = this.currentMessage
     if (!message) throw new Error("serialize requires a durable message")
-    await appendFile(
-      join(controlDirectory, "serialization.jsonl"),
-      `${JSON.stringify({ event: "start", messageId: message.id, at: Date.now() })}\n`,
-    )
+    // The attempt and the process identify the execution, so a start pairs with
+    // its own finish even when a superseded attempt outlives its replacement.
+    const execution = { messageId: message.id, attempt: message.attempt, processId: process.pid }
+    const path = join(controlDirectory, "serialization.jsonl")
+    await appendFile(path, `${JSON.stringify({ event: "start", ...execution, at: Date.now() })}\n`)
     await new Promise((resolve) => setTimeout(resolve, 100))
     this.count += 1
-    await appendFile(
-      join(controlDirectory, "serialization.jsonl"),
-      `${JSON.stringify({ event: "finish", messageId: message.id, at: Date.now() })}\n`,
-    )
+    await appendFile(path, `${JSON.stringify({ event: "finish", ...execution, at: Date.now() })}\n`)
     return this.count
   }
 }
diff --git a/examples/failure-recovery/serialization.ts b/examples/failure-recovery/serialization.ts
index 4296116..61cdd64 100644
--- a/examples/failure-recovery/serialization.ts
+++ b/examples/failure-recovery/serialization.ts
@@ -3,13 +3,23 @@ import assert from "node:assert/strict"
 export interface SerializationEvent {
   event: "start" | "finish"
   messageId: string
+  attempt: number
+  processId: number
   at: number
 }
 
 export interface SerializationProof {
   executions: number
   retried: boolean
-  overlapped: boolean
+  supersededOverlap: boolean
+}
+
+interface Execution {
+  messageId: string
+  attempt: number
+  processId: number
+  startedAt: number
+  finishedAt: number
 }
 
 export function parseSerializationEvent(line: string): SerializationEvent {
@@ -17,75 +27,107 @@ export function parseSerializationEvent(line: string): SerializationEvent {
   if (
     (event.event !== "start" && event.event !== "finish") ||
     typeof event.messageId !== "string" ||
+    typeof event.attempt !== "number" ||
+    typeof event.processId !== "number" ||
     typeof event.at !== "number"
   ) {
     throw new TypeError("invalid serialization event")
   }
-  return { event: event.event, messageId: event.messageId, at: event.at }
+  return {
+    event: event.event,
+    messageId: event.messageId,
+    attempt: event.attempt,
+    processId: event.processId,
+    at: event.at,
+  }
 }
 
 // One identity commits one state transition at a time. The control file is
 // written outside the transaction, so it records execution attempts rather than
-// commits: a worker that loses its lease keeps running until it notices, and
-// its replacement executes the same message again. A superseded attempt may
-// therefore overlap anything, because its write is fenced out and the committed
-// state is what proves it.
+// commits: a worker that loses its lease keeps running until it notices, and its
+// replacement executes the same message under a higher attempt. The superseded
+// attempt may therefore overlap anything, because its write is fenced out and
+// the committed state is what proves it.
 //
-// The surviving attempts are the ones that count, so the last attempt of each
-// message must still have the identity to itself.
+// Each event carries its attempt and process, so a start pairs with its own
+// finish rather than with whichever finish arrived next. Without that, a
+// superseded attempt finishing late reads as its replacement finishing, and a
+// second message could then overlap a replacement that is still running.
 export function assertSerializedExecution(
   events: readonly SerializationEvent[],
   options: { messageCount: number },
 ): SerializationProof {
-  const ordered = [...events].sort((left, right) => left.at - right.at)
+  const executions = pairExecutions(events)
+
+  const messageIds = new Set(executions.map((execution) => execution.messageId))
+  assert.equal(
+    messageIds.size,
+    options.messageCount,
+    `expected ${options.messageCount} messages to run, saw ${messageIds.size}`,
+  )
+
+  const survivingAttempt = new Map<string, number>()
+  for (const execution of executions) {
+    const highest = survivingAttempt.get(execution.messageId) ?? 0
+    if (execution.attempt > highest) survivingAttempt.set(execution.messageId, execution.attempt)
+  }
+  const surviving = executions.filter(
+    (execution) => survivingAttempt.get(execution.messageId) === execution.attempt,
+  )
 
-  const lastStartedAt = new Map<string, number>()
-  for (const event of ordered) {
-    if (event.event === "start") lastStartedAt.set(event.messageId, event.at)
+  for (const [index, execution] of surviving.entries()) {
+    for (const other of surviving.slice(index + 1)) {
+      assert(
+        !overlaps(execution, other),
+        `${describe(execution)} and ${describe(other)} overlap, and neither was superseded`,
+      )
+    }
   }
 
-  const open = new Map<string, number[]>()
-  const surviving = new Set<string>()
-  let running = 0
-  let concurrent = 0
-  let executions = 0
+  const supersededOverlap = executions.some((execution) =>
+    executions.some((other) => other !== execution && overlaps(execution, other)),
+  )
 
-  for (const event of ordered) {
+  return {
+    executions: executions.length,
+    retried: executions.length > options.messageCount,
+    supersededOverlap,
+  }
+}
+
+function pairExecutions(events: readonly SerializationEvent[]): Execution[] {
+  const started = new Map<string, SerializationEvent>()
+  const executions: Execution[] = []
+
+  for (const event of [...events].sort((left, right) => left.at - right.at)) {
+    const key = `${event.messageId}#${event.attempt}#${event.processId}`
     if (event.event === "start") {
-      open.set(event.messageId, [...(open.get(event.messageId) ?? []), event.at])
-      executions += 1
-      running += 1
-      concurrent = Math.max(concurrent, running)
-      if (event.at === lastStartedAt.get(event.messageId)) {
-        surviving.add(event.messageId)
-        assert.equal(
-          surviving.size,
-          1,
-          `${[...surviving].join(" and ")} overlap, and neither was superseded by a retry`,
-        )
-      }
+      assert(!started.has(key), `${describe(event)} started twice`)
+      started.set(key, event)
       continue
     }
-    const openForMessage = open.get(event.messageId) ?? []
-    assert(openForMessage.length > 0, `finish of ${event.messageId} has no matching start`)
-    const startedAt = openForMessage.pop()
-    open.set(event.messageId, openForMessage)
-    running -= 1
-    if (startedAt === lastStartedAt.get(event.messageId)) surviving.delete(event.messageId)
+    const start = started.get(key)
+    assert(start !== undefined, `${describe(event)} finished with no matching start`)
+    started.delete(key)
+    executions.push({
+      messageId: event.messageId,
+      attempt: event.attempt,
+      processId: event.processId,
+      startedAt: start.at,
+      finishedAt: event.at,
+    })
   }
 
-  assert.equal(running, 0, "an execution never wrote a finish")
+  const unfinished = [...started.values()].map(describe)
+  assert.equal(unfinished.length, 0, `${unfinished.join(", ")} never wrote a finish`)
 
-  const messageIds = new Set(ordered.map((event) => event.messageId))
-  assert.equal(
-    messageIds.size,
-    options.messageCount,
-    `expected ${options.messageCount} messages to run, saw ${messageIds.size}`,
-  )
+  return executions
+}
 
-  return {
-    executions,
-    retried: executions > options.messageCount,
-    overlapped: concurrent > 1,
-  }
+function overlaps(left: Execution, right: Execution): boolean {
+  return left.startedAt < right.finishedAt && right.startedAt < left.finishedAt
+}
+
+function describe(execution: { messageId: string; attempt: number }): string {
+  return `${execution.messageId} attempt ${execution.attempt}`
 }
diff --git a/test/failure-recovery-serialization.test.ts b/test/failure-recovery-serialization.test.ts
index 9b6e8a3..0982178 100644
--- a/test/failure-recovery-serialization.test.ts
+++ b/test/failure-recovery-serialization.test.ts
@@ -4,100 +4,144 @@ import {
   type SerializationEvent,
 } from "../examples/failure-recovery/serialization.js"
 
-function execution(messageId: string, startedAt: number, finishedAt: number): SerializationEvent[] {
+function execution(options: {
+  messageId: string
+  attempt: number
+  startedAt: number
+  finishedAt: number
+  processId?: number
+}): SerializationEvent[] {
+  const { messageId, attempt, startedAt, finishedAt, processId = attempt } = options
   return [
-    { event: "start", messageId, at: startedAt },
-    { event: "finish", messageId, at: finishedAt },
+    { event: "start", messageId, attempt, processId, at: startedAt },
+    { event: "finish", messageId, attempt, processId, at: finishedAt },
   ]
 }
 
 describe("serialization proof", () => {
   it("accepts two executions that do not overlap", () => {
-    const events = [...execution("a", 10, 20), ...execution("b", 30, 40)]
+    const events = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 20 }),
+      ...execution({ messageId: "b", attempt: 1, startedAt: 30, finishedAt: 40 }),
+    ]
 
     expect(assertSerializedExecution(events, { messageCount: 2 })).toEqual({
       executions: 2,
       retried: false,
-      overlapped: false,
+      supersededOverlap: false,
     })
   })
 
   // A worker can lose its lease mid-operation, and the replacement executes the
-  // same message again. That is the at-least-once contract, so the proof counts
-  // messages rather than executions.
+  // same message again under a higher attempt. That is the at-least-once
+  // contract, so the proof counts messages rather than executions.
   it("accepts a message that executes twice after a lost lease", () => {
-    const events = [...execution("a", 10, 20), ...execution("a", 30, 40), ...execution("b", 50, 60)]
+    const events = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 20 }),
+      ...execution({ messageId: "a", attempt: 2, startedAt: 30, finishedAt: 40 }),
+      ...execution({ messageId: "b", attempt: 1, startedAt: 50, finishedAt: 60 }),
+    ]
 
     expect(assertSerializedExecution(events, { messageCount: 2 })).toEqual({
       executions: 3,
       retried: true,
-      overlapped: false,
+      supersededOverlap: false,
     })
   })
 
-  // The stale attempt is what lost the lease, so it is still running when the
-  // replacement starts. Its writes are fenced out, and the committed state is
-  // what proves that, so the log is allowed to interleave here.
-  it("accepts a stale attempt that is still running when its replacement starts", () => {
-    const events: SerializationEvent[] = [
-      { event: "start", messageId: "a", at: 10 },
-      { event: "start", messageId: "a", at: 20 },
-      { event: "finish", messageId: "a", at: 30 },
-      { event: "finish", messageId: "a", at: 40 },
-      ...execution("b", 50, 60),
+  // The attempt that lost the lease is the one that was slow, so it is still
+  // running when its replacement starts. Its write is fenced out, and the
+  // committed state is what proves that, so the log may interleave here.
+  it("accepts a superseded attempt that outlives the start of its replacement", () => {
+    const events = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 30 }),
+      ...execution({ messageId: "a", attempt: 2, startedAt: 20, finishedAt: 40 }),
+      ...execution({ messageId: "b", attempt: 1, startedAt: 50, finishedAt: 60 }),
     ]
 
     expect(assertSerializedExecution(events, { messageCount: 2 })).toEqual({
       executions: 3,
       retried: true,
-      overlapped: true,
+      supersededOverlap: true,
     })
   })
 
-  // A retry excuses the superseded attempt, not the surviving ones. Message a
-  // retries, and then the attempt that replaced it runs at the same time as b.
-  it("rejects overlap between the surviving attempts even after a retry", () => {
-    const events: SerializationEvent[] = [
-      ...execution("a", 10, 20),
-      { event: "start", messageId: "a", at: 30 },
-      { event: "start", messageId: "b", at: 35 },
-      { event: "finish", messageId: "a", at: 40 },
-      { event: "finish", messageId: "b", at: 45 },
+  // The superseded attempt finishing late must not be read as its replacement
+  // finishing. The replacement is still running, so a second message that
+  // starts here is a real serialization failure.
+  it("rejects a second message that overlaps a still-running replacement", () => {
+    const events = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 35 }),
+      ...execution({ messageId: "a", attempt: 2, startedAt: 20, finishedAt: 60 }),
+      ...execution({ messageId: "b", attempt: 1, startedAt: 40, finishedAt: 50 }),
     ]
 
     expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/overlap/)
   })
 
-  // Without a retry there is no stale owner, so nothing excuses an overlap.
   it("rejects executions that overlap when no message ran twice", () => {
-    const events: SerializationEvent[] = [
-      { event: "start", messageId: "a", at: 10 },
-      { event: "start", messageId: "b", at: 15 },
-      { event: "finish", messageId: "a", at: 20 },
-      { event: "finish", messageId: "b", at: 25 },
+    const events = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 20 }),
+      ...execution({ messageId: "b", attempt: 1, startedAt: 15, finishedAt: 25 }),
     ]
 
     expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/overlap/)
   })
 
+  it("accepts one execution that ends exactly as the next begins", () => {
+    const events = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 20 }),
+      ...execution({ messageId: "b", attempt: 1, startedAt: 20, finishedAt: 30 }),
+    ]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).not.toThrow()
+  })
+
   it("rejects an execution that never finished", () => {
-    const events = [...execution("a", 10, 20), { event: "start", messageId: "b", at: 30 } as const]
+    const events: SerializationEvent[] = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 20 }),
+      { event: "start", messageId: "b", attempt: 1, processId: 1, at: 30 },
+    ]
 
     expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/finish/)
   })
 
   it("rejects a finish with no start", () => {
     const events: SerializationEvent[] = [
-      ...execution("a", 10, 20),
-      { event: "finish", messageId: "b", at: 30 },
-      ...execution("b", 40, 50),
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 20 }),
+      { event: "finish", messageId: "b", attempt: 1, processId: 1, at: 30 },
     ]
 
     expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/start/)
   })
 
+  it("rejects one attempt that started twice", () => {
+    const events: SerializationEvent[] = [
+      { event: "start", messageId: "a", attempt: 1, processId: 1, at: 10 },
+      { event: "start", messageId: "a", attempt: 1, processId: 1, at: 15 },
+      { event: "finish", messageId: "a", attempt: 1, processId: 1, at: 20 },
+      { event: "finish", messageId: "a", attempt: 1, processId: 1, at: 25 },
+      ...execution({ messageId: "b", attempt: 1, startedAt: 30, finishedAt: 40 }),
+    ]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/twice/)
+  })
+
+  it("rejects an attempt that starts again after it finished", () => {
+    const events: SerializationEvent[] = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 20 }),
+      { event: "start", messageId: "a", attempt: 1, processId: 1, at: 25 },
+      ...execution({ messageId: "b", attempt: 1, startedAt: 30, finishedAt: 40 }),
+    ]
+
+    expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/finish/)
+  })
+
   it("rejects a run that lost one of the messages", () => {
-    const events = [...execution("a", 10, 20), ...execution("a", 30, 40)]
+    const events = [
+      ...execution({ messageId: "a", attempt: 1, startedAt: 10, finishedAt: 20 }),
+      ...execution({ messageId: "a", attempt: 2, startedAt: 30, finishedAt: 40 }),
+    ]
 
     expect(() => assertSerializedExecution(events, { messageCount: 2 })).toThrow(/message/)
   })