This is a literal transilation of TLA+ syntax to FizzBee syntax.

1. Maintain a bool variable newly_promoted to indicate a new leader
   who has not caught up on previous version topics.
2. Continue to update vtOffset and rtOffset for each node irrespective
   of whether the node is a leader or follower.
3. Make the leader and follower consumption serial instead of atomic
   - The leader will first post to version_topic, then, update the local datastore, then update the offsets
   - Similarly, the follower will first update its local datastore and then update the offsets.
   The system can crash at either of these points, and the design is verified to work even if the system crashes in between