IronFleet: Proving Practical Distributed Systems Correct
đź“ś 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.”
✨ Summary
Paper summary
IronFleet presents a verification methodology for practical distributed systems that combines TLA-style state-machine refinement with Floyd–Hoare verification in Dafny. The system is divided into three layers: a concise centralized specification, an abstract distributed protocol, and a concrete imperative implementation. Refinement proofs connect the protocol to the specification and the implementation to the protocol, while a reduction argument handles interleavings among independently executing hosts. The methodology also includes verified libraries for data refinement, packet marshalling and parsing, collection reasoning, and temporal-logic proofs.
The authors apply the approach to two systems: IronRSL, a feature-rich Paxos-based replicated state-machine library, and IronKV, a lease-based sharded key-value store. They verify safety properties such as linearizability and preservation of key ownership, as well as liveness properties under explicit scheduling and network assumptions. The implementation-level proofs include bounded packet representations, parsing and serialization, mutable data structures, and integer-overflow concerns. The evaluated systems achieved competitive—but not baseline-matching—performance: IronRSL reached up to 18,200 requests per second and IronKV up to 28,800 requests per second. The reported development effort was approximately 3.7 person-years, with 39,253 lines of proof-related code and 5,114 executable implementation lines.
Subsequent influence
The project released its verification framework and implementations publicly, enabling continued experimentation with IronFleet’s Dafny-based methodology. Microsoft later published a related version, “IronFleet: Proving Safety and Liveness of Practical Distributed Systems,” as a Communications of the ACM research highlight. (github.com) Later research explicitly treats IronFleet as an important baseline for verified distributed systems: a liveness-verification paper describes it as the first use of SMT-based verification for distributed-protocol liveness while identifying its substantial manual proof and solver-tuning requirements. (doi.org) Other projects have reused or reimplemented its core ideas, including verified Rust/Verus work based on IronFleet’s specifications and refinement methodology, and VeriBetrFS, which reports using the IronFleet methodology for verified storage-system crash safety. (github.com) These references indicate continuing influence primarily as a research methodology and artifact for end-to-end verification of distributed and storage systems, rather than evidence of broad production deployment.