6.5840 2026 Lecture 15:  Verification: IronFleet

IronFleet: Proving Practical Distributed Systems Correct (2015)

Claim: my raft labs are bug-free because
(1) I passed all the test cases
(2) Raft thesis has proofs
Q: Convincing?
A: No.
   Tests are incomplete, proof could be wrong, proof is not about code.  It
   would be nice if there was another way. Today's lecture will be about another
   way to achieving correctness.

IronFleet
  Formal verification for distributed systems
  Think about all the papers, all the "what-if"s. This is both an answer to "how
  to reason about those systems", and also might help more deeply understand why
  distributed systems are tricky to reason about.
  By the end of studying this paper, the goal is to know the fundamental
  distributed systems verification techniques.

Basic mechanized verification
  Picture:
  implementation
  specification: definition of what system should provide (trusted)
  proof: steps for showing that spec is satisfied (untrusted)
  proof checker: tool that reads spec, proof, and impl, and outputs "yes" or
  "no" (trusted)
  TCB (trusted computing base) includes spec and verifier

IronFleet methodology.

Hoare logic:
  demo
  precondition, postcondition, SMT solver (e.g. Z3), assertions, loop invariants
    sort function
    - spec (pre+post condition)
    - invariant
    - introduce a bug in code -> dafny verification fails
    Dafny can compile the verified code.
  Lesson: specification is trusted.
  (Further topics: weakest preconditions, separation logic)
  What about distributed systems though?

State machines
  Specify overall distributed systems behavior
    State: per-machine state, network state
    Init ⊆ State
    Next ⊆ State × State
  Picture:
  Spec state machine for lock
  Implementation state machine for lock
    Concurrency -> interleaving transitions
    Transfer packets
  State machines are just a tool---can be at whatever level

IronFleet-style refinement
  Low-level behaviors are subset of high-level behaviors; only care about
  "externally visible" events.
  Picture: lockservice refinement
  Could use stutters (v.s. IronFleet's more complex picture)
  Refinement is transitive

Invariants:
  Property that holds throughout execution
  Can capture important guarantees, or serve as an intermediate proof step
  e.g. only one leader per term in Raft implementation
  True after all "atomic" transitions
  Helps prove refinement


IronFleet methodology:
  Figure 3.
  Complex implementation state machine
  Slightly simpler protocol state machine
    mathematical integers, unbounded sequences, immutable types, sending
    high-level messages (rather than bytes)
  Trusted, simpler spec state machine
  Q: How to connect pre+postconditions of methods to state machine
  transitions?
  Q: how to prove refinement (for lock, need a refinement mapping)?

How to apply IronFleet methodology to Raft?
  Figure 3.
  Top-level spec: State is log. Init: empty. Transitions: Commit(op).
  Prelecture question: where would the leader election restriction go wrong?
  A: Could go wrong at any step: if the protocol state machine is incorrectly
  written, could prove refinement impl -> protocol, but get stuck at protocol ->
  spec. However, if protocol is correctly written, then impl -> protocol would
  get stuck (while protocol -> spec might be provable).

Induction:
  Fundamental rule in program verification
  Loop invariants use induction
  Inductive invariants for distributed systems
  Conceptual picture.
  E.g.
    (exists a valid Transfer packet for e and no node holds lock
     \/ all transfer packets are stale and one node holds lock)

Proof engineering:
  Figure 12, Proof effort.
  Automation; lots of different decision procedures, tradeoffs
  Triggers
  Libraries
  Opaqueness (e.g. temporal logic formulas)

Liveness v.s. safety
  Temporal Logic of Actions
  (Network is eventually good) -> every node will hold the lock infinitely often
  Must show:
  - for any infinite execution (subject to assumptions), there is a "good" state
  Assumptions are "fairness" assumptions
  Reasoning principles like "WF1"

10min Q&A

Limitations:
  No local concurrency => round robin scheduler
  No crash recovery
  No (verified) client libraries
  Not clear how to use a verified IronFleet system as part of a bigger verified
  system.

--------------------------------------------------------------------------------
sort.dfy example

predicate sorted(s: seq<int>) {
  forall i, j :: 0 <= i < j < |s| ==> s[i] <= s[j]
}

predicate pivoted(s: seq<int>, p: int) {
  forall i, j :: 0 <= i <= p < j < |s| ==> s[i] <= s[j]
}

method insertion_sort(a: array<int>)
  modifies a
  ensures sorted(a[..])
  ensures multiset(a[..]) == multiset(old(a[..]))
{
  var i := 1;
  while i < a.Length
    invariant 1 <= i
    invariant sorted(a[..(if i < a.Length then i else a.Length)])
    invariant multiset(a[..]) == multiset(old(a[..]))
  {
    var j := i;
    while j > 0 && a[j-1] > a[j]
      invariant 0 <= j <= i
      invariant multiset(a[..]) == multiset(old(a[..]))
      invariant sorted(a[..j])
      invariant sorted(a[j..i+1])
      invariant pivoted(a[..i+1], j)
    {
      a[j-1], a[j] := a[j], a[j-1];
      j := j - 1;
    }
    i := i + 1;
  }
}