This repository includes the TLA+ specification for the modified vrPaxos (Prof.Annie Liu) comprising of the merged Leader/Scout/Commander. Included in the specification are invariants specified by in the vrPaxos paper.