diff --git a/tla/consensus/MCabs.cfg b/tla/consensus/MCabs.cfg
index 3a104fd2d151..d81a6ab809ed 100644
--- a/tla/consensus/MCabs.cfg
+++ b/tla/consensus/MCabs.cfg
@@ -14,4 +14,6 @@ INVARIANTS
 
 PROPERTIES 
     AppendOnlyProp
-    
\ No newline at end of file
+
+SYMMETRY 
+    Symmetry
\ No newline at end of file
diff --git a/tla/consensus/MCabs.tla b/tla/consensus/MCabs.tla
index 02abc41ebd58..71fe0967ae23 100644
--- a/tla/consensus/MCabs.tla
+++ b/tla/consensus/MCabs.tla
@@ -1,6 +1,9 @@
 ---- MODULE MCabs ----
 
-EXTENDS abs
+EXTENDS abs, TLC
+
+Symmetry ==
+      Permutations(Servers)
 
 CONSTANTS NodeOne, NodeTwo, NodeThree
 
diff --git a/tla/consensus/abs.tla b/tla/consensus/abs.tla
index b0855392f03d..b1b88e29b4b4 100644
--- a/tla/consensus/abs.tla
+++ b/tla/consensus/abs.tla
@@ -2,24 +2,30 @@
 \* Abstract specification for a distributed consensus algorithm.
 \* Assumes that any node can atomically inspect the state of all other nodes. 
 
-EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, FiniteSetsExt
+EXTENDS Sequences, SequencesExt, Naturals, FiniteSets, FiniteSetsExt, Relation
 
-CONSTANT Servers, Terms, MaxLogLength
+CONSTANT Servers
+ASSUME IsFiniteSet(Servers)
+
+\* Terms is (strictly) totally ordered with a smallest element.
+CONSTANT Terms
+ASSUME /\ IsStrictlyTotallyOrderedUnder(<, Terms) 
+       /\ \E min \in Terms : \A t \in Terms : t <= min
+
+CONSTANT MaxLogLength
+ASSUME MaxLogLength \in Nat
 
 \* Commit logs from each node
 \* Each log is append-only and the logs will never diverge.
 VARIABLE cLogs
 
 TypeOK ==
-    /\ cLogs \in [Servers -> 
-        UNION {[1..l -> Terms] : l \in 0..MaxLogLength}]
+    cLogs \in [Servers -> Seq(Terms)]
 
 StartTerm == Min(Terms)
 
-InitialLogs == {
-    <<>>,
-    <<StartTerm, StartTerm>>,
-    <<StartTerm, StartTerm, StartTerm, StartTerm>>}
+InitialLogs == 
+    UNION {[ 1..n -> {StartTerm} ] : n \in {0,2,4}}
     
 Init ==
     cLogs \in [Servers -> InitialLogs]