We introduce a sequentialization procedure for fault-tolerant protocols that takes as input a Distal program and produces a sequentialized counterpart as output. The sequentialization procedure captures a representative subset of the behaviors of the input system and is easier to model check; for a broad class of protocols, it captures a representative for every behavior. Our notion of sequentialization-equivalence extends the well-studied notion of communication closure in distributed protocols, which relates asynchronous and synchronous executions. We implemented our sequentialization and applied it to verify several consensus protocols, including ZooKeeper Atomic Broadcast, and Raft, using the P framework. We considered P models that include critical safety bugs present in implementations and known by the community. The P model checker found these bugs only when using the sequential model but not in the original asynchronous counterparts.