We present pretend synchrony, a new approach to verifying distributed systems, based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous when verifying their correctness. To do so, we compute a synchronization, a semantically equivalent program where all sends, receives, and message bu ers, have been replaced by simple assignments, yielding a program that can be veri ed using Floyd-Hoare style Veri cation Conditions and SMT. We implement our approach as a framework for writing veri ed distributed programs in Go and evaluate it with four challenging case studies— the classic two-phase commit protocol, the Raft leader election protocol, single- decree Paxos protocol, and a Multi-Paxos based distributed key-value store. We find that pretend synchrony allows us to develop performant systems while making veri cation of functional correctness simpler by reducing manually speci ed invariants by a factor of 6, and faster, by reducing checking time by three orders of magnitude.