diff --git a/.github/workflows/spec.yaml b/.github/workflows/spec.yaml
index 6c1971fb..68e66509 100644
--- a/.github/workflows/spec.yaml
+++ b/.github/workflows/spec.yaml
@@ -20,7 +20,7 @@ jobs:
           check-latest: true
 
       - name: Install quint
-        run: npm i @informalsystems/quint@0.21.0 -g
+        run: npm i @informalsystems/quint@0.22.4 -g
 
       - name: Run test
         run: cd spec && make test
diff --git a/spec/informal-spec/replica.rs b/spec/informal-spec/replica.rs
index 647794de..0727bbb8 100644
--- a/spec/informal-spec/replica.rs
+++ b/spec/informal-spec/replica.rs
@@ -250,7 +250,7 @@ impl ReplicaState {
         self.phase = Phase::Prepare;
         
         // Send a new view message to the other replicas, for synchronization.
-        let new_view = NewView::new(self.get_justification(view));
+        let new_view = NewView::new(self.create_justification());
         
         self.send(new_view);
     }
@@ -265,4 +265,4 @@ impl ReplicaState {
             Justification::Timeout(self.high_timeout_qc.unwrap())
         }
     }
-}
\ No newline at end of file
+}
diff --git a/spec/informal-spec/types.rs b/spec/informal-spec/types.rs
index d8074005..400bce84 100644
--- a/spec/informal-spec/types.rs
+++ b/spec/informal-spec/types.rs
@@ -72,7 +72,7 @@ impl Justification {
         match self {
             Commit(qc) => {
                 // The previous proposal was finalized, so we can propose a new block.
-                (qc.block_number + 1, None)
+                (qc.vote.block_number + 1, None)
             }
             Timeout(qc) => {
                 // Get the high vote of the timeout QC, if it exists. We check if there are
@@ -88,7 +88,7 @@ impl Justification {
                 let high_qc: Option<CommitQC> = qc.high_commit_qc;
 
                 if high_vote.is_some()
-                    && (high_qc.is_none() || high_vote.block_number > high_qc.block_number)
+                    && (high_qc.is_none() || high_vote.block_number > high_qc.vote.block_number)
                 {
                     // There was some proposal last view that might have been finalized.
                     // We need to repropose it.
@@ -98,7 +98,7 @@ impl Justification {
                     // that it couldn't have been finalized. Either way, we can propose
                     // a new block.
                     let block_number = match high_qc {
-                        Some(qc) => qc.block_number + 1,
+                        Some(qc) => qc.vote.block_number + 1,
                         None => 0,
                     };
 
diff --git a/spec/protocol-spec/replica.qnt b/spec/protocol-spec/replica.qnt
index f89ac1fd..ea44d11c 100644
--- a/spec/protocol-spec/replica.qnt
+++ b/spec/protocol-spec/replica.qnt
@@ -601,7 +601,7 @@ module replica {
 
                     | Some(qc) => {
                         val self1 = self.process_commit_qc(Some(qc))
-                        start_new_view(id, self1, signed_vote.vote.view + 1, Commit(qc))
+                        start_new_view(id, self1, signed_vote.vote.view + 1)
                     }
                 },
 
@@ -678,7 +678,7 @@ module replica {
                             ...self.process_commit_qc(qc.high_commit_qc),
                             high_timeout_qc: max_timeout_qc(qc_opt, self.high_timeout_qc)
                         }
-                        start_new_view(id, self1, signed_vote.vote.view + 1, Timeout(qc)),
+                        start_new_view(id, self1, signed_vote.vote.view + 1),
                     }
                 },
                 // unchanged variables
@@ -711,7 +711,7 @@ module replica {
                 }
 
             if (new_view_view > self.view) {
-                start_new_view(id, self1, new_view_view, new_view.justification)
+                start_new_view(id, self1, new_view_view)
             } else {
                 all {
                     replica_state' = replica_state,
@@ -731,7 +731,8 @@ module replica {
     // A step by the proposer for replica_id.
     // We pass new_block, which is used a substitute for: self.create_proposal(block_number).
     action proposer_step(replica_id: ReplicaId, new_block: Block): bool = all {
-        val replica_state_view = replica_state.get(replica_id).view
+        val replica = replica_state.get(replica_id)
+        val replica_state_view = replica.view
         val proposer_state_view = proposer_view.get(replica_id)
         all {
             // Check if we are in a new view and we are the leader.
@@ -745,7 +746,7 @@ module replica {
             // Get the justification for this view. If we have both a commit QC
             // and a timeout QC for this view (highly unlikely), we should prefer
             // to use the commit QC.
-            val justification = ghost_justifications.get((replica_id, replica_state_view))
+            val justification = replica.create_justification()
             // Get the block number and check if this must be a reproposal.
             val block_and_hash = justification.get_implied_block()
             val block_number = block_and_hash._1
@@ -798,8 +799,9 @@ module replica {
     }
 
     // a correct replica changes to a new view
-    action start_new_view(id: ReplicaId, self: ReplicaState, view: ViewNumber, justification: Justification): bool = {
+    action start_new_view(id: ReplicaId, self: ReplicaState, view: ViewNumber): bool = {
         // make sure that we do not go out of bounds with the new view
+        val justification = self.create_justification()
         all {
             VIEWS.contains(view),
             // switch to the Prepare phase
@@ -1016,6 +1018,26 @@ module replica {
         }
     }
 
+    def create_justification(self: ReplicaState): Justification = {
+        // We always have a timeout QC, at least, for the view 0.
+        // However, the type checker needs a well-typed value. Hence, use empty_tqc.
+        val empty_tqc: TimeoutQC = {
+            votes: Map(), agg_sig: Set(), high_commit_qc: None, ghost_view: 0
+        }
+        val high_tqc = self.high_timeout_qc.unwrap_or(empty_tqc)
+        match (self.high_commit_qc) {
+        | None =>
+            Timeout(high_tqc)
+
+        | Some(cqc) =>
+            if (cqc.vote.view >= high_tqc.ghost_view) {
+                Commit(cqc)
+            } else {
+                Timeout(high_tqc)
+            }
+        }
+    }    
+
     def justification_verify(justification: Justification): bool = {
         match (justification) {
             | Timeout(qc) =>
@@ -1675,4 +1697,18 @@ module replica {
     val views_over_2_example = CORRECT.forall(id => {
         replica_state.get(id).view <= 2
     })
+
+    // check this falsy invariant to see an example of a replica having
+    // both a high commit QC and a timeout QC for the same view
+    val high_commit_and_timeout_qc_example = CORRECT.forall(id => {
+        val self = replica_state.get(id)
+        match (self.high_commit_qc) {
+        | None => true
+        | Some(cqc) =>
+            match (self.high_timeout_qc) {
+            | None => true
+            | Some(tqc) => cqc.vote.view != tqc.ghost_view
+            }
+        }
+    })
 }
\ No newline at end of file