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.
UW CSE’s Verdi team (students James Wilcox, Doug Woos, and Pavel Panchekha, and faculty members Zach Tatlock, Xi Wang, Mike Ernst, and Tom Anderson) has just completed the first full formal verification of the Raft consensus protocol – a landmark achievement. (In addition to garnering lots of attention, they garnered more than 120 stars on GitHub!)