@article{hawblitzel2017ironfleet,
author = {Hawblitzel, Chris and Howell, Jon and Kapritsos, Manos and Lorch, Jay and Parno, Bryan and Stephenson, Justine and Setty, Srinath and Zill, Brian},
title = {IronFleet: Proving Safety and Liveness of Practical Distributed Systems},
year = {2017},
month = {July},
abstract = {Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs, but it 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 temporal logic of actions-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."},
url = {http://approjects.co.za/?big=en-us/research/publication/ironfleet-proving-safety-liveness-practical-distributed-systems/},
journal = {Communications of the ACM},
volume = {60},
}