diff --git a/Specs/Quint/asyncModelsTest.qnt b/Specs/Quint/asyncModelsTest.qnt
deleted file mode 100644
index d2f06ad27..000000000
--- a/Specs/Quint/asyncModelsTest.qnt
+++ /dev/null
@@ -1,264 +0,0 @@
-// -*- mode: Bluespec; -*-
-
-module asyncModelsTest {
-
-import statemachineAsync(
-    validators = Set("v1", "v2", "v3", "v4"),
-    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
-    Faulty = Set(),
-    Values = Set("a", "b"),
-    Rounds = Set(0, 1, 2, 3),
-    Heights = Set(0) // , 1, 2, 3)
-) as N4F0 from "./statemachineAsync"
-
-
-run ThreeDecideInRound1V4stillinZeroOld = {
-    N4F0::init
-    .then(N4F0::setNextValueToPropose("v2", "block"))
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3"))
-    .then(N4F0::valStep("v4"))
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::deliverProposal("v2", { height: 0, proposal: "block", round: 0, src: "v2", validRound: -1 }))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    // Timeoutpropose fired on 1, 3, proposer 2 received proposal
-    // they all moved to prevote (with step change we need extra step)
-    // now deliver to 1, 2, 3: nil from 1 and 3, value from proposer 
-    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" }))
-    .then(N4F0::deliverVote("v1", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" }))
-    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v1", step: "Prevote" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "block", round: 0, src: "v2", step: "Prevote" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v3", step: "Prevote" }))   
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    // timeoutPrevote started
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    // 1, 2, 3 receive precommit nil from 1, 2, 3
-    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" }))
-    .then(N4F0::deliverVote("v1", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v2", step: "Precommit" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "nil", round: 0, src: "v3", step: "Precommit" }))
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3"))   
-    // timeoutprecommit started
-    .then(N4F0::setNextValueToPropose("v3", "another block")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3"))     
-    .then(N4F0::deliverProposal("v1",  { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
-    .then(N4F0::deliverProposal("v2",  { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
-    .then(N4F0::deliverProposal("v3",  { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    // ^ everyone receives proosal
-    // v from prevote to precommit
-    .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v1", step: "Prevote" }))
-    .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
-    .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v3", step: "Prevote" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v1", step: "Prevote" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v3", step: "Prevote" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v1", step: "Prevote" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v3", step: "Prevote" }))
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3"))
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3"))    
-    // v 1, 2, 3 receives precommit
-    .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
-    .then(N4F0::deliverVote("v1", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
-    .then(N4F0::deliverVote("v2", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
-    .then(N4F0::deliverVote("v3", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))     
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3")) 
-    .then(N4F0::valStep("v1"))
-    .then(N4F0::valStep("v2"))
-    .then(N4F0::valStep("v3"))
-    .then(all {
-        assert(N4F0::system.get("v3").es.chain.head() == "another block"),
-        N4F0::unchangedAll
-    })       
-}
-
-run DecideForFutureRoundOld = {
-    ThreeDecideInRound1V4stillinZeroOld
-    .then(N4F0::deliverProposal("v4",  { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" }))
-//    .then(4.reps(i => N4F0::valStep("v4")))
-    .then(N4F0::valStep("v4"))
-    .then(N4F0::valStep("v4"))
-    .then(N4F0::valStep("v4"))
-    .then(N4F0::valStep("v4"))
-    .then(all {
-        assert(N4F0::system.get("v4").es.chain.head() == "another block"),
-        N4F0::unchangedAll
-    })
-   // .then(N4F0::valStep("v4"))
-           
-}
-
-run DecideOnProposalOld = {
-    ThreeDecideInRound1V4stillinZeroOld
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v2", step: "Precommit" }))
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v3", step: "Precommit" })) 
-    .then(N4F0::valStep("v4"))
-    .then(N4F0::valStep("v4"))
-    .then(N4F0::valStep("v4"))
-    .then(N4F0::deliverProposal("v4",  { height: 0, proposal: "another block", round: 1, src: "v3", validRound: -1 }))
-    .then(all {
-        assert(N4F0::system.get("v4").es.chain == List()),
-        N4F0::valStep("v4")
-    })
-    .then(all {
-        assert(N4F0::system.get("v4").es.chain.head() == "another block"),
-        N4F0::unchangedAll
-    })   
-}    
-
-run RoundswitchOld = {
-    ThreeDecideInRound1V4stillinZeroOld
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v1", step: "Precommit" }))
-    .then(N4F0::deliverVote("v4", { height: 0, id: "another block", round: 1, src: "v2", step: "Prevote" }))
-    .then(N4F0::valStep("v4"))
-    .then(all {
-        assert(N4F0::system.get("v4").es.cs.round == 0),
-        N4F0::valStep("v4")})
-    .then(all {
-        assert(N4F0::system.get("v4").es.cs.round == 1),
-        N4F0::unchangedAll
-    })   
-}   
-
-
-
-import statemachineAsync(
-    validators = Set("v1", "v2", "v3", "v4"),
-    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
-    Faulty = Set("v1"),
-    Values = Set("a", "b"),
-    Rounds = Set(0, 1, 2, 3),
-    Heights = Set(0) // , 1, 2, 3)
-) as N4F1 from "./statemachineAsync"
-
-// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::AgreementInv AsyncModels.qnt
-// quint run --init=N4F1::init --step=N4F1::step --invariant=N4F1::ConsensusOutputInv AsyncModels.qnt
-
-import statemachineAsync(
-    validators = Set("v1", "v2", "v3", "v4"),
-    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
-    Faulty = Set("v1", "v2"),
-    Values = Set("a", "b"),
-    Rounds = Set(0),  // , 1, 2, 3)
-    Heights = Set(0) // , 1, 2, 3)
-) as N4F2 from "./statemachineAsync"
-
-// v3 and v4 are correct. v2 is a faulty proposal and proposes differently to v3 and v4
-// this run leads to disagreement
-run DisagreementOld = {
-    N4F2::init
-    .then(N4F2::valStep("v3"))
-    .then(N4F2::valStep("v4"))
-    .then(N4F2::deliverProposal("v3", { height: 0, proposal: "b", round: 0, src: "v2", validRound: -1 }))
-    .then(N4F2::deliverProposal("v4", { height: 0, proposal: "a", round: 0, src: "v2", validRound: -1 }))
-    .then(N4F2::valStep("v3"))
-    .then(N4F2::valStep("v4"))
-    .then(all{
-        // they voted differently
-        assert(N4F2::voteBuffer == Map(
-            "v3" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" },  
-                        { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }),
-            "v4" -> Set({ height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }, 
-                        { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }))),
-            N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Prevote" })
-    })
-    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Prevote" }))
-    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Prevote" }))
-    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Prevote" }))
-    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Prevote" }))
-    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Prevote" }))
-    .then(N4F2::valStep("v3"))  
-    .then(N4F2::valStep("v3"))   
-    .then(N4F2::valStep("v3"))
-    .then(N4F2::valStep("v3"))
-    .then(N4F2::valStep("v4"))
-    .then(N4F2::valStep("v4"))
-    .then(N4F2::valStep("v4"))
-    .then(N4F2::valStep("v4"))
-    .then(all{
-        // they precommited diN4F2N4F2erently
-        assert( N4F2::voteBuffer.get("v3").contains({ height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) and
-                N4F2::voteBuffer.get("v4").contains({ height: 0, id: "b", round: 0, src: "v3", step: "Precommit" })), 
-        N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v1", step: "Precommit" }) })
-    .then(N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v2", step: "Precommit" }))    
-    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v1", step: "Precommit" })) 
-    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v2", step: "Precommit" })) 
-    .then(N4F2::valStep("v3"))  
-    .then(N4F2::valStep("v3"))   
-    .then(N4F2::valStep("v4"))
-    .then(N4F2::valStep("v4"))
-    .then(all{
-        assert(N4F2::AgreementInv),
-        N4F2::deliverVote("v4", { height: 0, id: "a", round: 0, src: "v4", step: "Precommit" }) })
-    .then(N4F2::deliverVote("v3", { height: 0, id: "b", round: 0, src: "v3", step: "Precommit" }))
-    .then(N4F2::valStep("v3"))   
-    .then(N4F2::valStep("v4"))
-    .then(all{
-        assert(not(N4F2::AgreementInv)),
-        N4F2::unchangedAll})   
-}
-
-
-
-}
diff --git a/Specs/Quint/disagreementRun.qnt b/Specs/Quint/disagreementRun.qnt
new file mode 100644
index 000000000..7748a796f
--- /dev/null
+++ b/Specs/Quint/disagreementRun.qnt
@@ -0,0 +1,45 @@
+// -*- mode: Bluespec; -*-
+
+module disagreementRun {
+
+import TendermintDSL.* from "./TendermintDSL"
+export TendermintDSL.*
+
+const groupA : Set[Address_t]
+val groupB = Correct.exclude(groupA)
+val aList = groupA.fold(List(), (s, x) => s.append(x)) 
+val bList = groupB.fold(List(), (s, x) => s.append(x)) 
+
+// A run for too many faulty nodes
+
+// TODO: assertions about proposer being faulty
+run DisagreementRun = {
+    val thisProposer = Proposer (validatorSet, 0, 0)
+    init
+    .then(2.reps(_ => ListTakeAStep(correctList)))
+    .then(ListDeliverProposal(aList, { height: 0, proposal: "a", round: 0, src: thisProposer, validRound: -1 }))
+    .then(ListDeliverProposal(bList, { height: 0, proposal: "b", round: 0, src: thisProposer, validRound: -1 }))
+    .then(ListTakeAStep(correctList))
+    // they voted differently
+    .then(ListTakeAStep(correctList)) // consume step change
+    .then(ListDeliverAllVotes("Prevote", aList.concat(faultyList), aList, validatorSet, 0, 0, "a"))
+    .then(ListDeliverAllVotes("Prevote", bList.concat(faultyList), bList, validatorSet, 0, 0, "b"))  
+    .then(aList.concat(faultyList).length().reps(_ => ListTakeAStep(aList)))
+    .then(bList.concat(faultyList).length().reps(_ => ListTakeAStep(bList)))
+    .then(ListTakeAStep(correctList)) // timeout prevote started -> extra step to consume pending
+    // they precommited differently
+    .then(ListTakeAStep(correctList)) // consume step change
+    .then(ListDeliverAllVotes("Precommit", aList.concat(faultyList), aList, validatorSet, 0, 0, "a"))
+    .then(ListDeliverAllVotes("Precommit", bList.concat(faultyList), bList, validatorSet, 0, 0, "b"))  
+    .then(aList.concat(faultyList).length().reps(_ => ListTakeAStep(aList)))
+    .then(bList.concat(faultyList).length().reps(_ => ListTakeAStep(bList)))
+    .then(all{
+        assert(not(AgreementInv)),
+        unchangedAll
+    })   
+}
+
+}
+
+
+}
\ No newline at end of file
diff --git a/Specs/Quint/disagreementTest.qnt b/Specs/Quint/disagreementTest.qnt
new file mode 100644
index 000000000..08a0a5a05
--- /dev/null
+++ b/Specs/Quint/disagreementTest.qnt
@@ -0,0 +1,20 @@
+// -*- mode: Bluespec; -*-
+
+module disagreementTest {
+
+import disagreementRun(
+    validators = Set("v1", "v2", "v3", "v4"),
+    validatorSet = Set("v1", "v2", "v3", "v4").mapBy(x => 1),
+    Faulty = Set("v1", "v2"),
+    Values = Set("a", "b"),
+    Rounds = Set(0),  // , 1, 2, 3)
+    Heights = Set(0), // , 1, 2, 3)
+    groupA = Set("v3")
+) as N4F2 from "./disagreementRun"
+
+run disagreementTest = {
+    N4F2::DisagreementRun    
+}
+
+
+}
\ No newline at end of file
diff --git a/Specs/Quint/someMultiRoundRuns.qnt b/Specs/Quint/someMultiRoundRuns.qnt
index cedfddadf..2c1056e1e 100644
--- a/Specs/Quint/someMultiRoundRuns.qnt
+++ b/Specs/Quint/someMultiRoundRuns.qnt
@@ -102,4 +102,6 @@ run RoundswitchRun = {
 }   
 
 
+
+
 }
\ No newline at end of file
diff --git a/Specs/Quint/someMultiRoundTest.qnt b/Specs/Quint/someMultiRoundTest.qnt
index d4f790cf2..b0462a907 100644
--- a/Specs/Quint/someMultiRoundTest.qnt
+++ b/Specs/Quint/someMultiRoundTest.qnt
@@ -28,4 +28,6 @@ run RoundswitchTest = {
     N4F0::RoundswitchRun
 }
 
+
+
 }
\ No newline at end of file