From f64b72c5655083f973f12a3d9f11d7f588e6af01 Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 22:19:08 -0700
Subject: [PATCH 1/5] feat: port Tesota's ProviderRetry model as a machine

Stage 10's target from Tesota is one of its design models ported with its
planted faults detected. ProviderRetry exercises time and cancellation.
Its choice of the next time depends on the state, so it is two events,
which the explorer can enumerate. Every obligation is proved with four
helper invariants, the explorer reaches all 148 states, and each planted
fault is refuted by the shortest run that breaks it.

Refs #82
---
 .../provider-retry-ignore-cancel-fault.accord | 104 +++++++++++++++++
 .../provider-retry-replay-tool-fault.accord   | 103 +++++++++++++++++
 conformance/cases/provider-retry.accord       | 109 ++++++++++++++++++
 3 files changed, 316 insertions(+)
 create mode 100644 conformance/cases/provider-retry-ignore-cancel-fault.accord
 create mode 100644 conformance/cases/provider-retry-replay-tool-fault.accord
 create mode 100644 conformance/cases/provider-retry.accord

diff --git a/conformance/cases/provider-retry-ignore-cancel-fault.accord b/conformance/cases/provider-retry-ignore-cancel-fault.accord
new file mode 100644
index 0000000..aa57c44
--- /dev/null
+++ b/conformance/cases/provider-retry-ignore-cancel-fault.accord
@@ -0,0 +1,104 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, refuted, proved, proved, proved, proved, proved, proved, proved, proved
+// The model's `IgnoreCancel` fault: the post-wait guard ignores cancellation,
+// so a retry that starts after `cancel` makes another call.
+
+/// Where a retried model call stands.
+enum RetryPhase { Failed, Waiting, Calling, Ended }
+
+/// A failed model call, retried within a budget and a time window.
+machine ProviderRetry {
+    intent "Retry a failed model call at most three times within its window, wait before each retry, never call again after cancellation, and never repeat a completed tool."
+
+    state {
+        phase: RetryPhase,
+        time: i32,
+        due: i32,
+        retries: i32,
+        calls: i32,
+        stopped: Bool,
+        calls_at_stop: i32,
+        terminal: Bool,
+        last_start: i32,
+        last_due: i32,
+        tools: i32,
+    }
+
+    init start(is_terminal: Bool) {
+        next {
+            phase: Failed,
+            time: 0,
+            due: 0,
+            retries: 0,
+            calls: 1,
+            stopped: false,
+            calls_at_stop: 0,
+            terminal: is_terminal,
+            last_start: 0,
+            last_due: 0,
+            tools: 1,
+        }
+    }
+
+    event schedule(delay: i32)
+        requires phase == Failed
+        requires delay == 1 or delay == 60 or delay == 121
+    {
+        if not terminal and not stopped and retries < 3 and time + delay < 120 {
+            next { phase: Waiting, due: time + delay, retries: retries + 1 }
+        } else {
+            next { phase: Ended }
+        }
+    }
+
+    event advance_to_due()
+        requires phase == Waiting and time < 120 and due >= time
+    {
+        next { time: due }
+    }
+
+    event advance_to_end()
+        requires phase == Waiting and time < 120
+    {
+        next { time: 120 }
+    }
+
+    event cancel()
+        requires not stopped and phase != Ended
+    {
+        next { stopped: true, calls_at_stop: calls }
+    }
+
+    event start_call()
+        requires phase == Waiting and time >= due and time < 120
+    {
+        next { phase: Calling, calls: calls + 1, last_start: time, last_due: due }
+    }
+
+    event stop_wait()
+        requires phase == Waiting and (stopped or time >= 120)
+    {
+        next { phase: Ended }
+    }
+
+    event failure(is_terminal: Bool)
+        requires phase == Calling
+    {
+        next { phase: Failed, terminal: is_terminal }
+    }
+
+    event success()
+        requires phase == Calling
+    {
+        next { phase: Ended }
+    }
+
+    invariant bounds: retries <= 3 and calls <= 4 and last_start < 120
+    invariant cancel_stops_calls: stopped implies calls == calls_at_stop
+    invariant wait_respected: last_start >= last_due
+    invariant tools_stay: tools == 1
+
+    helper invariant calls_follow_retries: calls <= retries + 1
+    helper invariant waiting_before_call: phase == Waiting implies calls <= retries
+    helper invariant time_in_window: time <= 120
+    helper invariant due_in_window: due <= 120
+}
diff --git a/conformance/cases/provider-retry-replay-tool-fault.accord b/conformance/cases/provider-retry-replay-tool-fault.accord
new file mode 100644
index 0000000..62b4d1f
--- /dev/null
+++ b/conformance/cases/provider-retry-replay-tool-fault.accord
@@ -0,0 +1,103 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, refuted, proved, proved, proved, proved, proved, proved, proved, proved, proved
+// The model's `ReplayTool` fault: a retry replays the completed tool.
+
+/// Where a retried model call stands.
+enum RetryPhase { Failed, Waiting, Calling, Ended }
+
+/// A failed model call, retried within a budget and a time window.
+machine ProviderRetry {
+    intent "Retry a failed model call at most three times within its window, wait before each retry, never call again after cancellation, and never repeat a completed tool."
+
+    state {
+        phase: RetryPhase,
+        time: i32,
+        due: i32,
+        retries: i32,
+        calls: i32,
+        stopped: Bool,
+        calls_at_stop: i32,
+        terminal: Bool,
+        last_start: i32,
+        last_due: i32,
+        tools: i32,
+    }
+
+    init start(is_terminal: Bool) {
+        next {
+            phase: Failed,
+            time: 0,
+            due: 0,
+            retries: 0,
+            calls: 1,
+            stopped: false,
+            calls_at_stop: 0,
+            terminal: is_terminal,
+            last_start: 0,
+            last_due: 0,
+            tools: 1,
+        }
+    }
+
+    event schedule(delay: i32)
+        requires phase == Failed
+        requires delay == 1 or delay == 60 or delay == 121
+    {
+        if not terminal and not stopped and retries < 3 and time + delay < 120 {
+            next { phase: Waiting, due: time + delay, retries: retries + 1 }
+        } else {
+            next { phase: Ended }
+        }
+    }
+
+    event advance_to_due()
+        requires phase == Waiting and time < 120 and due >= time
+    {
+        next { time: due }
+    }
+
+    event advance_to_end()
+        requires phase == Waiting and time < 120
+    {
+        next { time: 120 }
+    }
+
+    event cancel()
+        requires not stopped and phase != Ended
+    {
+        next { stopped: true, calls_at_stop: calls }
+    }
+
+    event start_call()
+        requires phase == Waiting and time >= due and time < 120 and not stopped
+    {
+        next { phase: Calling, calls: calls + 1, last_start: time, last_due: due, tools: tools + 1 }
+    }
+
+    event stop_wait()
+        requires phase == Waiting and (stopped or time >= 120)
+    {
+        next { phase: Ended }
+    }
+
+    event failure(is_terminal: Bool)
+        requires phase == Calling
+    {
+        next { phase: Failed, terminal: is_terminal }
+    }
+
+    event success()
+        requires phase == Calling
+    {
+        next { phase: Ended }
+    }
+
+    invariant bounds: retries <= 3 and calls <= 4 and last_start < 120
+    invariant cancel_stops_calls: stopped implies calls == calls_at_stop
+    invariant wait_respected: last_start >= last_due
+    invariant tools_stay: tools == 1
+
+    helper invariant calls_follow_retries: calls <= retries + 1
+    helper invariant waiting_before_call: phase == Waiting implies calls <= retries
+    helper invariant time_in_window: time <= 120
+    helper invariant due_in_window: due <= 120
+}
diff --git a/conformance/cases/provider-retry.accord b/conformance/cases/provider-retry.accord
new file mode 100644
index 0000000..9f1d72f
--- /dev/null
+++ b/conformance/cases/provider-retry.accord
@@ -0,0 +1,109 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved
+// Tesota's ProviderRetry design model (models/ProviderRetry.tla at
+// 4ef9b191), as a machine. Each choice the model leaves open is an event's
+// parameter, or two events where it depends on the state: `Advance` sets the
+// time to `due` or to the end of the window, so it is `advance_to_due` and
+// `advance_to_end`. The constant `route` and the stuttering `Done` are left
+// out. The four invariants aren't inductive on their own; the four helper
+// invariants make them so.
+
+/// Where a retried model call stands.
+enum RetryPhase { Failed, Waiting, Calling, Ended }
+
+/// A failed model call, retried within a budget and a time window.
+machine ProviderRetry {
+    intent "Retry a failed model call at most three times within its window, wait before each retry, never call again after cancellation, and never repeat a completed tool."
+
+    state {
+        phase: RetryPhase,
+        time: i32,
+        due: i32,
+        retries: i32,
+        calls: i32,
+        stopped: Bool,
+        calls_at_stop: i32,
+        terminal: Bool,
+        last_start: i32,
+        last_due: i32,
+        tools: i32,
+    }
+
+    init start(is_terminal: Bool) {
+        next {
+            phase: Failed,
+            time: 0,
+            due: 0,
+            retries: 0,
+            calls: 1,
+            stopped: false,
+            calls_at_stop: 0,
+            terminal: is_terminal,
+            last_start: 0,
+            last_due: 0,
+            tools: 1,
+        }
+    }
+
+    event schedule(delay: i32)
+        requires phase == Failed
+        requires delay == 1 or delay == 60 or delay == 121
+    {
+        if not terminal and not stopped and retries < 3 and time + delay < 120 {
+            next { phase: Waiting, due: time + delay, retries: retries + 1 }
+        } else {
+            next { phase: Ended }
+        }
+    }
+
+    event advance_to_due()
+        requires phase == Waiting and time < 120 and due >= time
+    {
+        next { time: due }
+    }
+
+    event advance_to_end()
+        requires phase == Waiting and time < 120
+    {
+        next { time: 120 }
+    }
+
+    event cancel()
+        requires not stopped and phase != Ended
+    {
+        next { stopped: true, calls_at_stop: calls }
+    }
+
+    event start_call()
+        requires phase == Waiting and time >= due and time < 120 and not stopped
+    {
+        next { phase: Calling, calls: calls + 1, last_start: time, last_due: due }
+    }
+
+    event stop_wait()
+        requires phase == Waiting and (stopped or time >= 120)
+    {
+        next { phase: Ended }
+    }
+
+    event failure(is_terminal: Bool)
+        requires phase == Calling
+    {
+        next { phase: Failed, terminal: is_terminal }
+    }
+
+    event success()
+        requires phase == Calling
+    {
+        next { phase: Ended }
+    }
+
+    invariant bounds: retries <= 3 and calls <= 4 and last_start < 120
+    invariant cancel_stops_calls: stopped implies calls == calls_at_stop
+    invariant wait_respected: last_start >= last_due
+    invariant tools_stay: tools == 1
+
+    helper invariant calls_follow_retries: calls <= retries + 1
+    helper invariant waiting_before_call: phase == Waiting implies calls <= retries
+    helper invariant time_in_window: time <= 120
+    helper invariant due_in_window: due <= 120
+}

From 46300bd0f5d5f859d6feaf922d9a9ff801da06d6 Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 22:24:41 -0700
Subject: [PATCH 2/5] feat: port opossum's circuit breaker state as a machine

Stage 10's target from outside Tesota is opossum's breaker, proved. The
port is faithful, so it claims only what opossum holds: a pending probe
implies half-open or shut down, and a call runs neither once shut down
nor while open and enabled. Every obligation is proved, and two planted
faults are refuted by runs. opossum's own behaviours that its states
don't suggest are listed in the file, and the exact error rate and the
rejected inconsistent restore are its two deliberate divergences.

Refs #82
---
 .../cases/opossum-admits-call-fault.accord    | 110 +++++++++++++++
 conformance/cases/opossum-trip-fault.accord   | 111 +++++++++++++++
 conformance/programs/opossum/breaker.accord   | 126 ++++++++++++++++++
 3 files changed, 347 insertions(+)
 create mode 100644 conformance/cases/opossum-admits-call-fault.accord
 create mode 100644 conformance/cases/opossum-trip-fault.accord
 create mode 100644 conformance/programs/opossum/breaker.accord

diff --git a/conformance/cases/opossum-admits-call-fault.accord b/conformance/cases/opossum-admits-call-fault.accord
new file mode 100644
index 0000000..19fddfa
--- /dev/null
+++ b/conformance/cases/opossum-admits-call-fault.accord
@@ -0,0 +1,110 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, refuted, proved, proved, proved, proved, proved, proved, proved, passed
+// opossum's breaker (conformance/programs/opossum) with a planted fault:
+// `admits_call` forgets that a shut-down breaker runs nothing.
+
+/// Where the breaker stands.
+pub enum BreakerPhase { Closed, Open, HalfOpen, Shutdown }
+
+/// A circuit breaker's state, without its timers, statistics or cache.
+pub machine Breaker {
+    intent "Let calls through while closed, refuse them while open, let one probe through when the reset timeout ends, and let nothing through once shut down."
+
+    state {
+        phase: BreakerPhase,
+        pending_close: Bool,
+        enabled: Bool,
+        warming_up: Bool,
+    }
+
+    init initial(is_enabled: Bool, is_warming_up: Bool) {
+        next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    /// A breaker restored from `options.state`; `open_expired` is whether more
+    /// than the reset timeout has passed since the saved `lastTimerAt`.
+    init restored(is_enabled: Bool, is_warming_up: Bool, closed: Bool, half_open: Bool, shut_down: Bool, open_expired: Bool)
+        requires not (closed and half_open)
+    decide {
+        | shut_down               => next { phase: Shutdown, pending_close: half_open, enabled: false, warming_up: is_warming_up }
+        | closed                  => next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+        | half_open or open_expired => next { phase: HalfOpen, pending_close: true, enabled: is_enabled, warming_up: is_warming_up }
+        | otherwise               => next { phase: Open, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    event close() {
+        if phase == Closed {
+            next { }
+        } else {
+            next { phase: Closed, pending_close: false }
+        }
+    }
+
+    /// opossum's `open()`; `open` is an Accord keyword.
+    event trip() {
+        if phase == Open {
+            next { }
+        } else {
+            next { phase: Open, pending_close: false }
+        }
+    }
+
+    /// The reset timeout ended: the next call is the probe.
+    event reset_elapsed() {
+        next { phase: HalfOpen, pending_close: true }
+    }
+
+    /// A protected call was let through; a half-open breaker's probe is used.
+    event call_admitted() {
+        next { pending_close: false }
+    }
+
+    event shut_down() {
+        next { phase: Shutdown, enabled: false }
+    }
+
+    event enable() {
+        next { enabled: true }
+    }
+
+    event disable() {
+        next { enabled: false }
+    }
+
+    event warm_up_ended() {
+        next { warming_up: false }
+    }
+
+    /// Whether a protected call runs now: closed, or holding its half-open probe.
+    fn admits() -> Bool {
+        phase == Closed or pending_close
+    }
+
+    /// Whether `fire()` runs the action at all: never once shut down, always
+    /// when disabled, and otherwise as `admits` says.
+    fn admits_call() -> Bool
+        ensures phase == Shutdown implies not result
+        ensures phase == Open and enabled implies not result
+    {
+        not enabled or phase == Closed or pending_close
+    }
+
+    /// Whether a failure opens the breaker, given the rolling window's counts.
+    fn opens_on_failure(fires: i64, failures: i64, volume_threshold: i64, threshold: i64) -> Bool
+        requires fires >= 0 and failures >= 0 and failures <= fires and fires <= 1000000000000
+        requires threshold >= 0 and threshold <= 1000000
+    decide {
+        | warming_up                                     => false
+        | fires < volume_threshold and phase != HalfOpen => false
+        | otherwise                                      => failures * 100 > threshold * fires or phase == HalfOpen
+    }
+
+    invariant pending_close_is_half_open: pending_close implies phase == HalfOpen or phase == Shutdown
+}
+
+example Breaker
+    initial(is_enabled: true, is_warming_up: false)
+    trip()
+    reset_elapsed()
+    call_admitted()
+    close()
+    gives phase == Closed and not pending_close
diff --git a/conformance/cases/opossum-trip-fault.accord b/conformance/cases/opossum-trip-fault.accord
new file mode 100644
index 0000000..5f43874
--- /dev/null
+++ b/conformance/cases/opossum-trip-fault.accord
@@ -0,0 +1,111 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, refuted, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, passed
+// opossum's breaker (conformance/programs/opossum) with a planted fault:
+// `trip` keeps `pending_close`, so a half-open breaker that trips is open and
+// still holds a probe.
+
+/// Where the breaker stands.
+pub enum BreakerPhase { Closed, Open, HalfOpen, Shutdown }
+
+/// A circuit breaker's state, without its timers, statistics or cache.
+pub machine Breaker {
+    intent "Let calls through while closed, refuse them while open, let one probe through when the reset timeout ends, and let nothing through once shut down."
+
+    state {
+        phase: BreakerPhase,
+        pending_close: Bool,
+        enabled: Bool,
+        warming_up: Bool,
+    }
+
+    init initial(is_enabled: Bool, is_warming_up: Bool) {
+        next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    /// A breaker restored from `options.state`; `open_expired` is whether more
+    /// than the reset timeout has passed since the saved `lastTimerAt`.
+    init restored(is_enabled: Bool, is_warming_up: Bool, closed: Bool, half_open: Bool, shut_down: Bool, open_expired: Bool)
+        requires not (closed and half_open)
+    decide {
+        | shut_down               => next { phase: Shutdown, pending_close: half_open, enabled: false, warming_up: is_warming_up }
+        | closed                  => next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+        | half_open or open_expired => next { phase: HalfOpen, pending_close: true, enabled: is_enabled, warming_up: is_warming_up }
+        | otherwise               => next { phase: Open, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    event close() {
+        if phase == Closed {
+            next { }
+        } else {
+            next { phase: Closed, pending_close: false }
+        }
+    }
+
+    /// opossum's `open()`; `open` is an Accord keyword.
+    event trip() {
+        if phase == Open {
+            next { }
+        } else {
+            next { phase: Open }
+        }
+    }
+
+    /// The reset timeout ended: the next call is the probe.
+    event reset_elapsed() {
+        next { phase: HalfOpen, pending_close: true }
+    }
+
+    /// A protected call was let through; a half-open breaker's probe is used.
+    event call_admitted() {
+        next { pending_close: false }
+    }
+
+    event shut_down() {
+        next { phase: Shutdown, enabled: false }
+    }
+
+    event enable() {
+        next { enabled: true }
+    }
+
+    event disable() {
+        next { enabled: false }
+    }
+
+    event warm_up_ended() {
+        next { warming_up: false }
+    }
+
+    /// Whether a protected call runs now: closed, or holding its half-open probe.
+    fn admits() -> Bool {
+        phase == Closed or pending_close
+    }
+
+    /// Whether `fire()` runs the action at all: never once shut down, always
+    /// when disabled, and otherwise as `admits` says.
+    fn admits_call() -> Bool
+        ensures phase == Shutdown implies not result
+        ensures phase == Open and enabled implies not result
+    {
+        phase != Shutdown and (not enabled or phase == Closed or pending_close)
+    }
+
+    /// Whether a failure opens the breaker, given the rolling window's counts.
+    fn opens_on_failure(fires: i64, failures: i64, volume_threshold: i64, threshold: i64) -> Bool
+        requires fires >= 0 and failures >= 0 and failures <= fires and fires <= 1000000000000
+        requires threshold >= 0 and threshold <= 1000000
+    decide {
+        | warming_up                                     => false
+        | fires < volume_threshold and phase != HalfOpen => false
+        | otherwise                                      => failures * 100 > threshold * fires or phase == HalfOpen
+    }
+
+    invariant pending_close_is_half_open: pending_close implies phase == HalfOpen or phase == Shutdown
+}
+
+example Breaker
+    initial(is_enabled: true, is_warming_up: false)
+    trip()
+    reset_elapsed()
+    call_admitted()
+    close()
+    gives phase == Closed and not pending_close
diff --git a/conformance/programs/opossum/breaker.accord b/conformance/programs/opossum/breaker.accord
new file mode 100644
index 0000000..fe32af9
--- /dev/null
+++ b/conformance/programs/opossum/breaker.accord
@@ -0,0 +1,126 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, passed
+// The state and decisions of opossum's CircuitBreaker (opossum 10.0.0, commit
+// decbedf63d7815049233e544dcb351590ff0c84e, lib/circuit.js), ported
+// faithfully as a machine. Emitted events, timers, the cache, the semaphore,
+// the rolling statistics and fallbacks stay in opossum; its adapter.patch
+// calls this module for every state change and decision.
+//
+// Where opossum's behaviour isn't what its states suggest, the port keeps it
+// and claims no more:
+// - any success while half-open closes the breaker, a late success from a
+//   call admitted before it opened included (`close` from `HalfOpen`);
+// - `close()` or `open()` after `shutdown()` leaves the shut-down state;
+// - `disable()` lets calls through whatever the state;
+// - `shutdown()` while half-open keeps `pending_close`.
+// Two divergences are deliberate: the error rate is compared exactly,
+// `failures * 100 > threshold * fires`, where opossum divides in floating
+// point, so a threshold must be a whole number; and a restored state that
+// says it is both closed and half-open, which opossum's own `toJSON` never
+// writes, is rejected.
+
+/// Where the breaker stands.
+pub enum BreakerPhase { Closed, Open, HalfOpen, Shutdown }
+
+/// A circuit breaker's state, without its timers, statistics or cache.
+pub machine Breaker {
+    intent "Let calls through while closed, refuse them while open, let one probe through when the reset timeout ends, and let nothing through once shut down."
+
+    state {
+        phase: BreakerPhase,
+        pending_close: Bool,
+        enabled: Bool,
+        warming_up: Bool,
+    }
+
+    init initial(is_enabled: Bool, is_warming_up: Bool) {
+        next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    /// A breaker restored from `options.state`; `open_expired` is whether more
+    /// than the reset timeout has passed since the saved `lastTimerAt`.
+    init restored(is_enabled: Bool, is_warming_up: Bool, closed: Bool, half_open: Bool, shut_down: Bool, open_expired: Bool)
+        requires not (closed and half_open)
+    decide {
+        | shut_down               => next { phase: Shutdown, pending_close: half_open, enabled: false, warming_up: is_warming_up }
+        | closed                  => next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+        | half_open or open_expired => next { phase: HalfOpen, pending_close: true, enabled: is_enabled, warming_up: is_warming_up }
+        | otherwise               => next { phase: Open, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    event close() {
+        if phase == Closed {
+            next { }
+        } else {
+            next { phase: Closed, pending_close: false }
+        }
+    }
+
+    /// opossum's `open()`; `open` is an Accord keyword.
+    event trip() {
+        if phase == Open {
+            next { }
+        } else {
+            next { phase: Open, pending_close: false }
+        }
+    }
+
+    /// The reset timeout ended: the next call is the probe.
+    event reset_elapsed() {
+        next { phase: HalfOpen, pending_close: true }
+    }
+
+    /// A protected call was let through; a half-open breaker's probe is used.
+    event call_admitted() {
+        next { pending_close: false }
+    }
+
+    event shut_down() {
+        next { phase: Shutdown, enabled: false }
+    }
+
+    event enable() {
+        next { enabled: true }
+    }
+
+    event disable() {
+        next { enabled: false }
+    }
+
+    event warm_up_ended() {
+        next { warming_up: false }
+    }
+
+    /// Whether a protected call runs now: closed, or holding its half-open probe.
+    fn admits() -> Bool {
+        phase == Closed or pending_close
+    }
+
+    /// Whether `fire()` runs the action at all: never once shut down, always
+    /// when disabled, and otherwise as `admits` says.
+    fn admits_call() -> Bool
+        ensures phase == Shutdown implies not result
+        ensures phase == Open and enabled implies not result
+    {
+        phase != Shutdown and (not enabled or phase == Closed or pending_close)
+    }
+
+    /// Whether a failure opens the breaker, given the rolling window's counts.
+    fn opens_on_failure(fires: i64, failures: i64, volume_threshold: i64, threshold: i64) -> Bool
+        requires fires >= 0 and failures >= 0 and failures <= fires and fires <= 1000000000000
+        requires threshold >= 0 and threshold <= 1000000
+    decide {
+        | warming_up                                     => false
+        | fires < volume_threshold and phase != HalfOpen => false
+        | otherwise                                      => failures * 100 > threshold * fires or phase == HalfOpen
+    }
+
+    invariant pending_close_is_half_open: pending_close implies phase == HalfOpen or phase == Shutdown
+}
+
+example Breaker
+    initial(is_enabled: true, is_warming_up: false)
+    trip()
+    reset_elapsed()
+    call_admitted()
+    close()
+    gives phase == Closed and not pending_close

From 7d85a6f0a0464c13c64d462114abdc4418321d6a Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 22:32:20 -0700
Subject: [PATCH 3/5] feat: run opossum's tests with the generated breaker
 module

adapter.patch makes opossum's lib/circuit.js keep its state in the
module built from the port and ask it for each decision; the script
runs opossum's lint and tests as released and with the module in place.

Refs #82
---
 conformance/programs/opossum/NOTICE        |  10 +
 conformance/programs/opossum/adapter.patch | 299 +++++++++++++++++++++
 scripts/check-opossum.sh                   |  58 ++++
 3 files changed, 367 insertions(+)
 create mode 100644 conformance/programs/opossum/NOTICE
 create mode 100644 conformance/programs/opossum/adapter.patch
 create mode 100644 scripts/check-opossum.sh

diff --git a/conformance/programs/opossum/NOTICE b/conformance/programs/opossum/NOTICE
new file mode 100644
index 0000000..e6c570c
--- /dev/null
+++ b/conformance/programs/opossum/NOTICE
@@ -0,0 +1,10 @@
+opossum circuit breaker state
+Author: Red Hat, Inc. (opossum's package.json)
+
+The port in breaker.accord is derived from opossum,
+https://github.com/nodeshift/opossum, release 10.0.0 at commit
+decbedf63d7815049233e544dcb351590ff0c84e (lib/circuit.js).
+It is licensed under Apache-2.0 (see LICENSE-APACHE at the repository root).
+The port states the breaker's state and its decisions as a machine;
+adapter.patch changes opossum's own lib/circuit.js to keep its state in the
+generated module and to ask it for each decision.
diff --git a/conformance/programs/opossum/adapter.patch b/conformance/programs/opossum/adapter.patch
new file mode 100644
index 0000000..36de688
--- /dev/null
+++ b/conformance/programs/opossum/adapter.patch
@@ -0,0 +1,299 @@
+diff --git a/lib/circuit.js b/lib/circuit.js
+index 82dd77f..012b177 100644
+--- a/lib/circuit.js
++++ b/lib/circuit.js
+@@ -4,19 +4,13 @@ const EventEmitter = require('events');
+ const Status = require('./status');
+ const Semaphore = require('./semaphore');
+ const MemoryCache = require('./cache');
++const Breaker = require('./breaker.mts');
+ 
+ const STATE = Symbol('state');
+-const OPEN = Symbol('open');
+-const CLOSED = Symbol('closed');
+-const HALF_OPEN = Symbol('half-open');
+-const PENDING_CLOSE = Symbol('pending-close');
+-const SHUTDOWN = Symbol('shutdown');
+ const FALLBACK_FUNCTION = Symbol('fallback');
+ const STATUS = Symbol('status');
+ const NAME = Symbol('name');
+ const GROUP = Symbol('group');
+-const ENABLED = Symbol('Enabled');
+-const WARMING_UP = Symbol('warming-up');
+ const VOLUME_THRESHOLD = Symbol('volume-threshold');
+ const OUR_ERROR = Symbol('our-error');
+ const RESET_TIMEOUT = Symbol('reset-timeout');
+@@ -180,6 +174,13 @@ class CircuitBreaker extends EventEmitter {
+     this.options.resetTimeout = options.resetTimeout ?? 30000;
+     this.options.errorThresholdPercentage =
+       options.errorThresholdPercentage ?? 50;
++    // The state machine compares the error rate exactly, so the threshold
++    // must be a whole number.
++    if (!Number.isInteger(this.options.errorThresholdPercentage)) {
++      throw new TypeError(
++        'options.errorThresholdPercentage must be a whole number'
++      );
++    }
+     this.options.rollingCountTimeout = options.rollingCountTimeout ?? 10000;
+     this.options.rollingCountBuckets = options.rollingCountBuckets ?? 10;
+     this.options.rollingPercentilesEnabled =
+@@ -238,7 +239,7 @@ class CircuitBreaker extends EventEmitter {
+     this[VOLUME_THRESHOLD] = Number.isInteger(options.volumeThreshold)
+       ? options.volumeThreshold
+       : 0;
+-    this[WARMING_UP] = options.allowWarmUp === true;
++    const allowWarmUp = options.allowWarmUp === true;
+ 
+     // The user can pass in a Status object to initialize the Status/stats
+     if (this.options.status) {
+@@ -252,31 +253,30 @@ class CircuitBreaker extends EventEmitter {
+       this[STATUS] = new Status(this.options);
+     }
+ 
+-    this[STATE] = CLOSED;
+-
++    let restored = null;
+     if (options.state) {
+-      this[ENABLED] = options.state.enabled !== false;
+-      this[WARMING_UP] = options.state.warmUp || this[WARMING_UP];
+-      // Closed if nothing is passed in
+-      this[CLOSED] = options.state.closed !== false;
+-      // These should be in sync
+-      this[HALF_OPEN] = this[PENDING_CLOSE] = options.state.halfOpen || false;
+-      // Open should be the opposite of closed,
+-      // but also the opposite of half_open
+-      this[OPEN] = !this[CLOSED] && !this[HALF_OPEN];
+-      this[SHUTDOWN] = options.state.shutdown || false;
++      const saved = options.state;
++      const closed = saved.closed !== false;
++      const halfOpen = Boolean(saved.halfOpen || false);
++      const shutdown = Boolean(saved.shutdown || false);
++      const expired = saved.lastTimerAt !== undefined &&
++        (Date.now() - saved.lastTimerAt) > this.options.resetTimeout;
++      this[STATE] = Breaker.restored(saved.enabled !== false,
++        Boolean(saved.warmUp || allowWarmUp), closed, halfOpen, shutdown,
++        expired);
++      if (shutdown) restored = 'shutdown';
++      else if (!closed && !halfOpen) restored = expired ? 'halfOpen' : 'open';
+     } else {
+-      this[PENDING_CLOSE] = false;
+-      this[ENABLED] = options.enabled !== false;
++      this[STATE] = Breaker.initial(options.enabled !== false, allowWarmUp);
+     }
+ 
+     this[FALLBACK_FUNCTION] = null;
+     this[NAME] = options.name || action.name || nextName();
+     this[GROUP] = options.group || this[NAME];
+ 
+-    if (this[WARMING_UP]) {
++    if (this[STATE].warmingUp) {
+       const timer = this[WARMUP_TIMEOUT] = setTimeout(
+-        _ => (this[WARMING_UP] = false),
++        _ => (this[STATE] = Breaker.warmUpEnded(this[STATE])),
+         this.options.rollingCountTimeout
+       );
+       if (typeof timer.unref === 'function') {
+@@ -331,8 +331,7 @@ class CircuitBreaker extends EventEmitter {
+      * @returns {void}
+      */
+     function _halfOpen (circuit) {
+-      circuit[STATE] = HALF_OPEN;
+-      circuit[PENDING_CLOSE] = true;
++      circuit[STATE] = Breaker.resetElapsed(circuit[STATE]);
+       circuit._renewAbortControllerIfNeeded();
+       /**
+        * Emitted after `options.resetTimeout` has elapsed, allowing for
+@@ -353,24 +352,15 @@ class CircuitBreaker extends EventEmitter {
+     });
+ 
+     // Prepopulate the State of the Breaker
+-    if (this[SHUTDOWN]) {
+-      this[STATE] = SHUTDOWN;
++    if (restored === 'shutdown') {
+       this.shutdown();
+-    } else if (this[CLOSED]) {
+-      this.close();
+-    } else if (this[OPEN]) {
+-      // If the state being passed in is OPEN but more time has elapsed
+-      // than the resetTimeout, then we should be in halfOpen state
+-      if (this.options.state.lastTimerAt !== undefined &&
+-        (Date.now() - this.options.state.lastTimerAt) >
+-        this.options.resetTimeout) {
+-        _halfOpen(this);
+-      } else {
+-        this.open();
+-      }
+-    } else if (this[HALF_OPEN]) {
+-      // Not sure if anything needs to be done here
+-      this[STATE] = HALF_OPEN;
++    } else if (restored === 'open') {
++      this.emit('open');
++    } else if (restored === 'halfOpen') {
++      // More time has elapsed than the resetTimeout since the saved state
++      // was opened, so the breaker is half-open.
++      this._renewAbortControllerIfNeeded();
++      this.emit('halfOpen', this.options.resetTimeout);
+     }
+   }
+ 
+@@ -395,12 +385,11 @@ class CircuitBreaker extends EventEmitter {
+    * @returns {void}
+    */
+   close () {
+-    if (this[STATE] !== CLOSED) {
++    if (this[STATE].phase !== 'closed') {
+       if (this[RESET_TIMEOUT]) {
+         clearTimeout(this[RESET_TIMEOUT]);
+       }
+-      this[STATE] = CLOSED;
+-      this[PENDING_CLOSE] = false;
++      this[STATE] = Breaker.close(this[STATE]);
+       this._renewAbortControllerIfNeeded();
+       /**
+        * Emitted when the breaker is reset allowing the action to execute again
+@@ -420,9 +409,8 @@ class CircuitBreaker extends EventEmitter {
+    * @returns {void}
+    */
+   open () {
+-    if (this[STATE] !== OPEN) {
+-      this[STATE] = OPEN;
+-      this[PENDING_CLOSE] = false;
++    if (this[STATE].phase !== 'open') {
++      this[STATE] = Breaker.trip(this[STATE]);
+       /**
+        * Emitted when the breaker opens because the action has
+        * failure percentage greater than `options.errorThresholdPercentage`.
+@@ -453,7 +441,7 @@ class CircuitBreaker extends EventEmitter {
+       clearTimeout(this[WARMUP_TIMEOUT]);
+     }
+     this.status.shutdown();
+-    this[STATE] = SHUTDOWN;
++    this[STATE] = Breaker.shutDown(this[STATE]);
+ 
+     // clear cache on shutdown
+     this.clearCache();
+@@ -464,7 +452,7 @@ class CircuitBreaker extends EventEmitter {
+    * @type {Boolean}
+    */
+   get isShutdown () {
+-    return this[STATE] === SHUTDOWN;
++    return this[STATE].phase === 'shutdown';
+   }
+ 
+   /**
+@@ -488,7 +476,7 @@ class CircuitBreaker extends EventEmitter {
+    * @type {Boolean}
+    */
+   get pendingClose () {
+-    return this[PENDING_CLOSE];
++    return this[STATE].pendingClose;
+   }
+ 
+   /**
+@@ -496,7 +484,7 @@ class CircuitBreaker extends EventEmitter {
+    * @type {Boolean}
+    */
+   get closed () {
+-    return this[STATE] === CLOSED;
++    return this[STATE].phase === 'closed';
+   }
+ 
+   /**
+@@ -504,7 +492,7 @@ class CircuitBreaker extends EventEmitter {
+    * @type {Boolean}
+    */
+   get opened () {
+-    return this[STATE] === OPEN;
++    return this[STATE].phase === 'open';
+   }
+ 
+   /**
+@@ -512,7 +500,7 @@ class CircuitBreaker extends EventEmitter {
+    * @type {Boolean}
+    */
+   get halfOpen () {
+-    return this[STATE] === HALF_OPEN;
++    return this[STATE].phase === 'half_open';
+   }
+ 
+   /**
+@@ -553,7 +541,7 @@ class CircuitBreaker extends EventEmitter {
+    * @type {Boolean}
+    */
+   get enabled () {
+-    return this[ENABLED];
++    return this[STATE].enabled;
+   }
+ 
+   /**
+@@ -561,7 +549,7 @@ class CircuitBreaker extends EventEmitter {
+    * @type {Boolean}
+    */
+   get warmUp () {
+-    return this[WARMING_UP];
++    return this[STATE].warmingUp;
+   }
+ 
+   /**
+@@ -656,7 +644,7 @@ class CircuitBreaker extends EventEmitter {
+     this.emit('fire', args);
+ 
+     // Protection, caches and coalesce disabled.
+-    if (!this[ENABLED]) {
++    if (!this[STATE].enabled) {
+       const result = this.action.apply(context, args);
+       return (typeof result.then === 'function')
+         ? result
+@@ -708,7 +696,7 @@ class CircuitBreaker extends EventEmitter {
+       this.emit('coalesceCacheMiss');
+     }
+ 
+-    if (!this.closed && !this.pendingClose) {
++    if (!Breaker.admits(this[STATE])) {
+       /**
+        * Emitted when the circuit breaker is open and failing fast
+        * @event CircuitBreaker#reject
+@@ -721,7 +709,7 @@ class CircuitBreaker extends EventEmitter {
+       return fallback(this, error, args) ||
+         Promise.reject(error);
+     }
+-    this[PENDING_CLOSE] = false;
++    this[STATE] = Breaker.callAdmitted(this[STATE]);
+ 
+     let timeout;
+     let timeoutError = false;
+@@ -898,7 +886,7 @@ class CircuitBreaker extends EventEmitter {
+    * @returns {void}
+    */
+   enable () {
+-    this[ENABLED] = true;
++    this[STATE] = Breaker.enable(this[STATE]);
+     this.status.startListeneningForRotateEvent();
+   }
+ 
+@@ -908,7 +896,7 @@ class CircuitBreaker extends EventEmitter {
+    * @returns {void}
+    */
+   disable () {
+-    this[ENABLED] = false;
++    this[STATE] = Breaker.disable(this[STATE]);
+     this.status.removeRotateBucketControllerListener();
+   }
+ 
+@@ -985,14 +973,9 @@ function fail (circuit, err, args, latency) {
+    * @type {Error}
+    */
+   circuit.emit('failure', err, latency, args);
+-  if (circuit.warmUp) return;
+-
+-  // check stats to see if the circuit should be opened
+   const stats = circuit.stats;
+-  if ((stats.fires < circuit.volumeThreshold) && !circuit.halfOpen) return;
+-  const errorRate = stats.failures / stats.fires * 100;
+-  if (errorRate > circuit.options.errorThresholdPercentage ||
+-    circuit.halfOpen) {
++  if (Breaker.opensOnFailure(circuit[STATE], stats.fires, stats.failures,
++    circuit.volumeThreshold, circuit.options.errorThresholdPercentage)) {
+     circuit.open();
+   }
+ }
diff --git a/scripts/check-opossum.sh b/scripts/check-opossum.sh
new file mode 100644
index 0000000..f4f625a
--- /dev/null
+++ b/scripts/check-opossum.sh
@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+# Stage 10's check against a state machine from outside Tesota: opossum's own
+# lint and tests, run once as released and once with its breaker state and
+# decisions kept in the module `accord build` writes from
+# conformance/programs/opossum, through adapter.patch.
+#
+# Usage: scripts/check-opossum.sh <empty folder> [opossum repository]
+# It needs git, Node 22 or later, npm with network access, and the solvers
+# (ACCORD_Z3 and ACCORD_CVC5). Both runs' output is kept in the folder.
+#
+# A few tests are known to fail in both runs on a slow or Windows machine:
+# a rolling-window test with a 10 ms window, and health-check timers that
+# fire after their test ended. A run passes when lint passes and every failing
+# assertion is one of those.
+set -euo pipefail
+
+work="${1:?usage: scripts/check-opossum.sh <empty folder> [opossum repository]}"
+repository="${2:-https://github.com/nodeshift/opossum}"
+commit=decbedf63d7815049233e544dcb351590ff0c84e
+root="$(cd "$(dirname "$0")/.." && pwd)"
+port="$root/conformance/programs/opossum"
+repo="$work/opossum"
+known='^not ok [0-9]+ (failures reset because no event emitter is provided and rollingCountTimeout set to 10ms|\.end\(\) already called.*|plan != count)$'
+
+if [ -e "$work" ] && [ -n "$(ls -A "$work")" ]; then
+  echo "$work: not empty" >&2
+  exit 2
+fi
+git -c core.autocrlf=false clone --quiet --no-checkout "$repository" "$repo"
+git -C "$repo" -c core.autocrlf=false checkout --quiet "$commit"
+(cd "$repo" && npm ci --ignore-scripts --no-audit --no-fund > "$work/npm.log" 2>&1)
+
+run() { # label
+  local log="$work/$1.log" status=0
+  (
+    cd "$repo"
+    npx eslint --ignore-path .gitignore .
+    npx tape test/*.js
+  ) > "$log" 2>&1 || status=$?
+  echo "$1: $(grep -E '^# (tests|pass|fail)' "$log" | tr '\n' ' ') (output in $log)"
+  local others
+  others="$(grep -E '^not ok' "$log" | tr -d '\r' | grep -Ev "$known" || true)"
+  if ! grep -qE '^# tests ' "$log" || [ -n "$others" ]; then
+    echo "$1: failed beyond the known tests (exit $status)" >&2
+    [ -n "$others" ] && echo "$others" >&2
+    return 1
+  fi
+}
+
+failed=0
+run original || failed=1
+
+(cd "$root" && cargo run --release --quiet -- build "$port" --out "$work/generated")
+cp "$work/generated/breaker.ts" "$repo/lib/breaker.mts"
+git -C "$repo" apply "$port/adapter.patch"
+git -C "$repo" status --short
+run generated || failed=1
+exit "$failed"

From ed354d43fe2a83944c467c193a8cd4b65c43fdf6 Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 22:32:21 -0700
Subject: [PATCH 4/5] docs: describe the opossum port and its check

Refs #82
---
 conformance/README.md | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/conformance/README.md b/conformance/README.md
index a7bfecc..35e00a3 100644
--- a/conformance/README.md
+++ b/conformance/README.md
@@ -84,6 +84,32 @@ Node 20, so CI doesn't run it. The port is licensed under Apache-2.0;
 attribution is in [`programs/axios-retry/NOTICE`](programs/axios-retry/NOTICE)
 and the source header.
 
+## opossum circuit breaker
+
+[`programs/opossum/`](programs/opossum) ports the state and decisions of
+opossum's `CircuitBreaker` from opossum 10.0.0 at commit
+`decbedf63d7815049233e544dcb351590ff0c84e` as a machine, with two faults,
+`opossum-admits-call-fault` and `opossum-trip-fault`, in [`cases/`](cases). Emitted events, timers, the cache,
+the semaphore, the rolling statistics and fallbacks stay in opossum. Where
+opossum's behaviour isn't what its states suggest, the port keeps it and
+claims no more: any success while half-open closes the breaker, a late one
+included. Two divergences are deliberate: the error rate is compared exactly,
+so `errorThresholdPercentage` must be a whole number, and a restored state
+that says it is both closed and half-open is rejected.
+
+[`adapter.patch`](programs/opossum/adapter.patch) is written by hand: it makes
+opossum's own `lib/circuit.js` keep its state in the generated `breaker.ts`,
+copied into opossum as `lib/breaker.mts` (in a `"type": "commonjs"` package,
+Node loads it only under that extension), and ask it for each decision. It
+throws a `TypeError` at construction for a fractional threshold.
+`scripts/check-opossum.sh <empty folder>` runs opossum's lint and tests as
+released and with the generated module in place. It needs git, Node 22 or
+later and network access, so CI doesn't run it. On the machine it was written
+on, test 331, a rolling window of 10 ms, and tests 547 to 549, health-check
+timers that fire after their test ended, fail in both runs; the check accepts
+those only. The port is licensed under Apache-2.0; attribution is in
+[`programs/opossum/NOTICE`](programs/opossum/NOTICE).
+
 ## Cedar partial authorization
 
 [`programs/cedar/`](programs/cedar) ports the Boolean decision in Cedar's

From dc2fd898115316eebd092a5c2202ad73190705f9 Mon Sep 17 00:00:00 2001
From: Canitas <112231952+Sequela02@users.noreply.github.com>
Date: Thu, 12 Nov 2026 22:37:50 -0700
Subject: [PATCH 5/5] docs: close stage 10 with both ports and the tla-ts
 comparison

Stage 10 is done when a Tesota design model is ported with its faults
detected and opossum's breaker is proved with its tests passing on the
generated module. Both hold, and the ProviderRetry port reaches the same
148 states and the same shortest fault traces as tla-ts on Tesota's
model. The opossum port gains its license header; opossum names no
copyright holder, so none is invented.

Refs #82
---
 ROADMAP.md                                    |  4 +--
 conformance/programs/opossum/breaker.accord   |  3 +++
 .../2026-11-12-stage-10-machines/README.md    | 25 +++++++++++++++++++
 3 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/ROADMAP.md b/ROADMAP.md
index b606ce5..f942ec1 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -133,8 +133,8 @@ Taken on 2026-11-07:
 | 7. Intents and the review view | `intent` declarations; the human view (intent, specification, examples, counterexamples, open cases, surviving mutants, what wasn't proved); the agent view as structured diagnostics | The review of `gate-rule` and an outside-domain rule is readable without their code | Built, check moved to the public phase ([#46](https://github.com/sequelcore/accord/issues/46)): the [gate and Cedar packets](docs/design/stage-7-review/README.md) await a reader from outside the project |
 | 8. TypeScript output | Accord compiled to a TypeScript module | Tesota's own tests pass with the generated rule in place of the original | Done ([#47](https://github.com/sequelcore/accord/issues/47)): `accord build` ([reference](docs/typescript.md)), checked against the interpreter; Tesota's typecheck and tests pass with the generated rules (`scripts/check-tesota.sh`), and axios-retry's lint and specs with its generated request predicates (`scripts/check-axios-retry.sh`) |
 | 9. Whole rules | Calls between functions, proved through the callee's contract; `all`, `any` and `count` over lists; length and indexing: what `verdict-rule`, the largest rule, and Cedar's policy-set evaluation need | `verdict-rule` and Cedar's policy-set evaluation ported and proved | Done ([#69](https://github.com/sequelcore/accord/issues/69)): `verdict-rule` in `conformance/programs/tesota/`, where Tesota's typecheck and tests pass with it generated (`scripts/check-tesota.sh`), and Cedar's policy-set evaluation in `conformance/programs/cedar/`, each with planted faults refuted; calls (`conformance/cases/call*.accord`) and lists (`list-*.accord`); [proof cost and undecided rate](docs/design/measurements/2026-11-12-stage-9-proof-cost/README.md) |
-| 10. State machines | `machine` declarations, invariants, explicit-state model checking, planted faults | A Tesota design model ported, its faults detected; the circuit breaker of [opossum](https://github.com/nodeshift/opossum) (Apache-2.0), closed, open and half-open, proved, and opossum's tests pass with the generated module | Next ([#82](https://github.com/sequelcore/accord/issues/82)) |
-| 11. Structured data | Records, sum types and `match`, recursion with `decreases`, `Text` operations beyond equality | Version comparison from [node-semver](https://github.com/npm/node-semver) (ISC) proved, and node-semver's tests for it pass with the generated module | |
+| 10. State machines | `machine` declarations, invariants, explicit-state model checking, planted faults | A Tesota design model ported, its faults detected; the circuit breaker of [opossum](https://github.com/nodeshift/opossum) (Apache-2.0), closed, open and half-open, proved, and opossum's tests pass with the generated module | Done ([#82](https://github.com/sequelcore/accord/issues/82)): machines checked by the solvers and an explorer, and written as TypeScript ([syntax](docs/design/syntax.md#machines), [TypeScript](docs/typescript.md)); Tesota's ProviderRetry model in `conformance/cases/provider-retry.accord`, its two faults refuted and its 148 states matching tla-ts ([measurement](docs/design/measurements/2026-11-12-stage-10-machines/README.md)); opossum's breaker in `conformance/programs/opossum/`, proved, with opossum's lint and tests passing with the generated module (`scripts/check-opossum.sh`) |
+| 11. Structured data | Records, sum types and `match`, recursion with `decreases`, `Text` operations beyond equality | Version comparison from [node-semver](https://github.com/npm/node-semver) (ISC) proved, and node-semver's tests for it pass with the generated module || Next ([#83](https://github.com/sequelcore/accord/issues/83)) |
 | 12. Complete programs | Effects (files, standard input and output, exit codes) declared in types, errors as values, a `main` | `wc` from [uutils/coreutils](https://github.com/uutils/coreutils) (MIT) written only in Accord, its effects in its types and its proofs still fail-closed; uutils' tests for `wc` pass against it | |
 | 13. Standard library and modules | Maps and sets, generic types, imports between packages, as stages 11 and 12's programs need them | Accord's own E2 tooling (`docs/design/e2-human-review/materials.py` and `score.py`) rewritten in Accord; their self-tests and CI check pass | |
 | 14. Native code | A native backend (LLVM), and validation of its output before it relies on a proof | Stage 12's `wc` compiled natively; uutils' tests pass, and a published measurement against uutils' Rust `wc`, with the same algorithm and each side's safety checks stated | |
diff --git a/conformance/programs/opossum/breaker.accord b/conformance/programs/opossum/breaker.accord
index fe32af9..f1d2956 100644
--- a/conformance/programs/opossum/breaker.accord
+++ b/conformance/programs/opossum/breaker.accord
@@ -1,4 +1,7 @@
 // expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, passed
+// SPDX-License-Identifier: Apache-2.0
+// Derived from opossum, by Red Hat, Inc. according to its package.json; its
+// LICENSE names no copyright holder. Licensed under Apache-2.0; see NOTICE.
 // The state and decisions of opossum's CircuitBreaker (opossum 10.0.0, commit
 // decbedf63d7815049233e544dcb351590ff0c84e, lib/circuit.js), ported
 // faithfully as a machine. Emitted events, timers, the cache, the semaphore,
diff --git a/docs/design/measurements/2026-11-12-stage-10-machines/README.md b/docs/design/measurements/2026-11-12-stage-10-machines/README.md
index 32becf0..6ebf378 100644
--- a/docs/design/measurements/2026-11-12-stage-10-machines/README.md
+++ b/docs/design/measurements/2026-11-12-stage-10-machines/README.md
@@ -147,3 +147,28 @@ violation in the correct model.
 - Solver times: each file ran once with a 10-second limit, and none timed
   out.
 - That the stand-in matches opossum on paths its tests don't reach.
+
+## The port against tla-ts, 2026-11-12
+
+Once machines were checked, the ProviderRetry port
+(`conformance/cases/provider-retry.accord`) was compared with Tesota's TLA+
+model run by [tla-ts](https://github.com/aidenybai/tla-ts), a TLC
+replacement in TypeScript, at `8067c48`:
+
+```
+node <tla-ts>/packages/tla-ts/dist/cli.js ProviderRetry.tla -config <cfg>
+```
+
+with the model and its three configurations from Tesota at `4ef9b191`.
+
+| Configuration | tla-ts | Accord's explorer |
+| --- | --- | --- |
+| `ProviderRetry.cfg` | 148 distinct states, no violation | 148 states, all of them; every obligation proved |
+| `ProviderRetry-no-cancel.cfg` | `CancelStopsCalls` violated after Schedule, Advance, Cancel, StartCall | `start_call` refuted after `schedule(1)`, `advance_to_due()`, `cancel()`, `start_call()` |
+| `ProviderRetry-replay-tool.cfg` | `ToolsAndRouteStay` violated after Schedule, Advance, StartCall | `start_call` refuted after `schedule(1)`, `advance_to_due()`, `start_call()` |
+
+The state counts agree, and so do the shortest traces, step for step. The
+port writes `Advance`'s choice of the next time as two events, since the
+choice depends on the state; the states it reaches are the model's. This is
+agreement with a second checker on one model, not a proof that the explorer
+is complete.