Verdi

Formally Verifying Distributed Systems

Distributed systems are hard to get right in large part because they must tolerate faults gracefully: machines may crash and the network may drop, reorder, or duplicate packets. Verdi is a framework from the University of Washington to implement and formally verify distributed systems. Verdi supports several different fault models ranging from idealistic to realistic. Verdi's verified system transformers (VSTs) encapsulate common fault tolerance techniques. Developers can verify an application in an idealized fault model, and then apply a VST to obtain an application that is guaranteed to have analogous properties in a more adversarial environment.

Verdi is developed using the Coq proof assistant, and systems are extracted to OCaml for execution. Verdi systems, including a fault-tolerant key-value store, achieve comparable performance to unverified counterparts.

News

We have recently finished verifying an implementation of the Raft consensus protocol in Verdi. Our paper describing this effort will appear at CPP 2016!

By “popular” demand, here are the slides from the Verdi talk at PLDI 2015. If you use these in a reading group, we'd love to hear from you with comments and questions.

Check out our Video abstract!

Source

Both the Verdi framework and our verified Raft implementation are open-source. Please feel free to submit comments, issues, and pull requests on either repository.

Publications

James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang, Michael D. Ernst, and Thomas Anderson. Verdi: A Framework for Implementing and Verifying Distributed Systems. PLDI 2015, Portland, OR, June 2015.
Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst, and Thomas Anderson. Planning for Change in a Formal Verification of the Raft Consensus Protocol. CPP 2016, St. Petersburg, FL, January 2016.

Blog posts about Verdi

Network Semantics for Verifying Distributed Systems. This is the first post in a series on Verdi. In this post, we'll get our feet wet by defining a formal model of how distributed systems execute on the network.

How to build a simple system in Verdi. This long-awaited post shows how to implement and verify a simple distributed system in Verdi.

The Verdi Team

The Verdi developers can be reached via email. Feel free to email if you're using Verdi, thinking about using Verdi, or have questions. Verdi is developed in the University of Washington Programming Languages and Software Engineering group, by