Floyd–Hoare-style imperative verification5, 7 to reason about
those complexities while ignoring concurrency. To simplify
reasoning about concurrency, we impose a machine-checked
reduction-enabling obligation on the implementation. Finally,
we structure our protocols using always-enabled actions
(Section 4) to greatly simplify liveness proofs.
To illustrate IronFleet’s applicability, we have built and
proven correct two rather different distributed systems:
IronRSL, a Paxos-based12 replicated-state-machine library,
and IronKV, a sharded key-value store. All IronFleet code is
IronRSL, our first application, has a complex implementation including many details often omitted by prior work, such
as state transfer, log truncation, dynamic view-change timeouts, batching, and a reply cache. We prove full functional
correctness and the key liveness property: if the network is
eventually synchronous for a live quorum of replicas, then clients that persist in sending requests eventually get replies.
Unlike IronRSL, which uses distribution for reliability,
IronKV uses it for improved throughput by moving “hot”
keys to dedicated machines. For IronKV, we prove complete
functional correctness and an important liveness property:
if the network is fair then the reliable-transmission component eventually delivers each message.
While verification rules out a host of problems, it is not
a panacea. IronFleet’s correctness relies on several assumptions (Section 2. 4). Also, verification requires more up-front
development effort: the automated tools we use fill in many
low-level proof steps automatically, but still require considerable assistance from the developer. Finally, we focus on
verifying newly written code in Dafny, a verification-friendly
language (Section 2. 2), rather than verifying existing code.
2. BACKGROUND AND ASSUMPTIONS
We briefly describe the existing verification techniques that
IronFleet draws upon, as well as our assumptions.
2. 1. State machine refinement
State machine refinement11 is often used to reason about dis-
2. 2. Floyd–Hoare verification
tributed systems. 1, 8, 18 The developer describes the desired
system as a simple abstract state machine with potentially
infinitely many states and with nondeterministic transition
predicates. She then creates a series of increasingly com-
plex (but still declarative) state machines, and proves that
each one refines the one “above” it (Figure 1). State machine
L refines H if each of L’s possible behaviors, that is, each
(potentially infinite) sequence of states the machine may
visit, corresponds to an equivalent behavior of H. State
machine refinement in a distributed-system context (e.g.,
TLA-style refinement13) typically considers declarative speci-
fications, not imperative code.
Many program verification tools support Floyd–Hoare style5, 7
first-order predicate logic reasoning about imperative programs. That is, the programmer annotates a program with
assertions about the program’s state, and the verifier checks
that the assertions hold for all possible program inputs. For
example, the code in Figure 2 asserts a condition about its
input via a precondition and asserts a condition about its output via a postcondition.
We use Dafny, 14 a high-level language that automates verification via the Z32 SMT solver. This enables it to fill in many
low-level proofs automatically; for example, it easily verifies
the program in Figure 2 for all possible inputs x without any
However, many proposition classes are not decidable in
general, so Z3 uses heuristics. For example, propositions
involving universal quantifiers (∀) and existential quantifiers
(∃) are undecidable. Thus, it is possible to write correct code
in Dafny that the solver nevertheless cannot prove automatically. In such cases, the developer may insert annotations to
guide the verifier’s heuristics to a proof.
Once a program verifies, Dafny compiles it to C# and has
the .NET compiler produce an executable. Other languages
(e.g., C++) are currently unsupported, but it would be possible to compile Dafny to them to, for example, simplify integration with existing code. Our previous work6 shows how to
compile Dafny to verifiable assembly to avoid depending on
the Dafny compiler, .NET, and Windows.
Like most verification tools, Dafny only considers one
single-threaded program, not a collection of concurrently
executing hosts. Indeed, some verification experts estimate
that the state-of-the-art in concurrent program verification
lags that of sequential verification by a decade. 19
2. 3. Temporal logic of actions (TLA)
Temporal logic and its extension TLA11 are standard tools
for reasoning about safety and liveness. Temporal logic
formulas are predicates about the system’s current and future
states. The simplest type of formula ignores the future; for
example, a formula P could be “host h holds the lock now.”
Other formulas involve the future; for example, ◊P means
P eventually holds, and P means P holds now and forever.
Thus, ∀h ∈ Hosts: ◊P means that for any host, it is always
true that h will eventually hold the lock.
H0 H1 H2 H3 H4
L0 L1 L2 L3 L4 L5 L6 L7
Figure 1. State machine refinement. The low-level state machine
behavior L0…L7 refines the high-level behavior H0…H4. Each
low-level state corresponds to a high-level state; for each such
correspondence, shown as a dashed line, the two states must satisfy
the spec’s refinement conditions. Each low-level step maps to one
high-level step (e.g., L0→L1 maps to H0→H1) or no high-level steps
(e.g., L2→L3). method halve(x:int) returns (y:int) requires x > 0;
ensures y < x;
y := x / 2;
Figure 2. Simple Floyd–Hoare verification example.