@inproceedings{hawblitzel2015ironfleet,
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 Practical Distributed Systems Correct},
booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)},
year = {2015},
month = {October},
abstract = {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."},
publisher = {ACM - Association for Computing Machinery},
url = {http://approjects.co.za/?big=en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/},
edition = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)},
}