Verdi: a framework for implementing and formally verifying distributed systems

By James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, T. Anderson. ACM-SIGPLAN Symposium on Programming Language Design and Implementation, 2015

379 citations recorded by the source corpus.

Distributed systems are difficult to implement correctly because they must handle both concurrency and failures: machines may crash at arbitrary points and networks may reorder, drop, or duplicate packets. Further, their behavior is often too complex to permit exhaustive testing. Bugs in these systems have led to the loss of critical data and unacceptable service outages. We present Verdi, a framework for implementing and formally verifying distributed systems in Coq. Verdi formalizes various network semantics with different faults, and the developer chooses the most appropriate fault model when verifying their implementation. Furthermore, Verdi eases the verification burden by enabling the developer to first verify their system under 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 the first mechanically checked proof of linearizability of the Raft state machine replication algorithm, as well as verified implementations of a primary-backup replication system and a key-value store. These verified systems provide similar performance to unverified equivalents.

Subfields: Computer Networks and Communications

View Paper: https://www.semanticscholar.org/paper/5a8aafae38aeabd5533a271ab02396529b7b41c9

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Computer Networks and Communications

Citations in the corpus

Using Crash Hoare logic for certifying the FSCQ file system (2015, background): “Verdi [63] reasons about distributed systems written in Coq and can extract the implementation into executable code.”
This paper is included in the Proceedings of the 2022 USENIX Annual Technical Conference. (neutral): “Verdi [54] and Ironﬂeet [33] help build formally veriﬁed systems.”
Tendermint: Byzantine Fault Tolerance in the Age of Blockchains (2016, methodology): “Furthermore, Raft’s safety guarantees have been formally proven using the Coq proof assistant [106] and a framework built above Coq, called Verdi, for formally verifying distributed systems [104].”
CLN2INV: Learning Loop Invariants with Continuous Logic Networks (2019, background): “However, as programs have become increasingly complex, real-world program verification often requires prohibitively expensive manual effort (Wilcox et al., 2015; Gu et al., 2016; Chajed et al., 2019).”