Ironfleet: Proving Safety and Liveness of Practical Distributed Systems
We demonstrate the methodology on a complex implementation of a Paxos-based replicated state machine library and a lease-based sharded key-value store. With our methodology and lessons learned, we aim to raise the standard for distributed systems from "tested" to "correct."
