IronFleet: Proving Practical Distributed Systems Correct - Hawblitzel, Chris; Howell, Jon; Kapritsos, Manos; Lorch, Jay; Parno, Bryan; Stephenson, Justine; Setty, Srinath; Zill, Brian (Proceedings of the ACM Symposium on Operating Systems Principles (SOSP), 2015)
Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs a priori, but verification has historically been difficult to apply at full-program scale, much less distributed-system scale. We describe a methodology for building practical and provably correct distributed systems based on a unique blend of TLA-style state-machine refinement and Hoare-logic verification. We demonstrate the methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store. We prove that each obeys a concise safety specification, as well as desirable liveness requirements. Each implementation achieves performance competitive with a reference system. With our methodology and lessons learned, we aim to raise the standard for distributed systems from "tested" to "correct."