diff --git a/examples/README.md b/examples/README.md
index 7835502ad..0e8c954b0 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -49,6 +49,9 @@ listed without any additional command line arguments.
 | Example | Syntax (`parse`) | Types (`typecheck`) | Unit tests (`test`) | Apalache (`verify`) |
 |---------|:----------------:|:-------------------:|:-------------------:|:-------------------:|
 | [classic/distributed/ClockSync/clockSync3.qnt](./classic/distributed/ClockSync/clockSync3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/ewd426/ewd426.qnt](./classic/distributed/ewd426/ewd426.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/ewd426/ewd426_3.qnt](./classic/distributed/ewd426/ewd426_3.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/ewd426/ewd426_4.qnt](./classic/distributed/ewd426/ewd426_4.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/ewd840/ewd840.qnt](./classic/distributed/ewd840/ewd840.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/LamportMutex/LamportMutex.qnt](./classic/distributed/LamportMutex/LamportMutex.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/Paxos/Paxos.qnt](./classic/distributed/Paxos/Paxos.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1284</sup> |
diff --git a/examples/classic/distributed/ewd426/README.md b/examples/classic/distributed/ewd426/README.md
new file mode 100644
index 000000000..1fec43c4e
--- /dev/null
+++ b/examples/classic/distributed/ewd426/README.md
@@ -0,0 +1,30 @@
+# EWD426
+
+This folder contains Quint specifications for the three different self-stabilization algorithms proposed by Dijkstra in [EWD426](https://www.cs.utexas.edu/~EWD/transcriptions/EWD04xx/EWD426.html).
+1. A solution with K-state machines [ewd426.qnt](ewd426.qnt)
+2. A solution with three-state machines [ewd426_3.qnt](ewd426_3.qnt)
+3. A solution with four-state machines [ewd426_4.qnt](ewd426_4.qnt)
+
+Due to the presence of temporal properties and fairness, we need to use TLC to model check these specs. As the integration with TLC is not completed, we provide a script to automate running it for these specific specifications: [check_with_tlc.sh](check_with_tlc.sh).
+
+If you are trying to learn/understand these algorithms, we recommend playing with the Quint REPL. For that, pick one of the files (for example [ewd426.qnt](ewd426.qnt)) and run the following command in the terminal:
+``` sh
+quint -r ewd426.qnt::ewd426
+```
+
+This will open the REPL with the `ewd426` machine loaded. You can now interact with the machine and explore its states and transitions:
+
+``` bluespec
+Quint REPL 0.22.4
+Type ".exit" to exit, or ".help" for more information
+>>> init
+true
+>>> step
+true
+>>> show_token(system)
+Map(0 -> false, 1 -> true, 2 -> true, 3 -> false, 4 -> true, 5 -> false)
+>>> 5.reps(_ => step)
+true
+>>> show_token(system)
+Map(0 -> true, 1 -> false, 2 -> false, 3 -> false, 4 -> false, 5 -> false)
+```
diff --git a/examples/classic/distributed/ewd426/check_with_tlc.sh b/examples/classic/distributed/ewd426/check_with_tlc.sh
new file mode 100644
index 000000000..0314a81a2
--- /dev/null
+++ b/examples/classic/distributed/ewd426/check_with_tlc.sh
@@ -0,0 +1,67 @@
+#!/bin/bash
+
+# Files to process
+FILES=("ewd426.qnt" "ewd426_3.qnt" "ewd426_4.qnt")
+
+# Apalache jar path
+APALACHE_JAR="$HOME/.quint/apalache-dist-0.47.2/apalache/lib/apalache.jar"
+
+# Memory options for Java
+JAVA_OPTS="-Xmx8G -Xss515m"
+
+for file in "${FILES[@]}"; do
+    base_name="${file%.qnt}"
+    tla_file="${base_name}.tla"
+    cfg_file="${base_name}.cfg"
+
+    echo "Processing $file..."
+
+    # Step 1: Compile the .qnt file to .tla
+    quint compile --target=tlaplus "$file" --temporal=convergence,closure,persistence --invariant=tokenInv > "$tla_file"
+
+    if [[ $? -ne 0 ]]; then
+        echo "Error: Compilation failed for $file"
+        exit 1
+    fi
+
+    # Step 2: Fix init to be a predicate instead of an assignment
+    perl -0777 -i -pe "s/(.*)'\s+:= (.*_self_stabilization_.*?initial)/\1 = \2/s" "$tla_file"
+
+
+    if [[ $? -ne 0 ]]; then
+        echo "Error: Failed to edit $tla_file"
+        exit 1
+    fi
+
+    # Step 3: Create the .cfg file
+    cat <<EOF > "$cfg_file"
+INIT
+q_init
+
+NEXT
+q_step
+
+PROPERTY
+q_temporalProps
+
+INVARIANT
+q_inv
+EOF
+
+    # Step 4: Run TLC with the required Apalache lib files and check output
+    output=$(java $JAVA_OPTS -cp "$APALACHE_JAR" tlc2.TLC -deadlock "$tla_file" 2>&1)
+
+    # Step 5: Delete the generated .tla and .cfg files
+    rm -f "$tla_file" "$cfg_file"
+
+    if echo "$output" | grep -q "Model checking completed. No error has been found."; then
+        echo "Model checking succeeded for $tla_file"
+    else
+        echo "Error: Model checking failed for $tla_file"
+        echo "$output"
+        exit 1
+    fi
+
+done
+
+echo "All files processed successfully."
diff --git a/examples/classic/distributed/ewd426/ewd426.qnt b/examples/classic/distributed/ewd426/ewd426.qnt
new file mode 100644
index 000000000..9607c645d
--- /dev/null
+++ b/examples/classic/distributed/ewd426/ewd426.qnt
@@ -0,0 +1,85 @@
+// -*- mode: Bluespec; -*-
+/**
+ * ewd426's Stabilizing Token Ring (EWD426)
+ * K state machine
+ * This implementation ensures that from some time on,
+ * exactly one token circulates in a set of nodes,
+ *
+ * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025
+ */
+module self_stabilization {
+  // Number of nodes in the ring
+  const N: int
+  const K: int
+
+  /// Ensures the state space is larger than the number of nodes
+  assume _ = K >= N
+
+  val bottom = 0
+  val top = N
+
+  /// Mapping of node indices to their states
+  var system: int -> int
+
+  /// Check if a node has the token
+  pure def has_token(nodes: int -> int, index: int): bool =
+    if (index == bottom)
+      nodes.get(bottom) == nodes.get(top)
+    else
+      not(nodes.get(index) == nodes.get(index - 1))
+
+  /// Update the state of a specific node
+  pure def state_transition(nodes: int -> int, index: int): int =
+    if (not(has_token(nodes, index)))
+      nodes.get(index)
+    else if (index == bottom)
+      (nodes.get(bottom) + 1) % K
+    else
+      nodes.get(index - 1)
+
+  /// Initialize all nodes with non-deterministic states
+  action init = all {
+    nondet initial = 0.to(N).setOfMaps(0.to(K - 1)).oneOf()
+    system' = initial
+  }
+
+  /// Pick a single active node non-deterministically and update its state
+  action step = {
+    nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf()
+    system' = system.set(node, state_transition(system, node))
+  }
+
+  /// Pick several active nodes non-deterministically and update their state.
+  /// Closer to the distributed demon is discussed in EWD 391. We are not
+  /// considering interleaving in the execution of state_transition here
+  action distributed_step = {
+    nondet nodes = 0.to(N).filter(i => has_token(system, i)).powerset().exclude(Set()).oneOf()
+    system' = nodes.fold(system, (s, x) => s.set(x, state_transition(system, x)))
+  }
+
+  // Pure function to count how many tokens exist
+  pure def count_tokens(nodes: int -> int): int = {
+    0.to(N).filter(i => has_token(nodes, i)).size()
+  }
+
+  // Temporal properties
+  temporal convergence = step.weakFair(Set(system)) implies eventually(count_tokens(system) == 1)
+  temporal closure = always(count_tokens(system) == 1 implies always(count_tokens(system) == 1))
+  temporal persistence = step.weakFair(Set(system)) implies eventually(always(count_tokens(system) == 1))
+
+  // Invariant
+  def tokenInv = count_tokens(system) > 0
+
+  /// to better see the token in the repl
+  pure def show_token(nodes: int -> int): int -> bool =
+    nodes.keys().mapBy(i => has_token(nodes, i))
+}
+
+module ewd426 {
+  import self_stabilization(N = 5, K = 7).*
+}
+
+module broken_ewd426 {
+  // This should break the assumption of K >= N. See #1182.
+  import self_stabilization(N = 3, K = 2).*
+}
diff --git a/examples/classic/distributed/ewd426/ewd426_3.qnt b/examples/classic/distributed/ewd426/ewd426_3.qnt
new file mode 100644
index 000000000..a4d3b9fc9
--- /dev/null
+++ b/examples/classic/distributed/ewd426/ewd426_3.qnt
@@ -0,0 +1,102 @@
+// -*- mode: Bluespec; -*-
+/**
+ * ewd426's Stabilizing Token Ring (EWD426)
+ * 3 state machine
+ * This implementation ensures that from some time on,
+ * exactly one token circulates in a set of nodes.
+ *
+ * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025
+ */
+module self_stabilization_three_state {
+  // Number of nodes in the ring
+  const N: int
+
+  val bottom = 0
+  val top = N
+
+  // Variable: Mapping of node indices to their states
+  var system: int -> int
+
+  pure def has_token(nodes: int -> int, index: int): bool =
+    val s = nodes.get(index)
+    if (index == bottom)
+      val r = nodes.get(1)
+      (s + 1) % 3 == r
+    else if (index == top)
+      val l = nodes.get(N - 1)
+      val r = nodes.get(bottom)
+      l == r and not((l + 1) % 3 == s)
+    else
+      val l = nodes.get(index - 1)
+      val r = nodes.get(index + 1)
+      or {
+        (s + 1) % 3 == l,
+        (s + 1) % 3 == r
+      }
+
+  // Transition function for the three-state machine
+  pure def state_transition(nodes: int -> int, index: int): int =
+    val s = nodes.get(index)
+    if (not(has_token(nodes, index)))
+      s
+    else if (index == bottom)
+      (s + 2) % 3 // (s - 1) % 3
+    else if (index == top)
+      val l = nodes.get(N - 1)
+      (l + 1) % 3
+    else
+      val l = nodes.get(index - 1)
+      val r = nodes.get(index + 1)
+      if ((s + 1) % 3 == l)
+        // Not 100% sure what ewd426 wants here. Might be non-determinism
+        // between the two options. We make it deterministic here.
+        if ((s + 1) % 3 == r)
+          r
+        else
+          l
+      else if ((s + 1) % 3 == r)
+        r
+      else
+        s
+
+  /// Initialize all nodes with random states
+  action init = all {
+    nondet initial = 0.to(N).setOfMaps(0.to(2)).oneOf()
+    system' = initial
+  }
+
+  /// Pick a single active node non-deterministically and update its state
+  action step = {
+    nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf()
+    system' = system.set(node, state_transition(system, node))
+  }
+
+  /// Pick several active nodes non-deterministically and update their state.
+  /// Closer to the distributed demon is discussed in EWD 391. We are not
+  /// considering interleaving in the execution of state_transition here
+  action distributed_step = {
+    nondet nodes = 0.to(N).filter(i => has_token(system, i)).powerset().exclude(Set()).oneOf()
+    system' = nodes.fold(system, (s, x) => s.set(x, state_transition(system, x)))
+  }
+
+  // Pure function to count how many tokens exist
+  pure def count_tokens(nodes: int -> int): int = {
+    to(0, N).filter(i => has_token(nodes, i)).size()
+  }
+
+  // Temporal properties
+  temporal convergence = step.weakFair(Set(system)) implies eventually(count_tokens(system) == 1)
+  temporal closure = always(count_tokens(system) == 1 implies always(count_tokens(system) == 1))
+  temporal persistence = step.weakFair(Set(system)) implies eventually(always(count_tokens(system) == 1))
+
+  // Invariant
+  def tokenInv = count_tokens(system) > 0
+
+  /// to better see the token in the repl
+  pure def show_token(nodes: int -> int): int -> bool =
+    nodes.keys().mapBy(i => has_token(nodes, i))
+}
+
+module ewd426_3 {
+  import self_stabilization_three_state(N = 5).*
+}
diff --git a/examples/classic/distributed/ewd426/ewd426_4.qnt b/examples/classic/distributed/ewd426/ewd426_4.qnt
new file mode 100644
index 000000000..962bfabd6
--- /dev/null
+++ b/examples/classic/distributed/ewd426/ewd426_4.qnt
@@ -0,0 +1,109 @@
+// -*- mode: Bluespec; -*-
+/**
+ * ewd426's Stabilizing Token Ring (EWD426)
+ * 4 state machine
+ * This implementation ensures that from some time on,
+ * exactly one token circulates in a set of nodes,
+ *
+ * Mahtab Norouzi, Josef Widder, Informal Systems, 2024-2025
+ */
+module self_stabilization_four_state {
+  const N: int
+
+  val bottom = 0
+  val top = N
+
+  type State = {
+    x: bool,
+    up: bool
+  }
+
+  var system: int -> State
+
+  pure def has_token(nodes: int -> State, index: int): bool =
+    val s = nodes.get(index)
+    if (index == bottom)
+      val r = nodes.get(1)
+      s.x == r.x and not(r.up)
+    else if (index == top)
+      val l = nodes.get(N - 1)
+      not(s.x == l.x)
+    else
+      val l = nodes.get(index - 1)
+      val r = nodes.get(index + 1)
+      or {
+        not(s.x == l.x),
+        and {
+          s.x == r.x,
+          s.up,
+          not(r.up)
+        }
+      }
+
+  // Pure function to handle the four-state transition
+  pure def state_transition(nodes: int -> State, index: int): State =
+    val s = nodes.get(index)
+    if (not(has_token(nodes, index)))
+      s
+    else if (index == bottom)
+      { x: not(s.x), up: s.up }
+    else if (index == top)
+      { x: not(s.x), up: s.up }
+    else
+      val l = nodes.get(index - 1)
+      val r = nodes.get(index + 1)
+      if (not(s.x == l.x))
+        { x: not(s.x), up: true }
+      else
+        // and {s.x == r.x, s.up, not(r.up)}
+        { x: s.x, up: false }
+
+  action init = all {
+    val allState = Set(
+      { x: false, up: false },
+      { x: false, up: true },
+      { x: true, up: false },
+      { x: true, up: true }
+    )
+    nondet initial = 0.to(N).setOfMaps(allState).oneOf()
+    // "For the bottom machine upS = true by definition, for the top machine upS = false by definition"
+    system' = initial
+      .setBy(bottom, s => { ...s, up: true })
+      .setBy(top, s => { ...s, up: false })
+  }
+
+  /// Pick a single active node non-deterministically and update its state
+  action step = {
+    nondet node = 0.to(N).filter(i => has_token(system, i)).oneOf()
+    system' = system.set(node, state_transition(system, node))
+  }
+
+  /// Pick several active nodes non-deterministically and update their state.
+  /// Closer to the distributed demon is discussed in EWD 391. We are not
+  /// considering interleaving in the execution of state_transition here
+  action distributed_step = {
+    nondet nodes = 0.to(N).filter(i => has_token(system, i)).powerset().exclude(Set()).oneOf()
+    system' = nodes.fold(system, (s, x) => s.set(x, state_transition(system, x)))
+  }
+
+  // Pure function to count how many tokens exist
+  pure def count_tokens(nodes: int -> State): int = {
+    0.to(N).filter(i => has_token(nodes, i)).size()
+  }
+
+  // Temporal properties
+  temporal convergence = step.weakFair(Set(system)) implies eventually(count_tokens(system) == 1)
+  temporal closure = always(count_tokens(system) == 1 implies always(count_tokens(system) == 1))
+  temporal persistence = step.weakFair(Set(system)) implies eventually(always(count_tokens(system) == 1))
+
+  // Invariant
+  def tokenInv = count_tokens(system) > 0
+
+  /// to better see the token in the repl
+  pure def show_token(nodes: int -> State): int -> bool =
+    nodes.keys().mapBy(i => has_token(nodes, i))
+}
+
+module ewd426_4 {
+  import self_stabilization_four_state(N = 5).*
+}