Formal Verification of Distributed Systems

In the past several years, full formal verification has become a viable option for ensuring the correctness of real systems. Tools like the Coq proof assistant allow engineers to rigorously prove that their programs behave correctly. In this talk, I'll discuss and demo both Coq itself and Verdi, the framework I've developed with my colleagues at the University of Washington to verify distributed systems. We recently used Verdi to complete the first formal verification of an implementation of the Raft distributed consensus protocol, and I'll talk about this result as well as about the future of distributed systems verification.

Doug Woos will be visiting us from University of Washington, where he is a Ph.D student in Computer Science focusing on systems, networks, and programming languages. Doug is the son of VTFun regular, Dennis.