diff --git a/safekeeper/spec/ProposerAcceptorReconfig.tla b/safekeeper/spec/ProposerAcceptorReconfig.tla
index f5793bd2d4..4a9b459024 100644
--- a/safekeeper/spec/ProposerAcceptorReconfig.tla
+++ b/safekeeper/spec/ProposerAcceptorReconfig.tla
@@ -29,6 +29,7 @@ PAS == INSTANCE ProposerAcceptorStatic
 \* Is c a valid config?
 IsConfig(c) ==
     /\ DOMAIN c = {"generation", "members", "newMembers"}
+    \* Unique id of the configuration.
     /\ c.generation \in Nat
     /\ c.members \in SUBSET acceptors
     \* newMembers is NULL when it is not a joint conf.
@@ -66,9 +67,18 @@ Init ==
 \* + 1.
 RestartProposer(p) ==
     /\ \E a \in acceptors: PAS!RestartProposerWithTerm(p, acc_state[a].term + 1)
+    \* Reset conf to NULL; ProposerBumpConf will communicate it before voting can start.
     /\ prop_conf' = [prop_conf EXCEPT ![p] = NULL]
     /\ UNCHANGED <<acc_conf, conf_store>>
 
+\* Acceptor a immediately votes for proposer p.
+Vote(p, a) ==
+    \* Configuration must be the same.
+    /\ prop_conf[p] /= NULL
+    /\ prop_conf[p].generation = acc_conf[a].generation
+    /\ PAS!Vote(p, a)
+    /\ UNCHANGED <<prop_conf, acc_conf, conf_store>>
+
 \* Do CAS on the conf store, starting change into the new_members conf.
 StartChange(new_members) ==
     \* Possible only if we don't already have the change in progress.
@@ -76,6 +86,27 @@ StartChange(new_members) ==
     /\ conf_store' = [generation |-> conf_store.generation + 1, members |-> conf_store.members, newMembers |-> new_members]
     /\ UNCHANGED <<prop_state, acc_state, committed, elected_history, prop_conf, acc_conf>>
 
+\* Proposer p adopts higher conf from acceptor a.
+ProposerBumpConf(p, a) ==
+    \* It happens when either p doesn't have conf at all yet or it is lower than a's.
+    /\ \/ prop_conf[p] = NULL
+       \* TLA+ disjunction evaluation doesn't short-circuit for a good reason:
+       \* https://groups.google.com/g/tlaplus/c/U6tOJ4dsjVM/m/UdOznPCVBwAJ
+       \* so repeat the null check.
+       \/ (prop_conf[p] /= NULL) /\ (acc_conf[a].generation > prop_conf[p].generation)
+       \* When conf is bumped before proposer is elected we reset its state
+       \* (preserving config and doing inc on term to have a chance for
+       \* succeeding election) because some of the votes already collected could
+       \* have been from non-members of updated conf. Resetting is simpler than
+       \* figuring out these.
+    /\ IF prop_state[p].state = "campaign" THEN
+           PAS!RestartProposerWithTerm(p, prop_state[p].term + 1)
+        \* Otherwise we allow to bump conf without restart.
+       ELSE UNCHANGED <<prop_state>>
+    /\ prop_conf' = [prop_conf EXCEPT ![p] = acc_conf[a]]
+    /\ UNCHANGED <<acc_state, committed, elected_history, acc_conf, conf_store>>
+
+
 \*******************************************************************************
 \* Final spec
 \*******************************************************************************
@@ -83,7 +114,8 @@ StartChange(new_members) ==
 Next ==
   \/ \E new_members \in SUBSET acceptors: StartChange(new_members)
   \/ \E p \in proposers: RestartProposer(p)
-\*   \/ \E p \in proposers: \E a \in acceptors: Vote(p, a)
+  \/ \E p \in proposers: \E a \in acceptors: ProposerBumpConf(p, a)
+  \/ \E p \in proposers: \E a \in acceptors: Vote(p, a)
 \*   \/ \E p \in proposers: BecomeLeader(p)
 \*   \/ \E p \in proposers: \E a \in acceptors: UpdateTerm(p, a)
 \*   \/ \E p \in proposers: \E a \in acceptors: TruncateWal(p, a)
diff --git a/safekeeper/spec/modelcheck.sh b/safekeeper/spec/modelcheck.sh
index 2b9ba0e071..ba854611c5 100755
--- a/safekeeper/spec/modelcheck.sh
+++ b/safekeeper/spec/modelcheck.sh
@@ -46,5 +46,6 @@ echo "" >> $outfile
 # https://docs.tlapl.us/codebase:architecture#fingerprint_sets_fpsets
 #
 # Add -simulate to run in infinite simulation mode.
+# -coverage 1 is useful for profiling (check how many times actions are taken).
 java -Xmx$MEM -XX:MaxDirectMemorySize=$MEM -XX:+UseParallelGC -Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet \
   -cp "${TOOLSPATH}" tlc2.TLC $SPEC -config $CONFIG -workers auto -gzip | tee -a $outfile