diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh
index e8f7753e8..b1de4db9b 100755
--- a/examples/.scripts/run-example.sh
+++ b/examples/.scripts/run-example.sh
@@ -136,6 +136,8 @@ get_verify_args () {
     args="--init=Init --step=Next"
   elif [[ "$file" == "games/tictactoe/tictactoe.qnt" ]] ; then
     args="--max-steps=1" # pretty slow, and we just want to check that verification can run
+  elif [[ "$file" == "classic/distributed/TeachingConcurrency/teachingConcurrency.qnt" ]] ; then
+    args="--temporal correct"
   fi
   echo "${args}"
 }
diff --git a/examples/README.md b/examples/README.md
index 183b6df69..97f3e36d7 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -54,6 +54,7 @@ listed without any additional command line arguments.
 | [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> |
 | [classic/distributed/Paxos/Voting.qnt](./classic/distributed/Paxos/Voting.qnt) | :white_check_mark: | :white_check_mark: | N/A[^parameterized] | N/A[^nostatemachine] |
 | [classic/distributed/ReadersWriters/ReadersWriters.qnt](./classic/distributed/ReadersWriters/ReadersWriters.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
+| [classic/distributed/TeachingConcurrency/teachingConcurrency.qnt](./classic/distributed/TeachingConcurrency/teachingConcurrency.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt](./classic/distributed/TwoPhaseCommit/two_phase_commit_modules.qnt) | :white_check_mark: | :white_check_mark: | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> | :x:<sup>https://github.com/informalsystems/quint/issues/1299</sup> |
 | [classic/sequential/BinSearch/BinSearch.qnt](./classic/sequential/BinSearch/BinSearch.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
diff --git a/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt b/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt
new file mode 100644
index 000000000..6de668fcd
--- /dev/null
+++ b/examples/classic/distributed/TeachingConcurrency/teachingConcurrency.qnt
@@ -0,0 +1,98 @@
+// -*- mode: Bluespec; -*-
+/**
+ * A simple algorithm from Lamport's "Teaching Concurrency" paper:
+ * https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf
+ *
+ * Run in verifier with:
+ * quint verify --temporal correct teachingConcurrency.qnt
+ */
+
+// An example instance of the algorithm with N=5.
+module teachingConcurrency {
+    import teachingConcurrencyN(NUM_PROCS=5).*
+}
+
+// A concurrency algorithm providing a basic form of mutual
+// exclusion. For details and proofs see section 7.2 of
+// https://lamport.azurewebsites.net/tla/proving-safety.pdf
+module teachingConcurrencyN {
+    // N processes (numbered from 0 to N-1).
+    const NUM_PROCS: int
+    assume nonEmpty = NUM_PROCS >= 1
+
+    var x: List[int]
+    var y: List[int]
+
+    // Set of processes yet to be executed.
+    var pendingProcs: Set[int]
+
+    // Initial state:
+    //  - x and y zeroed for all processes
+    //  - all processes pending scheduling
+    action init = all {
+        x' = zeroes(NUM_PROCS),
+        y' = zeroes(NUM_PROCS),
+        pendingProcs' = 0.to(NUM_PROCS-1),
+    }
+
+    // Stepping action: randomly pick a pending process (if
+    // any) and execute it. Otherwise stutter forever, as
+    // every process has stopped.
+    action step = {
+        if (termination) {
+            allStopped
+        } else {    
+            processUpdate
+        }
+    }
+
+    // Execute the algorithm for a pending process.
+    action processUpdate = {
+        nondet proc = pendingProcs.oneOf()
+
+        val nextX = x.replaceAt(proc, 1)
+        val index = circularIndex(proc, NUM_PROCS)
+        val yValue = nextX[index]
+
+        all {
+            x' = nextX,
+            y' = y.replaceAt(proc, yValue),
+            pendingProcs' = pendingProcs.exclude(Set(proc)),
+        }
+    }
+
+    // All processes have stopped.
+    action allStopped = all {
+        x' = x,
+        y' = y,
+        pendingProcs' = pendingProcs,
+    }
+
+    // Return a List of 0s, with the given length.
+    pure def zeroes(len: int): List[int] = {
+        0.to(len-1).fold(List(), (l, _) => l.append(0))
+    }
+
+    // Calculate the circular index `(i-1) mod N`.
+    pure def circularIndex(i: int, N: int): int = {
+        if (i == 0) {
+            N-1
+        } else {
+            i-1
+        }
+    }
+
+    // Correctness invariant: (after every process has
+    // stopped) y[i] == 1 for at least one process.
+    val yContainsOne = {
+        y.select(v => v == 1).length() >= 1
+    }
+
+    // Termination invariant: all processes have stopped
+    // (i.e. none is pending scheduling).
+    val termination = {
+        pendingProcs.size() == 0
+    }
+
+    temporal correct = eventually(termination and yContainsOne)
+}