diff --git a/tlatools/src/tlc2/TLCGlobals.java b/tlatools/src/tlc2/TLCGlobals.java
index d199f3fac3116d8a3fc35ac3a9a2e9a17a96c272..e6aee0b5c60b17f2d671a4038194dada25ccfe68 100644
--- a/tlatools/src/tlc2/TLCGlobals.java
+++ b/tlatools/src/tlc2/TLCGlobals.java
@@ -52,7 +52,11 @@ public class TLCGlobals
 	public static String lnCheck = "default";
 	
 	public static boolean doLiveness() {
-		return !lnCheck.equals("final");
+		return !(lnCheck.equals("final") || lnCheck.equals("seqfinal"));
+	}
+
+	public static boolean doSequentialLiveness() {
+		return lnCheck.startsWith("seq");
 	}
 
 	public synchronized static void setNumWorkers(int n)
diff --git a/tlatools/src/tlc2/tool/liveness/LiveCheck.java b/tlatools/src/tlc2/tool/liveness/LiveCheck.java
index 5d15cebc3f07f3928132ef3716df61afe0379a5b..f253e135f1c81f10e042d0f2165b50f1341b843a 100644
--- a/tlatools/src/tlc2/tool/liveness/LiveCheck.java
+++ b/tlatools/src/tlc2/tool/liveness/LiveCheck.java
@@ -227,7 +227,7 @@ public class LiveCheck implements ILiveCheck {
 		 * a violation found by another LW. However, if any LW fails to check, we terminate
 		 * model checking after all LWs completed.
 		 */
-		final int wNum = Math.min(checker.length, TLCGlobals.getNumWorkers());
+		final int wNum = TLCGlobals.doSequentialLiveness() ? 1 : Math.min(checker.length, TLCGlobals.getNumWorkers());
 		final ExecutorService pool = Executors.newFixedThreadPool(wNum);
 		// CS is really just a container around the set of Futures returned by the pool. It saves us from
 		// creating a low-level array.