Implementing reliable distributed systems is challenging because they run in unreliable environments and must tolerate faults gracefully: machines may crash and networks may reorder, drop, or duplicate packets. Failing to do so can lead to catastrophic failures and major outage of web services.

We present Verdi, a framework for implementing and formally verifying practical distributed systems in Coq. Verdi formalizes five network semantics with different kinds of faults, and allows developers to choose the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling developers to construct systems from modular components. This separation of concerns eases reasoning because the developer can verify their system in an idealized fault model, then transfer the resulting correctness guarantees to a more realistic fault model without any additional proof burden. To demonstrate Verdi’s utility, we present a series of case studies including a key-value store application and a primary-backup replication mechanism.