Introduction

jetstream_distributed is a set of distributed protocols written in Verus, plus the Jetstream services that speak them. The protocols are exclusive mutable ownership of an actor across machines, Raymond’s routing layer, Raft, SWIM gossip membership, and a distributed actor with a mailbox in front of it.

Rust:
    at most one mutable reference

Distributed ownership:
    at most one authoritative mutable owner

This is not Rust’s borrow checker extended across a network. It is a runtime protocol, and the proofs are about a model of it. The Reference says exactly what is claimed and what is not, starting with what this is, and what it is not.

What this book is for

It has two parts, and they answer different questions.

The chapters answer: how do the algorithms relate to each other? Which one assumes what the others provide, which two are glued together and how, which are independent, and where a relationship is intended but not built yet. They are short, and they are written to be read in order.

The Reference is the full record, which used to be the repository’s README: every theorem, with the name of the proof and what it assumes, and what each result does not say. It is long, because each algorithm is described in detail, and it is meant to be looked things up in, not read through.

The chapters do not repeat the Reference’s claims tables. Where a chapter makes a claim it gives the row number (A14, MB10, C54) and links to the table, so the statement of what is proved lives in one place.

How to read it

Start with How the algorithms relate. It is one page, and every later chapter is a closer look at one box in its picture. Then read Evidence before trusting any sentence in this book that contains the word “guarantee”: it explains the three tiers (proved, tested, assumed) and the file naming that tells them apart.

The protocol chapters are in the order the dependencies run, so each one can lean on the ones before it:

1. Ownership, the base everything else uses or assumes.
2. Raymond and Composed, which route the privilege and tie the routing to ownership.
3. Raft, which is how the base’s strongest assumption could be bought.
4. SWIM, which agrees on nothing and promises only that views converge.
5. The actor and the mailbox, which sit on ownership.

The next three chapters are about running these: the services, placement and discovery, and the actor system over QUIC. After them, usage examples are runnable programs, and the Reference follows.

What this book will not do

It will not say a thing is proved when it is only tested. Where the code and the book disagree, the code wins and the book is the thing to fix. Where a chapter describes a design that is not built, it says “not built” in the same sentence.

How the algorithms relate

One page. Every later chapter is a closer look at one box.

The picture

   Raft                                   SWIM
   consensus                              membership by merge
   · · · · · · · · ·                      · · · · · · · · · ·
   :  could buy    :                      :  a hint to      :
   :  the atomic   :                      :  placement      :
   :  registry     :                      :  (QUIC system)  :
   ▼ · · · · · · · ·                      ▼ · · · · · · · · ·
 ┌───────────────────────┐   couples   ┌───────────────────┐
 │ Ownership             │◄────────────│ Raymond           │
 │ epochs, fencing       │             │ routes the        │
 │ "who may mutate"      │             │ privilege         │
 └───────────────────────┘             └───────────────────┘
      ▲            ▲                           ▲
      │ fences     └────────────┬──────────────┘
      │ the journal             │ guards tie the two
      │                    ┌────┴─────────────────┐
 ┌────┴─────────────┐      │ Composed             │
 │ Actor            │      │ one machine, both    │
 │ a journal, and   │      │ layers               │
 │ the state it     │      └──────────────────────┘
 │ folds to         │
 └────▲─────────────┘
      │ delivers to
 ┌────┴─────────────┐
 │ Mailbox          │
 │ the queue in     │
 │ front of it      │
 └──────────────────┘

Solid lines are relationships the code builds: one module imports or enforces the other. Dotted lines are relationships that are intended or are a hint only. The difference matters, and the rest of this page is mostly about it.

Three ways of getting one answer

The protocols do not agree on how to get a single authoritative answer in a system where nobody can see everything. They buy it three different ways, and the difference is the reason they are all here.

Ownership is the one that depends on the others. Its strongest assumption is a single atomic, durable registry. Raft is the standard way to make a record like that fault-tolerant, which is why it is in the repository, and SWIM is the standard way to notice that a node has gone, which ownership treats as unreliable by construction (below).

The relationships, one by one

Ownership ← Raymond: routing never grants authority

Raymond routes a single privilege between peers. The ownership model says who may mutate. The glue is one predicate:

couples(r, s) = every node that may mutate in s holds the privilege in r

The direction is the point. Routing only constrains who could have authority; it never creates it. So a duplicated or reordered request cannot manufacture an owner. That is Raymond’s chapter.

Composed: the guards are the relationship

On its own couples is only a predicate, and nothing stops a token moving out from under an owner. Composed defines one state machine over both layers and turns the synchronisation into guards: the privilege may pass only once the actor is Unowned, and a node may acquire only if it holds the privilege. Crash takeover is a separate step (SeizeToken), so the safety claim is not restricted to executions where the privilege always moves voluntarily.

Ownership ← Actor: the journal write is the fenced mutation

An actor’s state is not held by its host. It is a journal of accepted messages, and the state is a fold over it. Appending is the one thing a host does that matters, and the ownership layer fences it. So the actor’s exclusivity theorems are the ownership layer’s, used as they are, and a handover moves no state: the new owner reads the same journal and recomputes. See the actor.

Actor ← Mailbox: refusing out of order needs something that retries in order

The actor refuses a message that arrives ahead of its turn rather than buffering it. That is safe and also useless on its own, because nothing makes a refused message arrive again. The mailbox is the queue that does, and it is where the first liveness theorem lives, under a stated fairness assumption. See the mailbox.

Ownership ⇢ Raft: the strongest assumption, and the one unbuilt edge

Ownership’s first assumption is that the owner record is updated atomically, which in a real deployment must be bought from consensus. Today the ownership service buys atomicity from a process-local lock and survival from a durable, monotone epoch floor, so a restarted registry cannot move epochs backwards. It does not replicate. Raft proves Election Safety, Log Matching and State Machine Safety (with one stated hypothesis), but nothing connects it to the registry. Raft says where the missing connection would go.

SWIM ⇢ everything else: an unreliable detector, by design

Ownership does not trust failure detection. Its model lets the coordinator revoke a perfectly healthy node, and safety has to survive that: it comes from the epoch bump, not from the detector being right. SWIM’s Suspect and Dead are exactly that kind of signal, which is why using them as a hint is consistent with the proofs. In the QUIC system a suspect host is not placed on and a dead one is not found, and nothing moves an actor. See SWIM and the actor system.

A pattern that repeats: belief versus authority

Three layers separate what a node believes from what is so, and the same discipline keeps each safe:

A node cannot fence itself. A partitioned owner accepts its own stale epoch, and the rejection that matters happens at the resource. Every chapter that follows leans on this.

HyParView: unconnected, so far

HyParView answers a different question from SWIM (who should I gossip with?, with no verdict on anyone) and is built beside it. Nothing consumes it, and nothing in the code relates it to SWIM beyond both being membership. It is one node’s views and handlers; the property that makes a cluster of them an overlay (symmetric active views) is not claimed.

What is not related yet

Said plainly, because a map that implies edges that do not exist is worse than none:

• Raft and ownership are not connected. Nothing runs the registry on a replicated log.
• Raymond and the composed services keep the global record in one process. They check the rules; they do not distribute them.
• Host, the journal service, does not sit behind the mailbox, though the mailbox is proved in front of the model.
• Nothing here proves liveness of a handover. Safety survives every failure the model admits; progress does not.
• No automatic failover. Membership can say a host left. Nothing yet decides to move its actors, and doing so from a partition starts a second copy that only the ownership epoch keeps harmless.

Evidence: proved, tested, assumed

Every claim in this repository is in one of three tiers, and the tiers are not interchangeable. A sentence in this book that says “guarantee” means the first tier unless it says otherwise.

What “proved” is about

The core of the repository is a model, and the proofs are about the model. Each algorithm also has verified executable code (small u64-valued functions and the records they act on), each with a postcondition stated in the model’s terms and a theorem discharging it. That is how the gap between model and code is narrowed: the service calls the function the theorem is about.

It is narrowed, not closed. The lock around a verified core, the roster, the network and the scheduler are not under proof. The Reference’s status section lists, by name, what is proven, what is modelled and not proven, and what is not modelled at all.

Reading the file names

The naming follows the vendored verified-storage convention, and it tells you which tier a file is in before you open it:

The most important thing to audit in a proof repository is the part nothing checks, so the trusted files are where to start. The model never imports the specification layer, so a specification cannot be quietly weakened to fit the model.

The rules the repository holds itself to

• No escape hatches. assume, admit, axiom, external_body and friends are rejected by CI in src/. The one documented exception is the vendored persistent-memory log, whose assumptions are listed.
• Nothing vendored is edited. The vendored directories are verbatim copies at a pinned commit, and CI diffs them.
• Say what is proved and what is merely tested. The running mailbox is a transcription of the mailbox model, not a refinement; only its queue-and-flags core is verified. A doc that blurs that is a bug.

What CI runs

Every pull request runs the whole of this: both Verus entry points over the crate, the vendored log’s proof check, the service tests, the simulated-network scenarios, a minute of coverage-guided fuzzing of the protocol search, and a check that the vendored skills are unmodified.

The simulated network is the part that reaches past the proofs. It runs the executable protocol under duplicated, reordered, delayed and dropped messages, with runtime oracles checking the same properties the theorems state, and a search over seeds with the ones that once broke something kept as a regression replay.

How to read a claim row

Each row in the Reference’s claims tables has the same four parts: a number (A14, MB10, C54), what is claimed, the name of the Verus theorem, and what it assumes. The last column is the one to read. A theorem with none there holds in every state. One that says reachability or an execution holds in every state a run can reach. One that names a hypothesis holds given it, and the hypothesis is stated so it can be discharged.

What this book does not prove

Nothing here is a proof. The chapters explain how the protocols fit and say which of the Reference’s claims each relationship rests on. If a chapter and the Reference disagree about what is proved, the Reference and the code are right, and the chapter is the thing to fix.

Checking it yourself

cargo test                              # services, simulated-network tests, unit tests
verus --crate-type=lib src/lib.rs       # the proofs (needs the pinned Verus)
cargo verus verify --no-default-features
mdbook build book                       # this book

Verus is pinned, with the Rust toolchain it was built against. If it is not installed, CI is the check.

Ownership: epochs and fencing

Ownership is the base. Everything else in this book either uses it (the actor), is tied to it (Raymond, through Composed), or is a way to satisfy its assumptions (Raft).

The state machine

An actor is, at any moment, in one of three states:

Owned        { owner, epoch }
Transferring { from, to, old_epoch, new_epoch }
Unowned      { epoch, intended_owner }

Ownership never moves atomically. A handover is four transitions:

Owned(A, 41)
      |  BeginTransfer(A -> B)         epoch 42 is allocated here
Transferring(A, B, 41, 42)
      |  CompleteRelease
Unowned(42, B)
      |  Acquire(B)
Owned(B, 42)

Two choices carry the whole design:

• The epoch advances at the start of a handover, not the end. From the moment A agrees to transfer, the current epoch is 42, so A’s epoch-41 authority is already fenced out. A does not need to be reachable, or alive, for that to take effect.
• Nobody has authority during the middle two stages. The design gives up availability during a handover so that double ownership is not representable. Neither node having authority is acceptable; both having it is not.

Who may mutate

Authority is one predicate, true in exactly one shape:

may_mutate(s, node, epoch) =
    s is Owned { owner, epoch: e }  and  node == owner  and  epoch == e

That is why exclusivity is structural here: two owners is not a state the model can represent, so the work is in showing that no transition reaches a bad state. Compare Raft, where nothing is structural and exclusivity is a counting argument over a set that no participant can see.

A server checks an incoming request with valid_fence(s, e) = e >= current_epoch(s). While Transferring, the current epoch is the new one, which is what makes the outgoing owner stale immediately.

Tokens are physical; authority is not

A Token { actor, epoch, holder } can be copied, survives a crash, and can be held by a node that was partitioned away for an hour. The model says so: the set of issued tokens only grows. Whether a token confers authority is a separate question, answered by the actor’s current state. Stale tokens exist and are inert.

What the proofs assume

The failure model is part of the system, not a side condition. The ones that matter for how the layers fit together:

Not claimed: liveness. Nothing says a transfer completes or that an actor ever becomes owned again. Safety survives every case in the table; progress does not.

The full table, and every theorem with the name of its proof and what it assumes, is in the Reference: failure model and claimed invariants.

Prior art: Chubby

The fencing mechanism is Chubby’s. A Chubby sequencer carries the lock name, mode and lock generation number, and the resource server is expected to reject a stale one. That is Token plus valid_fence, and the generation number is the model’s Epoch. What this repository adds is the proof, and the precision a proof forces: who may mutate is one predicate, and “a node cannot fence itself” cannot stay implicit. The Reference’s Relation to Chubby is the careful version, including the three deliberate differences (no timing, consensus assumed, peer-to-peer routing).

The service

The ownership service is the model run over Jetstream. Three things about it matter to the other chapters:

• Identity comes from the connection, never from an argument. No method takes a node number; the caller is the transport’s Context. Today that is an address against a roster fixed at construction, and an address is not a credential: it is as good as one in the simulated network and worth little on a real one.
• force is not on the wire. It is the coordinator’s own transition (revoking an owner), so a node-facing service does not offer it.
• The registry survives restarts. A process-local lock buys atomicity and none of survival, and a registry that forgets can move epochs backwards, which every fencing theorem forbids. So the starting epoch is read from a durable, monotone EpochFloor, and every burn is written down before the state that depends on it is visible. A registry that dies between the two skips an epoch, which is the safe direction to fail.

Next: Raymond, which routes the privilege and is tied to this.

Raymond: routing the privilege

Raymond’s algorithm is a distributed mutual-exclusion scheme. Here it is modelled as a routing layer, kept strictly separate from ownership semantics: it answers “which way is the privilege?”, never “who may mutate?”.

What each node keeps

Per node: a holder pointer, a request queue, an asked flag and a using flag. Alongside them, deliberately not derived from them, is privilege: the node that actually holds it.

request:  D -> B -> A -> C[token]
token:    C -> A -> B -> D

Requests travel hop by hop towards the token, and the token travels back along the reverse path.

Belief versus authority

The split between holder and privilege is the routing counterpart of the issued tokens versus the current state in ownership:

The split exists so that a seizure can take the privilege from a node without reaching into it. No implementation can edit the state of a node that is down, and an earlier version of the model assumed exactly that. After a seizure both holder[A] == A and holder[B] == B, and that is deliberate: A is a stale holder whose belief nobody could correct. Uniqueness belongs to privilege, not to the belief graph.

So the unconditional guarantee is an acyclic forest of beliefs plus one authoritative holder. Following the pointers to that holder needs one more condition, ray_no_stale_holders, which is what reconciliation restores.

Requests are state

Requests in flight are explicit state: every request ever sent, as an (originator, destination) pair. The set only grows and delivery does not consume it, the same choice the ownership layer makes for its network. The destination is resolved at send time, so a request can be delivered after the token has moved. A guard phrased against the live pointer would drop it silently, and “arbitrary delay” would have been claimed but not modelled.

How it is tied to ownership

One predicate:

couples(r, s) = every node that may mutate in s holds the privilege in r

Routing never grants authority; it only constrains who could have it. That is why a routing step, including a duplicated or reordered request, cannot manufacture an owner: it does not change who could be the owner.

On its own couples is only a predicate. Nothing in the routing layer sees the ownership state, so nothing stops the token moving out from under a node that still has authority. Composed closes that gap.

What is and is not claimed

• Claimed: at most one privilege holder, routing cannot manufacture ownership, duplicated, reordered and arbitrarily delayed requests are safe, and the executable routing steps agree with the model in both directions.
• Not claimed: liveness. “Every request is eventually served” needs FIFO, reliable links and no crashes, and none of those are assumed.
• No crash model of its own. The ownership layer models crash, recovery and unreliable detection; Raymond’s steps do not. What is modelled is the case that matters for the composed claim, a seizure that re-establishes the token without the holder acting.
• The service hosts the whole record in one process. The router holds every node’s entries under one lock because the model’s Raymond is one struct. It checks the rules; it does not distribute them. A deployment where each node keeps only its own entries is a different system, and nothing here says this one refines it.

The routing claims are the R-rows in the Reference’s Raymond section, including seizure without an oracle.

Next: Composed.

Composed: the two as one machine

Ownership says who may mutate. Raymond routes a privilege. Composed is the only place the two meet, and it meets them with guards, not assumptions.

Why a predicate is not enough

couples(r, s) says every node that may mutate holds the privilege. Stated as a predicate it is a hypothetical: the routing layer never sees the ownership state, so a routing step that moves the token has no way to know a node still has authority. The question “does token transfer preserve ownership safety?” has no answer until there is one machine in which both kinds of step happen.

The synchronisation is a guard

Composed defines one state machine over both layers. The steps that touch both are guarded:

Two carrier steps pass everything else through: Ray carries every Raymond step that does not move the token (request routing, entering and leaving the critical section), and Own carries every ownership transition that does not create authority over the actor.

Ray is guarded on “preserves the token”, deliberately wider than “is a routing step”. Had it admitted only routing, no execution could enter a critical section, every reachable state would keep using false, and the theorems would cover a degenerate fragment. A scenario that builds an execution from the initial state to one with a node inside the critical section rules that out the only way that counts: by exhibiting it.

What is then provable

couples becomes an invariant of the machine rather than a side condition: in every reachable composed state the only node that may mutate the actor is the node holding the token. Because the guards are what enforce it, “token transfer preserves ownership safety” is a claim about the system and not a hypothetical.

SeizeToken matters for the same reason. Without it the only token movement was a voluntary pass, so the invariant was quantified over executions where the token always moves politely. Crash-driven takeover, which is the case epochs exist for, was not among them. A scenario exhibits the crash takeover as a reachable execution.

A seizure leaves the old holder believing it still holds the privilege. The composed steps keep reconciliation debts: the nodes that owe a reconciliation after being seized from. That is the executable form of “a stale holder whose belief nobody could correct”, and reconcile is what clears it.

The executable side

The composed steps over both layers’ records (pass_token, seize_token, acquire_under_token, reconcile) are verified code whose contracts are the composed model’s steps. The coupling guards agree with the model in both directions, and a step a layer already proved is carried without a second proof.

What is not claimed

• The composed service refines the crash-free executions only. The composed model guards some steps on own.live, which is ground truth and not something a process can evaluate. The service has no Crash or Recover, so liveness of a node is a hypothesis for the steps that name a node that is not the caller. Seizing from a holder that is merely unreachable is inside the fragment, because SeizeToken has no liveness guard on the node it takes the privilege from.
• Both layers live behind one gate in one process. The Coordinator serialises them because the coupling reads both. It checks the rules; it does not distribute them. The coupling’s four steps are now data (Command, run through apply), which is what a replicated coordinator would need first; what it would need after that is in the Reference.
• The nodes involved must be live for a recipient or a seizure target. The service’s identity lookup speaks only for the caller, and a recipient of a passed privilege is not a caller, so nothing in the service establishes that for them.

The rows are CX1 and CX2 and the composed rows in the Reference’s claims table.

Next: Raft, which is about the assumption this chapter, like the last one, leaned on.

Raft: buying the atomic registry

Ownership’s strongest assumption is that the owner record is updated atomically, so that two coordinators cannot both read Owned { A, 41 } and allocate epoch 42 for different successors. A real deployment has to buy that from consensus, or from a store with compare-and-swap. Raft is the first half of buying it.

Status: not connected. Nothing outside src/raft/ imports Raft. The registry the ownership service runs is a process-local record with a durable epoch floor. This chapter is about what Raft proves and where the connection would go, not about a connection that exists.

The same statement, bought differently

Raft’s Election Safety is the exclusivity theorem with two words changed:

ownership:  at most one authoritative owner per epoch, because a single
            atomic registry hands the epoch out
raft:       at most one leader per term, because any two quorums share a
            voter and a voter votes once per term

The difference is why both are here. Ownership’s exclusivity is structural: two owners is not a state. In Raft nothing is structural. A cluster can perfectly well hold two servers who both believe they lead term 7. Ruling that out is a counting argument over a set that no single participant can see. Side by side, the two say what a coordinator costs.

The argument is three sentences, and the interesting clause is the one not in them: a cast vote is never ahead of its voter’s term. Without it the induction fails at the most ordinary step in the protocol, a server timing out into term t + 1 and voting for itself there.

The log

The model has a log. A client request stamps an entry with its leader’s term; append carries one entry under the consistency check and truncates whatever diverged; commit advances under figure 8’s restriction; a vote carries the up-to-date comparison.

What follows from a single step (a leader only appends, a follower agrees before it accepts, an entry is copied and not invented, a commit needs a majority of the committing leader’s own term) is the easy part. Log Matching is proved too, and it needed something the model did not have:

Ruling out a second entry at the same (index, term) is a fact about the run’s history, not about any one state. Nothing in the state says no leader of that term ever appended at that index before.

So the cluster carries ghost fields, each added because some question about the run has no answer in a single state: every (server, term) ever led; every entry any leader ever created, with the term of the entry before it; every entry any leader ever committed (the commit counter retreats, so a count cannot record it); and every vote together with the voter’s log as it stood when the vote was cast.

State Machine Safety, with one hypothesis

State Machine Safety is proved with exactly one hypothesis: that two commits at an index agree on the entry’s term. The value half is unconditional, because one (term, index) names one act of creation by one leader. Nothing about values, quorums or counting is missing; what remains is the induction hypothesis over leaders of terms, stated as one and with its upper endpoint still owed.

The durable log

The log’s storage is verified at the encoding level: recovery is exact, a crash can only rewind, and a byte prefix of the device parses back to a record prefix, so figure 2’s suffix deletion is implementable on a device that deletes nothing.

It is not wired to a device, and the obstacle is a crash model, not an interface: the persistent-memory log’s chunk size is 8 and a write must be safe for any subset of 8-byte chunks having flushed, which POSIX does not promise for a write crossing a chunk. Until a device supplies that, the vendored log’s two corruption assumptions are not assumptions of anything proved here.

Where the connection would go

Said as a design direction, not a plan: the registry’s record is the state a replicated log would carry, and the epoch-advancing transitions are the entries. Three things stand between here and there, and none is built:

1. A state machine on top of the log. The model’s server has a log and a commit count and no applied state: it proves the log, not what is applied from it.
2. The ownership registry reading and writing through it, instead of through a lock.
3. A device for the log, for the crash-model reason above.

Until then, the honest statement is that ownership’s atomicity is assumed and Raft’s consensus is proved, and the two do not yet touch.

The Raft rows (C1 onward) are in the Reference’s Raft section.

Next: SWIM, which does not try to agree on anything.

SWIM: membership by merge

Ownership and Raft both spend a majority round trip to get one authoritative answer. SWIM does not try to agree on anything. Every node keeps its own view of who else is alive, the views disagree constantly, and the only promise is that disagreements resolve rather than compound.

That is a different kind of promise, bought a different way: by an algebraic property of a merge rule, not by quorum intersection and not by structure.

The record and the rule

A member record is an incarnation number and a status: Alive, Suspect or Dead. Two records are compared by a key: a higher incarnation always wins, and at equal incarnations the more-dead status wins. merge keeps whichever side has the larger key. That is the entire rule.

A probe timeout or a self-refutation is not a different rule. Each is only a different choice of which record arrived:

• A probe that times out makes the node believe the peer Suspect, at the incarnation it had recorded when the probe began. The incarnation is an argument and is not re-read, because a probe is slow and a refutation can land while it is in flight. A suspicion at the old incarnation then loses to the refutation and changes nothing.
• A node that hears it is accused answers with a record one incarnation higher. Alive at a higher incarnation beats suspect and dead at the accusation’s.

What is proved

The claims are S1 to S14 in the Reference. In words:

Idempotence and absorbing a repeat are what let gossip’s real delivery model, at least once and arbitrarily duplicated, survive contact with merge at all. Commutativity and associativity are what make order not matter. S5 is what those add up to once lifted through every step of an execution: not that gossip arrives in order, or even that it arrives, only that whatever arrives never makes a view less accurate than it was.

What is not modelled

• No probe scheduler, no indirect-ping fallback, no dissemination budget. The model is the merge rule and one transition. How often to probe, and what to piggyback, is not modelled, so nothing here says gossip eventually arrives.
• No memberlist-style rejoin handshake. A graceful departure is Left, which out-ranks a failure verdict at the same incarnation. A member that comes back is an ordinary node that hears it is gone and refutes with a higher incarnation, exactly as after Dead. Memberlist gives a rejoin its own rules; here there are none.
• Nothing is forgotten. A departed or dead member’s record is kept, because it is what stops a stale report from reviving it, and it counts against the same bound on members. A cluster that churns through many identities will fill it.
• A node writes nothing down. Incarnations are self-correcting: a restarted node begins at 0, and the first peer to tell it what the cluster believes about it out-ranks its record and is answered with a higher incarnation. A restart costs a round trip, not correctness.

The service

Node is the shell around a verified table: the roster, the lock, the audit log, the batch limit and the order a batch is applied in are plain Rust that the tests exercise. Suspecting a peer, declaring it dead and refuting an accusation are not on the wire. They are things a node does about its own view, and putting them on the wire would let any caller make this node believe anything. A node suspects a peer because its own probe failed.

Who is in the cluster is the roster, and it can be closed or grow. Node::new builds a closed cluster: the members are the ones it was given, and a batch naming anyone else is refused. Node::admitting builds one that grows, with an admission policy, a function from a caller’s address to the member number that address may be. There is no join call. A join is the first ping or sync from an address the policy lets in; the sync reply is the whole table, so the newcomer learns who is there; and the others hear of it by gossip. The member number comes from the policy and the connection, never from the request. To leave, a node calls leave, which records it as Left and hands back that record to tell the peers. A node that is stopped without doing so is, to the cluster, a node that died, and the two are different records.

What this does not settle is who should be admitted. SWIM says nothing about that, and the example’s policy lets in every loopback address. Where a member lives is the deployment’s mapping from member number to address, not something SWIM gossips. A live member keeps one address; one that has left or died may come back from a different one, which replaces the old. And a cluster trusts its members: any one can fill the bound on members with made-up numbers.

How it relates to the rest

SWIM is independent of the other protocols in the proofs. It is related to them in one direction, and only as a hint:

• Ownership assumes failure detection is unreliable, and survives a revoke of a healthy node. SWIM’s Suspect and Dead are exactly that kind of signal.
• The actor system reads a SWIM view to decide where not to place new work and which addresses to stop returning. It never uses it to decide an actor has moved. That is the ownership epoch’s job.

The SWIM rows are in the Reference’s SWIM section.

Next: the actor, which sits on ownership.

HyParView: who to talk to

SWIM answers is each member up? by keeping a record and a verdict on every member. HyParView answers a different question, who should I talk to?, and keeps no table of the cluster to do it. A node holds two small sets:

• an active view, a handful of peers it gossips with. Links in it are meant to be two-sided: if a is in b’s active view, b is in a’s;
• a passive view, a larger reserve of nodes it has heard of and could promote when an active peer is lost.

Nothing here judges anyone alive or dead. A peer leaves the active view because a link closed or a slot was needed, not because it was suspected.

 Join(new) ──► contact adds `new` to its active view
              (demoting one peer to passive if full),
              and walks ForwardJoin(new, ttl) to its other active peers
 ForwardJoin ► at the end of the walk, adds `new` to active and asks it to reciprocate;
              before the end, passes the walk on, noting `new` in passive at ttl = prwl
 Disconnect ──► the peer leaves active and goes to passive
 Neighbor ────► the peer joins active (always granted, here)

What is built

This is the first piece, built the way SWIM was: one node’s views and the four handlers that maintain them, with the model, an executable table, and the proof that the table is the model. What the proofs say is a node’s views stay trustworthy under any message, in any order, any number of times: it is never its own peer, a peer is in one view and not both, and both views stay within their capacities. The paper leaves “drop a random peer” to the node; the model leaves it as a choice, so any way of choosing is correct, and the random choice is the caller’s.

What is not

No shuffle (which refreshes the passive view), no promotion on failure (which refills a vacated active slot), and nothing about several nodes together: symmetry of active views is the paper’s central property and is not claimed here, because the model is one node. The Reference has the rows and the full list.

Nothing consumes HyParView yet. It is written to sit beside SWIM behind the same membership::PeerSampling contract, so that a consumer can depend on the contract and not on either.

Next: the mailbox.

The actor: a journal fenced by ownership

A single-process actor is single-threaded by construction, so it never has to say what it guarantees. Spread over machines it does. The guarantees are the ones a single process gets for free: one thing at a time, each message once, in the order sent, and state that survives moving.

One decision

The actor’s state is not held by its host. It is a journal, the ordered sequence of messages the actor has accepted, and the state is a fold over it. Appending to the journal is the one thing a host does that matters, and it is fenced by ownership:

as_accept(host, epoch, message) requires  can_mutate(ownership, host, epoch)

can_mutate is Owned { host, epoch } and nothing else. A host that is not the owner, or owns a superseded generation, cannot append. The actor needs no second fence of its own: the journal write is the mutation the ownership protocol fences.

This is the actor’s relationship to ownership in one line, and it is why the actor’s exclusivity theorems are ownership’s, used as they are.

Everything else follows from three facts

1. Only the owner at the current epoch can append (ownership’s exclusivity and fencing).
2. An append is accepted only if the message’s sequence number is exactly the number already accepted from its sender. A duplicate and a message ahead of its turn are the same refusal.
3. The journal is only ever extended.

The network may delay, duplicate and reorder. The set of sent messages never shrinks, so a message can be offered to the host any number of times in any order. That is not a separate failure mode: it is what the accept guard is already quantified over.

What a handover does to the actor

Nothing, to the state. The new owner does not receive the state from the old one. It reads the same journal and recomputes. The journal records which host accepted each entry and under which epoch, but neither is needed to compute the state.

That is why the claims split cleanly:

The message

A message is an envelope: who sent it, the sender’s number for it, and a body of bytes. The actor’s behaviour folds over the body’s bytes, because a call to another actor is a request encoded for it. The sender’s counter is a u64, so Send is enabled only while it is below u64::MAX: the model’s numbers are the machine’s, and a sender that has used them all is refused rather than wrapped, because a wrapped counter would repeat a number and the accept guard would take the repeat for a duplicate.

The caller numbers its own messages. A retry after a lost reply is therefore the same (sender, seq) and not a second message. The host refuses an envelope naming anyone but the connection’s caller, a reused number with a different body, a number out of turn, and a body over the wire’s limit.

Direction, not built. The settled direction is that an envelope carries the receiver’s id as well as the sender’s, so that one connection can carry several actors. Today the envelope has no receiver, and the other calls (poll, acquire, accept, state, journal) name no actor either. Numbering would then be per (sender, receiver) pair. See the actor system.

What is not claimed

• Safety only. Nothing says a message is ever delivered, or that a sender retries. An out-of-order arrival is refused, not buffered, so something must retry in order for anything to progress. That something is the mailbox.
• The journal is assumed durable and linear. The model has no crash that loses an accepted entry, and the service’s journal is in memory: the guarantees hold for the life of the process and not across its death.
• The service refines crash-free executions only, for the reason the composed service does.
• The behaviour is a pure fold. What a message does beyond changing the state, an effect or a reply, is not modelled, and neither is what an effect does if its host is fenced halfway through.

The proof files are exclusive, delivery, state, refinement and scenario under src/actor/proofs/, all resting on one inductive invariant of six clauses. The rows are in the Reference’s actor section.

Next: the mailbox.

The mailbox: getting messages to the actor

The actor proves nothing about a message ever being offered to its host. The mailbox is the queue that would offer it, and it is where the lost-wakeup problem lives.

The problem

A drain that is scheduled rather than polling must be woken by the sender that finds it asleep. Every sender checks, then acts, with other senders and the drain acting in between. Get the interleaving wrong and a message sits in the queue with nobody coming to take it.

The machine

The protocol is the one in Apple’s swift-distributed-actors mailbox, which keeps it as a PlusCal/TLA+ model, with the same three flags (has, processing, scheduled) and the same step boundaries:

• A sender takes three steps: enqueue; read-and-set has; schedule, if has was clear and the drain is not running.
• The drain takes three: claim (clear has, mark running); take the queue; finish (stay scheduled exactly when has was set meanwhile).

The TLA+ model fixes two senders, five messages each, and a drain that stops after ten, so a model checker can exhaust it. Here a sender is an operation tracked in the mailbox’s state rather than a process, so any number of senders each sending any number of messages are covered at once. The bound is what the proof removes.

Two kinds of claim

Safety is a corollary of one invariant: nothing is lost or reordered, each message is taken in once, one sender’s messages keep their order with no gaps, and the drain never presents a message ahead of its turn (MB1–MB5).

The last of those is the link to the actor. The ith message processed is numbered the count of its sender’s messages among the i before it, word for word the guard of the actor’s accept. So a host accepting in this order is never refused for being early. The mailbox hands the actor an ordered stream, and the ownership fence that decides whether the actor may append it is the actor’s, unchanged.

Liveness is a different kind of claim, and the proof says so. It is a statement about the infinite run, it is false of the bare machine (a run in which the drain is never given a turn processes nothing), and so it is stated under a fairness assumption written down as a definition, not left implicit:

In every run in which the drain’s three steps and each sender’s two remaining ones are not starved, a message on the queue is later processed. (MB6)

Senders are not required to send. The fairness is weak fairness and nothing stronger, and it is an assumption about the scheduler that the protocol cannot enforce. Two runs keep the theorem honest: a fair run that does work and satisfies the theorem (MB8), and an unfair run in which a message is enqueued and never processed (MB9), which shows the assumption is necessary.

The temporal logic the liveness proof is stated in (leads-to, weak fairness, the WF1 rule) is rebuilt in the crate, not depended on, because the verified build links vstd and nothing else. Every rule is proved, not assumed (MB7).

What runs

The queue and flags the runtime keeps behind its lock are a verified core (MailboxCore), with one method per step and each method’s contract the model’s step (MB10, MB11). Everything around it is plain Rust that the tests exercise:

• the lock, the capacity and permits, the wakers and the notification;
• requeue, which puts back what a dropped round never handed out, and is not a model step;
• the claim that callers follow the sender’s three steps, which MB10 takes as a hypothesis and nothing checks.

Where it is, and is not, in front of an actor

The mailbox is proved in front of the model. In the running system:

• Host, the journal service, is not behind it. The owning node calls accept.
• A hosted service is: the supervisor puts a mailbox in front of any service it runs and serves it one request at a time, in each sender’s order. That is the services chapter.
• Subscriptions are not served through the mailbox, and the reply path is not bounded.

Next: Services over Jetstream.

Services over Jetstream

Each protocol also has a service that runs it over Jetstream RPC. The service calls the verified step functions; it does not re-derive them. This chapter is about what a service adds around a protocol, and the pieces that let several of them share a node.

The shape every service has

• The decision is a verified function; the service is the part around it. Who is calling, what a message carries, the lock, the audit log, the batch limit. The steps (steps_v.rs, exec_v.rs) are verified; the service files are plain Rust that Verus never sees, and the tests exercise them.
• Identity comes from the connection, never from an argument. No method takes the acting node’s number. The caller is the transport’s Context. This turns a whole class of “the message lied about who sent it” from a guarded-against bug into an unrepresentable one.
• Today that identity is an address against a roster, and an address is not a credential. The roster is fixed at construction everywhere except SWIM, whose node can also be built to admit new addresses by a policy (see SWIM). The shape survives replacing it with a TLS or key identity.
• One gate across a decision. A decision that reads the registry and then writes the journal holds one lock across both. Two locks taken one after the other would leave the gap that fencing exists to close.

Fencing a running actor

The actor’s journal write is fenced by ownership. A running service needs the same fence at the other end: a host that has lost the actor must stop acting for it.

Fence is the question “may this host still act for its actor?”. The intended answer is the ownership registry’s own may_write(host, epoch), which turns false the moment the epoch moves on, whether the owner handed the actor over or had it taken. Any Fn() -> bool is a fence.

serve_fenced asks it before each request:

• A request the fence refuses is answered FENCED and is never handled.
• A handler that is already running is finished, not cancelled.
• Delivery is at least once. A caller that gets FENCED may have had an earlier request run.

This is tested, not proved. The fence itself, the ownership check, is the proved part. What is checked here is that the loop around it does what its documentation says.

The supervisor

A Supervisor owns what runs on this node. LocalSupervisor hosts any number of actors, each as a service behind its own mailbox:

Three properties worth knowing:

• spawn requires a fence. An actor with no way to be told it has lost the actor is not something this node will host.
• A restart over Stopped or Retired reuses the same mailbox when the protocol matches. A session obtained before still works, and queued requests are not stranded.
• transport returns a session onto the mailbox, a Box<dyn ClientTransport<P>>, so a caller builds an ordinary generated channel and cannot tell a local actor from any other.

Draining

drain is a cooperative stop. It closes the actor’s fence, waits for the running handler to finish, drops the service, and returns. The mailbox is kept, with a small task answering every request FENCED, so a session made before the drain is told rather than left waiting.

Two details that came from review and are worth keeping in mind:

• Retirement is raced against waiting for work and nothing else, so it can never cancel a handler. It is also checked once more between rounds, because the mailbox is polled first and a backlog would otherwise starve a ready retire signal for ever.
• A handler that panics while the actor drains makes it Stopped, and drain reports an error instead of claiming a release that did not happen.

Not here

• Nothing decides when to drain. The mechanism exists; the policy does not.
• The retrying caller. A FENCED answer means “ask where the actor lives now”. No caller yet asks discovery again and retries.
• Tying the fence to a registry, host and epoch. The fence is a closure the caller supplies; nothing here constructs it from the ownership registry.

Next: Where things run.

Where things run: placement and discovery

Two questions about location, and they are different questions:

Discovery may be stale and nothing depends on its being right. A request that reaches a host that no longer owns the actor is answered FENCED by the fence in the services chapter, and the ownership epoch is what makes that answer true. Discovery is an optimisation of where to look, not a source of safety.

Discovery

Discovery has an associated Resource (what is being asked about) and Location (what comes back), and one async method:

discover(what: Resource) -> Result<Vec<Location>, DiscoveryError>

Two implementations exist, and they answer at different scopes:

• LocalSupervisor answers for its own node only. It is asked about an ActorRef and returns its own host id if the actor is Running. A draining, retired, stopped or absent actor is NotFound, which means “not here”, not “nowhere”.
• QuicDirectory answers with a URL, from a record of which host each placed actor was put on. See the actor system.

Placement

Placement takes a resource and returns the hosts that should run it. The one scheduler is the LAVA scheduler:

• It is the placement, scoring and ordering of the LAVA paper: placement (§4.3), NILAS scoring (§4.2) and LARS ordering (§4.4).
• Time is caller-supplied, monotonic. Exits are explicit events. A predicted expiry never removes a job.
• It knows hosts, their capacity and whether each is schedulable. It places a job, can migrate one, and can begin draining a host once an approval gate covers every job on it.
• A host can be made unschedulable without removing it. That is what the actor system does for a host membership suspects.

Around it, in the same area:

• CRUSH placement, behind its own feature because it is a dependency of its own. It is a stub.
• Prequal is not placement of actors; it picks which replica gets a request, by asking a few replicas how they are doing and sending to the one that looks best now. It is a pure decision: no sockets, no clock, no thread.
• Monitoring holds the Vivaldi network coordinates and a node’s published, numbered resources. This book does not go into it.

Evidence

All of this is plain Rust, not verified. The scheduling code is compiled into the dependency-free build, but none of it is under Verus; the tests are the evidence. Of this area, only Id and IdSet carry proofs. This chapter makes no claim of the kind the protocol chapters do, and the protocols do not depend on placement being correct: a badly placed actor is slow or unavailable, never doubly owned.

Next: the actor system.

The actor system over QUIC

ActorSystem is what puts the previous chapters in order for a caller who wants to talk to an actor and does not care where it is.

Four things in one trait

An actor system has:

• a supervisor, which says what runs here and hands out a transport onto a local actor’s mailbox;
• a discovery, which says where an actor lives, as locations;
• a placement, which decides which host should run something new;
• a dial, which opens a transport to a location. This is the one part that is specific to a transport.

connect is the one thing the trait adds, and the order it asks in is not the implementer’s to re-decide:

1. If the supervisor says the actor is Running here, hand out a session onto its mailbox. A local actor needs no network and no lookup.
2. Otherwise ask discovery, take the first location, and dial it.

What comes back is a Box<dyn ClientTransport<P>>, the same thing the supervisor returns, so the caller builds an ordinary generated channel on it and cannot tell a local actor from a remote one.

The QUIC system

QuicActorSystem dials over QUIC:

• one connection per location, opened on first use and reused while it is alive; a closed one is dropped and replaced;
• each dial opens a bidirectional stream on that connection, which is the lane;
• a name can resolve to several addresses, so each is tried in order and the last failure reported;
• a handshake timeout, because QUIC is over UDP and an address nobody listens on is not refused.

QuicActor is a handle that forwards the actor protocol over whichever transport connect found. It is tested over a real QUIC handshake on loopback.

Placement feeds discovery

QuicDirectory is both the placement and the discovery. It holds three things: each host’s address, the host each placed actor was put on, and the scheduler.

• add_host(id, capacity, url) registers a host with the scheduler and its address together, so a host that can be chosen can be reached.
• place asks the scheduler, then records the chosen host for the job’s actor. A job’s id is the actor’s. If the scheduler chose a host with no address, the job is taken back out and the placement is refused.
• discover answers from that record, looking the address up by host.

The record is a cache of the placement and is not kept in step with it. An actor that has exited or moved stays where it was put until placed again, and a caller that goes to the old address is answered FENCED.

Membership as a hint

SWIM tells the directory which hosts look gone:

A host is made placeable again only if the directory is what made it unplaceable, so a host drained for a migration is not switched back on by a rumour that it is alive. Each step is idempotent, so reading the same view twice changes nothing the second time.

Nothing moves an actor. The jobs of a host that left come back for the caller to place again or not. Placing them again starts a second copy if the host was only partitioned. What keeps that from corrupting anything is the ownership epoch, which only one of the two copies holds. That is ownership, not this.

What is not here

• One actor service per host. A dial reaches the actor service a host serves. Nothing on the lane says which actor. The settled direction is that an envelope carries the receiver’s id as well as the sender’s, so one connection can carry several actors; the other calls (poll, acquire, accept, state, journal) name no actor yet either. That is not built.
• Nobody drives the membership view on a timer, and the SWIM node has no change notification, so the view is polled.
• SWIM’s roster is keyed by address, so mapping a SWIM node to a host here relies on both using the same Id for a host.
• The Iroh system is entirely commented out.
• No automatic failover, and no retrying caller that re-asks discovery on FENCED.

Evidence

Plain Rust, tested, not proved. The tests include a real QUIC handshake, the placement path, every membership step including that a drained host stays drained, and one run against a real SWIM node that follows it from suspect to dead to refuted.

Usage examples

Five small programs, each runnable, each asserting what it shows. The code on this page is included from the files themselves when the book is built, so it cannot drift from what compiles: cargo test builds every example, and CI runs them.

cargo run --example ownership_handover
cargo run --example swim_membership
cargo run --example swim_node
cargo run --example actor_hosting
cargo run --example actor_basic

They are ordered the way the book is: the base first, then what sits on it. Each example is about using a piece, so for why it is shaped that way read the chapter named above it.

Handing an actor from one node to another

Chapter: Ownership.

A owns an actor at epoch 41 and writes. A agrees to hand it to B, which burns the epoch at once, so A’s next write at 41 is refused FENCED. B takes the actor at 42.

Things to notice:

• No call names the acting node. Who is calling is the Context, which a transport fills in. Here it is built by hand (from) because there is no network; over a real connection nothing else changes.
• The refusal comes from the registry, not from A. A still believes it holds 41.
• The floor. MemoryFloor::at(40) seeds the durable record of the highest epoch used, which is what keeps a restart from rewinding the actor.

//! The headline story, in process: a handover that fences the outgoing owner.
//!
//! `A` owns an actor at epoch 41 and writes. `A` agrees to hand it to `B`, which burns
//! the epoch at once. `A`, not yet knowing, writes again at 41 and is **fenced**. `B`
//! takes the actor at 42 and writes.
//!
//! That one refusal is what the protocol exists for. The registry is called directly
//! here, with no network, so the example is the shortest possible account of it. Over a
//! real connection nothing changes except where the caller's identity comes from:
//! [`Context::remote`] is filled in by the transport, never taken from an argument, and
//! the registry maps that address to a node through a roster fixed at construction.
//!
//! Run it with `cargo run --example ownership_handover`.

use std::collections::HashMap;
use std::net::{IpAddr, Ipv4Addr};
use std::sync::Arc;

use jetstream::prelude::jetstream_rpc::context::{Context, RemoteAddr};
use jetstream::prelude::*;
use jetstream_distributed::id::Id;
use jetstream_distributed::ownership::service::{MemoryFloor, Offer, Ownership, Registry};

const ADDR_A: IpAddr = IpAddr::V4(Ipv4Addr::new(10, 0, 0, 1));
const ADDR_B: IpAddr = IpAddr::V4(Ipv4Addr::new(10, 0, 0, 2));
const A: Id = Id(0);
const B: Id = Id(1);

/// The context a call from `addr` carries: what a transport would fill in.
fn from(addr: IpAddr) -> Context {
    Context::new(Some(RemoteAddr::IpAddr(addr)), None)
}

#[tokio::main]
async fn main() -> Result<()> {
    // Who is which node, by address, and where the epochs start. The floor is a
    // durable record of the highest epoch the registry has used, which is what keeps
    // a restart from rewinding the actor; seeding it at 40 makes the first epoch 41.
    let roster = HashMap::from([(ADDR_A, A), (ADDR_B, B)]);
    let registry = Registry::new(roster, A, Arc::new(MemoryFloor::at(40)))?;

    // The actor is offered to A at 41, and A takes it and writes.
    assert_eq!(registry.poll(from(ADDR_A)).await?, Offer::Grant(41));
    registry.acquire(from(ADDR_A), 41).await?;
    assert_eq!(registry.write(from(ADDR_A), 41).await?, 1);
    println!("A owns the actor at epoch 41 and wrote");

    // A agrees to hand it to B. The epoch is burned from this moment, so A is already
    // fenced out, whether or not it has been told.
    registry.begin_transfer(from(ADDR_A), B).await?;

    // The refusal this protocol exists for. A still believes it holds epoch 41; the
    // registry knows better, and says so in its own word.
    let fenced = registry.write(from(ADDR_A), 41).await.unwrap_err();
    assert_eq!(fenced.code(), Some("FENCED"));
    println!("A's write at the burned epoch 41 was refused: FENCED");

    // A is told to stop, and acknowledges at the transfer's epoch.
    assert_eq!(registry.poll(from(ADDR_A)).await?, Offer::Revoke(42));
    registry.release(from(ADDR_A), 42).await?;

    // Only now is the actor on offer to B, at the new epoch.
    assert_eq!(registry.poll(from(ADDR_B)).await?, Offer::Grant(42));
    registry.acquire(from(ADDR_B), 42).await?;
    assert_eq!(registry.write(from(ADDR_B), 42).await?, 2);
    println!("B took the actor at epoch 42 and wrote");

    // The audit log is what the test oracles read, and it records the refusal.
    for event in registry.log() {
        println!("  {event:?}");
    }
    Ok(())
}

A node’s view of a failure

Chapter: SWIM.

A node suspects a peer because its own probe failed, then declares it dead when the suspicion times out. A weaker report cannot undo that; a higher incarnation can, which is how a peer refutes an accusation.

Things to notice:

• suspect and declare_dead are methods on the node and not on the wire. What arrives from outside is a batch of Updates, merged by apply.
• The incarnation is an argument. It is the one the node had when the probe began, so a refutation that lands mid-probe cannot be accused after the fact.
• Applying a message twice changes nothing, which is the property that lets gossip be delivered at least once and in any order.

//! A SWIM node's view of a failure, and of being wrongly accused.
//!
//! A [`Node`] keeps one record per member: an incarnation number and a status. Two
//! records are compared by a key, a higher incarnation always winning and, at equal
//! incarnations, the more-dead status winning. Everything below is that one rule
//! applied to whichever record arrived.
//!
//! Suspecting a peer and declaring it dead are things a node does about *its own* view,
//! because its own probe failed, so they are methods on the node and not on the wire.
//! What does arrive from outside is a batch of [`Update`]s, merged by [`Node::apply`].
//!
//! Run it with `cargo run --example swim_membership`.

use std::collections::HashMap;
use std::net::{IpAddr, Ipv4Addr};

use jetstream_distributed::id::Id;
use jetstream_distributed::swim::service::{Liveness, Node, Update};

const ME: Id = Id(1);
const PEER: Id = Id(2);

fn main() -> Result<(), Box<dyn std::error::Error>> {
    // Who is a member, by address. A node off the roster cannot be built.
    let roster = HashMap::from([
        (IpAddr::V4(Ipv4Addr::new(10, 0, 0, 1)), ME),
        (IpAddr::V4(Ipv4Addr::new(10, 0, 0, 2)), PEER),
    ]);
    let node = Node::new(roster, ME)?;

    // Everyone starts alive at incarnation 0. Nothing is read from disk.
    assert_eq!(
        node.record(PEER),
        Some(Update {
            node: PEER,
            incarnation: 0,
            status: Liveness::Alive
        })
    );

    // A probe of the peer failed: believe it suspect, at the incarnation the node had
    // recorded when the probe began. That is an argument and not re-read, because a
    // probe is slow and a refutation can land while it is in flight.
    assert!(node.suspect(PEER, 0)?);
    println!("peer is suspect: {:?}", node.record(PEER).unwrap().status);

    // The suspicion timed out. This only takes effect if the peer is still suspect at
    // the incarnation the timer was started for.
    assert!(node.declare_dead(PEER, 0)?);
    println!("peer is dead:    {:?}", node.record(PEER).unwrap().status);

    // A weaker report does not undo a death: alive at the same incarnation loses.
    node.apply(&[Update {
        node: PEER,
        incarnation: 0,
        status: Liveness::Alive,
    }])?;
    assert_eq!(node.record(PEER).unwrap().status, Liveness::Dead);

    // Only a higher incarnation does. This is the refutation the peer makes when it
    // hears it is accused: alive at one incarnation above the accusation.
    node.apply(&[Update {
        node: PEER,
        incarnation: 1,
        status: Liveness::Alive,
    }])?;
    let record = node.record(PEER).unwrap();
    assert_eq!((record.incarnation, record.status), (1, Liveness::Alive));
    println!(
        "peer refuted:    incarnation {} {:?}",
        record.incarnation, record.status
    );

    // Applying the same message twice changes nothing the second time, which is what
    // lets gossip survive being delivered at least once and in any order.
    let again = [Update {
        node: PEER,
        incarnation: 1,
        status: Liveness::Alive,
    }];
    node.apply(&again)?;
    node.apply(&again)?;
    assert_eq!(node.record(PEER).unwrap().incarnation, 1);
    Ok(())
}

A SWIM cluster that members join and leave

Chapter: SWIM.

The previous example calls the node’s methods by hand. This one is the loop around it: a listener that serves ping and sync, a join through a seed, a probe that pings one peer a second and piggybacks its whole view, a suspicion when a ping fails, a timer that turns an unrefuted suspicion into death, and a way to leave. Run three of them; the second and third join through a seed:

cargo run --example swim_node -- run 1
cargo run --example swim_node -- run 2 1
cargo run --example swim_node -- run 3 2

Type leave in one terminal and the others record a departure, not a failure. Press Ctrl-C in another and they suspect it, then declare it dead. Start it again and it comes back at incarnation 1: its first caller tells it the cluster has it as gone, that out-ranks its record, and it answers with a higher incarnation. With no arguments the example does all of that in one process and asserts it, which is what CI runs.

Things to notice:

• A join is a sync with a seed. There is no join call. The seed’s admission policy lets the address in, its reply is the whole table, and the others hear of the newcomer by gossip. Node 3 above never calls node 1 to join.
• Who may join is a policy, and this example’s is open. Every loopback address 127.0.0.1 to 127.0.0.250 is a member. A real deployment writes a stricter one; SWIM does not say who should be admitted. The member number comes from the policy and the connection, never from the request.
• Leaving and dying are different records. leave writes Left, which out-ranks a failure verdict at the same incarnation, so a suspicion timer already running cannot turn a departure into a death. A node that is stopped without leaving is simply dead.
• The timing is this file’s choice and nothing is proved about it. The merge rule, the departure’s precedence, the refutation and the refusal of strangers are the verified and tested parts. When to probe, whom, and how long to wait are plain Rust.
• No indirect ping, and members are never forgotten: a departed member’s record is kept, and counts against the bound on members.
• Identity is the connection’s source address. Each member binds 127.0.0.<id> and connects from it. That works on Linux; on another OS give each member its own host. An address is not a credential, and where a member lives is the deployment’s mapping, not something SWIM gossips.

//! A SWIM node you can run as a process, in a cluster that members join and leave.
//!
//! [`Node`] is a table that obeys the merge rule and answers its peers; it has no
//! clock and no socket. What turns it into a member of a cluster is the part this
//! file writes, in plain Rust that Verus never sees and that nothing here proves:
//!
//! * **join**: start knowing only yourself, and `sync` with a seed. The seed's
//!   admission policy lets your address in as a member, and its reply is the whole
//!   cluster. The seed tells the others by gossip; you never call them to join;
//! * **serve**: accept a connection, hand it to the generated `MembershipService`;
//! * **probe**: every period, `ping` one peer, piggybacking this node's whole view;
//! * **suspect**: a ping that fails or times out makes the node believe the peer
//!   suspect, at the incarnation it had recorded *when the probe began*;
//! * **declare dead**: a suspicion that is not refuted within its timeout becomes
//!   death, but only if the peer is still suspect at that incarnation;
//! * **leave**: record yourself `Left` and tell every peer. A node that is stopped
//!   without doing so is, to the cluster, a node that died.
//!
//! The merge rule, the departure's precedence over a failure verdict, the
//! refutation and the refusal of strangers are the verified and tested parts.
//! *When* to probe, whom, and how long to wait are this file's choices, and
//! `crate::swim::model` says nothing about timing. There is no indirect ping
//! (`ping_req`): a peer that this node alone cannot reach is suspected on this
//! node's word.
//!
//! **Who may join is a policy, and this example's is open**: `127.0.0.<k>` for
//! `k` in `1..=250` is member `k`, and anyone who can reach a seed from such an
//! address is in. A real deployment writes a stricter one. Members are addressed
//! by loopback address because a node knows its caller by address; each listens
//! on port 9100 of its own address and connects from it. That works on Linux,
//! where all of `127.0.0.0/8` is loopback; elsewhere, give each member its own
//! host instead.
//!
//! Run a cluster in three terminals; the second and third join through a seed:
//!
//! ```text
//! cargo run --example swim_node -- run 1
//! cargo run --example swim_node -- run 2 1
//! cargo run --example swim_node -- run 3 2
//! ```
//!
//! Type `leave` in one to see the others record a departure. Press Ctrl-C in
//! another to see them suspect it and declare it dead. Start it again and watch it
//! be told what it was and outrank that. With no arguments the example does all of
//! that inside one process and asserts it: `cargo run --example swim_node`.

use std::collections::HashMap;
use std::net::{IpAddr, Ipv4Addr, SocketAddr};
use std::time::{Duration, Instant};

use jetstream::prelude::jetstream_rpc::session::{Session, SingleLaneSession};
use jetstream::prelude::*;
use jetstream_distributed::id::Id;
use jetstream_distributed::swim::service::{
    Admission, Liveness, Membership, Node, Update,
    membership_protocol::{MembershipChannel, MembershipService},
};
use tokio::net::{TcpListener, TcpSocket};
use tokio::task::JoinHandle;

const PORT: u16 = 9100;

/// The timings. Nothing proved depends on them.
#[derive(Clone, Copy)]
struct Timing {
    /// How often this node pings one peer.
    probe_every: Duration,
    /// How long a call may take before the peer is suspected.
    probe_timeout: Duration,
    /// How long a suspicion stands before it becomes death.
    suspicion: Duration,
}

const LIVE: Timing = Timing {
    probe_every: Duration::from_secs(1),
    probe_timeout: Duration::from_millis(500),
    suspicion: Duration::from_secs(5),
};

const FAST: Timing = Timing {
    probe_every: Duration::from_millis(40),
    probe_timeout: Duration::from_millis(100),
    suspicion: Duration::from_millis(200),
};

fn addr_of(member: u128) -> IpAddr {
    IpAddr::V4(Ipv4Addr::new(127, 0, 0, member as u8))
}

/// Who may join: this example lets in any loopback address `127.0.0.1` to
/// `127.0.0.250`, as the member with that last number.
fn policy() -> Admission {
    std::sync::Arc::new(|a| match a {
        IpAddr::V4(v4) => match v4.octets() {
            [127, 0, 0, k @ 1..=250] => Some(Id(k as u128)),
            _ => None,
        },
        IpAddr::V6(_) => None,
    })
}

/// Answer pings and syncs on `127.0.0.<me>:9100` for as long as the task lives.
async fn serve(node: Node, me: u128) -> std::io::Result<()> {
    let listener = TcpListener::bind(SocketAddr::new(addr_of(me), PORT)).await?;
    loop {
        let (stream, _) = listener.accept().await?;
        let node = node.clone();
        tokio::spawn(async move {
            // The session reads the peer's address off the stream, and `Node`
            // admits or refuses it: that is where "who is calling" comes from.
            let session = SingleLaneSession::<MembershipChannel, _, _>::service_io(stream);
            let Ok(lane) = Session::<MembershipChannel>::accept_lane(&session).await else {
                return;
            };
            let mut service = MembershipService { inner: node };
            let _ = jetstream_rpc::server::run(&mut service, lane).await;
        });
    }
}

#[derive(Clone, Copy)]
enum Call {
    /// SWIM's ping, with the view piggybacked.
    Ping,
    /// Push/pull: send the view, get the peer's whole table back. How a node joins.
    Sync,
}

/// One call to `peer`, made from this member's own address, carrying `view`.
async fn call(
    me: u128,
    peer: u128,
    kind: Call,
    view: Vec<Update>,
    within: Duration,
) -> Result<Vec<Update>> {
    let call = async {
        // Bind the source so the peer sees `127.0.0.<me>` and applies its policy to it.
        let socket = TcpSocket::new_v4()?;
        socket.bind(SocketAddr::new(addr_of(me), 0))?;
        let stream = socket.connect(SocketAddr::new(addr_of(peer), PORT)).await?;
        // The session owns the lane's I/O, so it outlives the channel.
        let session = SingleLaneSession::<MembershipChannel, _, _>::client_io(stream);
        let lane = Session::<MembershipChannel>::open_lane(&session).await?;
        let channel = MembershipChannel::new(64, Box::new(lane));
        channel.negotiate_version(u32::MAX).await?;
        match kind {
            Call::Ping => channel.ping(Context::default(), view).await,
            Call::Sync => channel.sync(Context::default(), view).await,
        }
    };
    match tokio::time::timeout(within, call).await {
        Ok(reply) => reply,
        Err(_) => Err(std::io::Error::new(std::io::ErrorKind::TimedOut, "call timed out").into()),
    }
}

/// The members this node would probe: everyone it has heard of except itself and
/// those that left. A member declared dead is still probed, because it may come back.
fn peers(node: &Node, me: u128) -> Vec<u128> {
    node.view()
        .into_iter()
        .filter(|u| u.node.0 != me && u.status != Liveness::Left)
        .map(|u| u.node.0)
        .collect()
}

/// Join through `seed`, then probe whoever the cluster turns out to hold, forever.
async fn probe(node: Node, me: u128, seed: Option<u128>, timing: Timing, verbose: bool) {
    // A join is a sync with the seed; its reply is the cluster. The seed may not be
    // up yet, so keep asking.
    if let Some(seed) = seed {
        loop {
            match call(me, seed, Call::Sync, node.view(), timing.probe_timeout).await {
                Ok(table) => {
                    if let Err(e) = node.apply(&table) {
                        eprintln!("[{me}] refused the seed's table: {e}");
                    }
                    break;
                }
                Err(e) => {
                    if verbose {
                        eprintln!("[{me}] cannot reach seed {seed} yet ({e})");
                    }
                    tokio::time::sleep(timing.probe_every).await;
                }
            }
        }
    }
    let mut seen = node.log().len();
    let mut turn = 0usize;
    loop {
        tokio::time::sleep(timing.probe_every).await;
        let peers = peers(&node, me);
        if peers.is_empty() {
            continue;
        }
        let peer = peers[turn % peers.len()];
        turn += 1;
        // The incarnation this node holds *now*, before the ping: a refutation
        // may land while the ping is in flight, and the accusation must not
        // outlive it.
        let held = node.record(Id(peer)).expect("a member").incarnation;
        match call(me, peer, Call::Ping, node.view(), timing.probe_timeout).await {
            // The ack is the peer's own word about everyone the ping mentioned,
            // including itself: the evidence that it is up.
            Ok(ack) => {
                if let Err(e) = node.apply(&ack) {
                    eprintln!("[{me}] refused a reply from {peer}: {e}");
                }
            }
            Err(e) => {
                if node.suspect(Id(peer), held).unwrap_or(false) && verbose {
                    eprintln!("[{me}] ping to {peer} failed ({e}); suspecting it");
                }
                let node = node.clone();
                tokio::spawn(async move {
                    tokio::time::sleep(timing.suspicion).await;
                    // A no-op unless the peer is still suspect at `held`.
                    let _ = node.declare_dead(Id(peer), held);
                });
            }
        }
        if verbose {
            let log = node.log();
            for event in &log[seen..] {
                eprintln!("[{me}] {event:?}");
            }
            seen = log.len();
        }
    }
}

/// Start member `me`: a fresh node that knows only itself, serving and probing,
/// and joining through `seed` if there is one.
fn start(
    me: u128,
    seed: Option<u128>,
    timing: Timing,
    verbose: bool,
) -> (Node, Vec<JoinHandle<()>>) {
    // A node starts at incarnation 0 and keeps nothing on disk. A restart is
    // corrected by the first peer that tells it what the cluster thinks of it.
    let node = Node::admitting(HashMap::from([(addr_of(me), Id(me))]), Id(me), policy())
        .expect("on its own roster");
    let server = {
        let node = node.clone();
        tokio::spawn(async move {
            if let Err(e) = serve(node, me).await {
                eprintln!("[{me}] cannot serve on 127.0.0.{me}:{PORT}: {e}");
            }
        })
    };
    let prober = tokio::spawn(probe(node.clone(), me, seed, timing, verbose));
    (node, vec![server, prober])
}

/// Leave: record the departure and tell every peer this node knows of.
async fn leave(node: &Node, me: u128, timing: Timing) {
    let said = node.leave();
    for peer in peers(node, me) {
        // A peer that cannot be reached is told by gossip from one that can.
        let _ = call(me, peer, Call::Ping, vec![said], timing.probe_timeout).await;
    }
}

fn status(node: &Node, of: u128) -> Option<Liveness> {
    node.record(Id(of)).map(|u| u.status)
}

async fn until(what: &str, mut ready: impl FnMut() -> bool) {
    let deadline = Instant::now() + Duration::from_secs(10);
    while !ready() {
        assert!(Instant::now() < deadline, "timed out waiting for {what}");
        tokio::time::sleep(Duration::from_millis(20)).await;
    }
}

fn stop(tasks: &[JoinHandle<()>]) {
    for task in tasks {
        task.abort();
    }
}

/// Members join through different seeds, one leaves, one is stopped, and the
/// one that left comes back.
async fn demonstrate() {
    // 1 starts alone; 2 joins through 1; 3 joins through 2, whose reply is how 3
    // learns of 1. 1 learns of 3 by gossip from 2.
    let (n1, _t1) = start(1, None, FAST, false);
    let (n2, t2) = start(2, Some(1), FAST, false);
    let (n3, t3) = start(3, Some(2), FAST, false);
    until("every member to know every other, alive", || {
        [(&n1, 2), (&n1, 3), (&n2, 3), (&n3, 1)]
            .iter()
            .all(|(n, of)| status(n, *of) == Some(Liveness::Alive))
    })
    .await;
    println!("three members joined through two seeds, and all know each other");

    // 3 leaves, and says so. The others record a departure, not a failure.
    leave(&n3, 3, FAST).await;
    until("1 and 2 to record 3 as having left", || {
        status(&n1, 3) == Some(Liveness::Left) && status(&n2, 3) == Some(Liveness::Left)
    })
    .await;
    stop(&t3);
    // A suspicion that was already running for 3 would have no effect: wait it out.
    tokio::time::sleep(FAST.suspicion * 2).await;
    assert_eq!(status(&n1, 3), Some(Liveness::Left), "left, and not dead");
    println!("member 3 left: members 1 and 2 recorded a departure, not a failure");

    // 2 is stopped without leaving. To the cluster that is a failure.
    stop(&t2);
    until("1 to declare 2 dead", || {
        status(&n1, 2) == Some(Liveness::Dead)
    })
    .await;
    println!("member 2 stopped without leaving: member 1 declared it dead");

    // 3 starts again, as a new process would: incarnation 0, no memory. It joins
    // through 1, which holds it as having left, and says so in its reply; that
    // out-ranks 3's own record, so 3 answers with a higher incarnation.
    let (n3, _t3) = start(3, Some(1), FAST, false);
    until("1 to see 3 alive again", || {
        status(&n1, 3) == Some(Liveness::Alive)
    })
    .await;
    let back = n1.record(Id(3)).unwrap();
    assert!(back.incarnation >= 1, "back only at a higher incarnation");
    assert!(n3.record(Id(3)).unwrap().incarnation >= 1);
    println!(
        "member 3 rejoined: alive again at incarnation {}",
        back.incarnation
    );
}

#[tokio::main(flavor = "current_thread")]
async fn main() {
    let args: Vec<String> = std::env::args().skip(1).collect();
    let args: Vec<&str> = args.iter().map(String::as_str).collect();
    let (me, seed) = match args[..] {
        [] => return demonstrate().await,
        ["run", me] => (me, None),
        ["run", me, seed] => (me, Some(seed)),
        _ => {
            eprintln!("usage: swim_node [run <id> [<seed id>]]");
            std::process::exit(2);
        }
    };
    let me: u128 = me.parse().expect("a member number");
    let seed: Option<u128> = seed.map(|s| s.parse().expect("a member number"));
    assert!((1..=250).contains(&me), "1 <= id <= 250");

    let (node, tasks) = start(me, seed, LIVE, true);
    eprintln!("[{me}] member {me} on 127.0.0.{me}:{PORT}; type `leave` to leave");

    // Typing `leave` leaves. A closed stdin does nothing: only a person saying so
    // is a departure.
    let (told, mut leaving) = tokio::sync::oneshot::channel::<()>();
    std::thread::spawn(move || {
        let mut line = String::new();
        while std::io::stdin().read_line(&mut line).is_ok_and(|n| n > 0) {
            if line.trim() == "leave" {
                let _ = told.send(());
                return;
            }
            line.clear();
        }
    });

    let mut shown = Vec::new();
    loop {
        tokio::select! {
            _ = tokio::time::sleep(LIVE.probe_every * 2) => {}
            Ok(()) = &mut leaving => {
                leave(&node, me, LIVE).await;
                eprintln!("[{me}] left, and told the cluster");
                return;
            }
        }
        let view = node.view();
        if view != shown {
            let line: Vec<String> = view
                .iter()
                .map(|u| format!("{}:{:?}@{}", u.node.0, u.status, u.incarnation))
                .collect();
            println!("[{me}] view: {}", line.join(" "));
            shown = view;
        }
        if tasks.iter().any(|t| t.is_finished()) {
            std::process::exit(1);
        }
    }
}

Hosting an actor under a fence

Chapters: Services over Jetstream and the actor.

A supervisor hosts an ordinary service behind a mailbox. The fence is the question “may this host still act for its actor?”. When it closes, the next request is answered FENCED without reaching the actor. Draining then drops the service and leaves the mailbox answering.

Things to notice:

• The actor is a plain trait implementation. It has no idea it has a mailbox, a fence or a supervisor.
• spawn requires a fence. There is no way to host an actor that cannot be told it lost.
• The caller gets an ordinary generated channel. It cannot tell a local actor from a remote one.
• In a deployment the fence is the ownership registry’s may_write(host, epoch). That wiring is not built; the example uses a flag in its place.

//! Hosting an actor under a fence, calling it, and draining it.
//!
//! A [`LocalSupervisor`] hosts actors on one node, each behind its own mailbox. The
//! actor is an ordinary service; it is handed a [`Fence`](jetstream_distributed::actor::service::Fence), which is the question "may
//! this host still act for its actor?". In a deployment the fence is the ownership
//! registry's `may_write(host, epoch)`. Here it is a flag, so the example can close it.
//!
//! What it shows, in order: an actor is hosted and called; the fence closes and the
//! next request is refused `FENCED` without reaching the actor; the actor is drained
//! and its service dropped; and discovery stops pointing at it.
//!
//! Run it with `cargo run --example actor_hosting`.

use std::num::NonZeroU32;
use std::sync::Arc;
use std::sync::atomic::{AtomicBool, AtomicU64, Ordering};

use jetstream::prelude::*;
use jetstream_distributed::actor::service::{
    ActorRef, Capacity, LocalSupervisor, Status, Supervisor,
};
use jetstream_distributed::id::Id;
use jetstream_distributed::scheduling::discovery::{Discovery, DiscoveryError};

use counter_protocol::{CounterChannel, CounterService};

/// How many requests the actor's mailbox holds before a sender has to wait.
const ROOM: Capacity = Capacity::Bounded(NonZeroU32::new(16).unwrap());

/// This node, and the actor it hosts. Both are plain [`Id`]s.
const ME: Id = Id(1);
const COUNTER: Id = Id(42);

#[service]
trait Counter {
    /// How many calls the counter has handled, counting this one.
    async fn next(&self, ctx: Context) -> Result<u64>;
}

#[derive(Default)]
struct CounterImpl(AtomicU64);

impl Counter for CounterImpl {
    async fn next(&self, _ctx: Context) -> Result<u64> {
        Ok(self.0.fetch_add(1, Ordering::SeqCst) + 1)
    }
}

#[tokio::main]
async fn main() -> Result<()> {
    let supervisor = LocalSupervisor::new(ME);

    // The fence starts open. Anything `Fn() -> bool` is a fence.
    let owner = Arc::new(AtomicBool::new(true));
    let fence = {
        let owner = owner.clone();
        move || owner.load(Ordering::SeqCst)
    };

    // Host the actor. `spawn` requires a fence: a host with no way to be told it
    // lost the actor is not something the supervisor will run.
    supervisor
        .spawn::<CounterChannel, _, _>(
            COUNTER,
            ROOM,
            CounterService {
                inner: CounterImpl::default(),
            },
            fence,
        )
        .await?;
    assert_eq!(supervisor.status(COUNTER), Status::Running);

    // Call it. A transport onto the actor's mailbox becomes an ordinary generated
    // channel, so the caller cannot tell it from a remote one.
    let transport = supervisor
        .transport::<CounterChannel>(COUNTER, Context::default())
        .await?;
    let counter = CounterChannel::new(64, transport);
    counter.negotiate_version(u32::MAX).await?;
    assert_eq!(counter.next(Context::default()).await?, 1);
    assert_eq!(counter.next(Context::default()).await?, 2);
    println!("hosted and called: the counter is at 2");

    // Discovery, asked about this actor, names this node.
    assert_eq!(supervisor.discover(ActorRef(COUNTER)).await, Ok(vec![ME]));

    // The actor's epoch moves on: ownership passed to another host. The fence
    // closes, and the next request is refused without reaching the actor.
    owner.store(false, Ordering::SeqCst);
    let refused = counter.next(Context::default()).await.unwrap_err();
    assert_eq!(refused.code(), Some("FENCED"));
    println!("fence closed: the next call was answered FENCED");

    // Drain it. A handler that was running would be finished, not cancelled; here
    // there is none. The service is dropped and the mailbox stays, answering FENCED.
    supervisor.drain(COUNTER).await?;
    assert_eq!(supervisor.status(COUNTER), Status::Retired);
    assert_eq!(
        supervisor.discover(ActorRef(COUNTER)).await,
        Err(DiscoveryError::NotFound),
        "a retired actor is not where a caller should go"
    );
    println!("drained: the actor is retired and no longer discoverable here");
    Ok(())
}

Two actors, one calling the other

Chapter: The mailbox.

A holds a channel to B and calls it. A is generic over what B is, so it cannot tell a mailbox from anything else that speaks the protocol.

//! Two actors, each behind its own mailbox.
//!
//! `ActorAImpl` calls `ActorB` as `self.b.b(ctx).await`. The `B` it holds is a
//! generated channel whose transport is a [`Session`] on `B`'s mailbox, and `B`'s
//! implementation is served from the other end by [`serve`], one request at a
//! time. `ActorAImpl` is generic over `B: ActorB` and cannot tell. `main` reaches
//! `A` the same way, through `A`'s mailbox.

use std::num::NonZeroU32;

use jetstream::prelude::*;
use jetstream_distributed::actor::service::{Capacity, Delivery, Mailbox, Session, serve};

use actora_protocol::{ActorAChannel, ActorAService};
use actorb_protocol::{ActorBChannel, ActorBService};

/// How many messages each mailbox holds before a sender has to wait. Always the
/// caller's to say.
const MAILBOX: Capacity = Capacity::Bounded(NonZeroU32::new(16).unwrap());

#[service]
trait ActorA {
    async fn a(&self, ctx: Context) -> Result<()>;
}

#[service]
trait ActorB {
    async fn b(&self, ctx: Context) -> Result<()>;
}

struct ActorAImpl<B> {
    b: B,
}

impl<B> ActorA for ActorAImpl<B>
where
    B: ActorB + Send + Sync,
{
    async fn a(&self, ctx: Context) -> Result<()> {
        eprintln!("A: calling B");
        self.b.b(ctx).await?;
        eprintln!("A: B answered");
        Ok(())
    }
}

struct ActorBImpl;

impl ActorB for ActorBImpl {
    async fn b(&self, _ctx: Context) -> Result<()> {
        eprintln!("B: handling a call");
        Ok(())
    }
}

#[tokio::main]
async fn main() -> Result<()> {
    // B, behind its mailbox.
    let b_mailbox = Mailbox::<Delivery<ActorBChannel>>::new(MAILBOX);
    let mut b = ActorBService { inner: ActorBImpl };
    tokio::spawn({
        let mailbox = b_mailbox.clone();
        async move { serve(mailbox, &mut b).await }
    });
    let b_channel = ActorBChannel::new(64, Box::new(Session::new(b_mailbox, Context::default())));
    b_channel.negotiate_version(u32::MAX).await?;

    // A, holding a channel to B, behind its own mailbox.
    let a_mailbox = Mailbox::<Delivery<ActorAChannel>>::new(MAILBOX);
    let mut a = ActorAService {
        inner: ActorAImpl { b: b_channel },
    };
    tokio::spawn({
        let mailbox = a_mailbox.clone();
        async move { serve(mailbox, &mut a).await }
    });
    let a_channel = ActorAChannel::new(64, Box::new(Session::new(a_mailbox, Context::default())));
    a_channel.negotiate_version(u32::MAX).await?;

    for _ in 0..2 {
        a_channel.a(Context::default()).await?;
    }
    Ok(())
}

Longer examples are the tests

The tests are real programs too, and a good deal longer. They are the better reading once the examples above make sense, because each one is a story with an expected ending:

They are plain Rust that Verus never sees. What they check is tested, not proved; see Evidence.

Ownership: the model and its claims

What this is, and what it is not

This repository does not claim that Rust’s borrow checker has been extended across machines. Nothing here is checked at compile time for your application code, no lifetime crosses a network link, and no &mut is transported anywhere.

What this is: a runtime protocol for moving exclusive write authority over an actor (named by an Id) between nodes, together with machine-checked proofs that the protocol’s exclusivity and fencing properties hold in every reachable state, including under crashes, partitions, duplicated messages and interrupted handovers.

The analogy to Rust is about the shape of the guarantee, not the mechanism. Rust’s &mut T is exclusive because the compiler refuses to create a second one. Here, authority is exclusive because may_mutate is only ever true in one shape - the actor is Owned, the caller is the owner, and the caller’s fencing epoch is exactly the actor’s current epoch - and because the protocol’s transitions provably keep it that way.

The core of this repository is a model, and the proofs are about the model. Each algorithm also has a service over Jetstream RPC, which runs the verified step functions; what those services do and do not claim is stated in The protocol as a Jetstream service and in each module’s docs.

Relation to Chubby

The obvious prior art is The Chubby lock service for loosely-coupled distributed systems (Burrows, OSDI 2006). It is worth being precise about the relationship, because the central mechanism here is Chubby’s, not a new one.

The fencing mechanism is the same idea. Chubby §2.4: a lock holder may request a sequencer, “an opaque byte-string that describes the state of the lock immediately after acquisition”, containing the lock name, the mode, and the lock generation number — a per-node counter that “increases when the node’s lock transitions from free to held”. The client passes it to the resource server, which “is expected to test whether the sequencer is still valid … if not, it should reject the request”. That is exactly Token { actor, epoch, holder } plus valid_fence, and Chubby’s lock generation number is this model’s Epoch. This repository is a formalisation of that design, not an alternative to it.

What this adds is the proof, and the precision that a proof forces. Chubby is an experience paper: it describes the initial design, compares it with actual use, and explains how the design had to change. It carries no machine-checked proofs, and it does not need to — its evidence is years of production at scale. The evidence here is different in kind. “The recipient server is expected to test whether the sequencer is still valid” is doing a great deal of work in that sentence, and writing the obligation down as a state machine is what turns it into something checkable:

• who may mutate is a single predicate, may_mutate, and theorem_no_authority_without_token proves that anyone who satisfies it provably holds an issued token for exactly that (actor, epoch);
• the headline scenario — A owns at 41, B takes over at 42, A returns still holding its epoch-41 token — is the situation sequencers exist for, and it is discharged as a nine-step execution rather than argued informally;
• the awkward part, a node cannot fence itself, becomes impossible to leave implicit. FenceGuard::accepts consults the node’s own belief, so a partitioned holder accepts its own stale epoch; the rejection that matters happens where the effect lands. Chubby’s locks are advisory for exactly this reason — “holding a lock called F neither is necessary to access the file F, nor prevents other clients from doing so” — and this model is advisory in the same sense, but has to say so in a proof obligation rather than in prose.

Three deliberate differences, and why.

The third difference is where this model has something Chubby does not, and it is also where it was recently found to be wrong. Because privilege moves between peers rather than being held centrally, a node can be left believing it holds the privilege after the privilege has moved. Chubby handles the corresponding case by checking a sequencer “against the server’s Chubby cache or … the most recent sequencer that the server has observed” — belief is checked against authority. This model originally had no such split on the routing side and resolved a seizure by editing the absent node’s state, which no implementation can do; see The holder graph is a tree and the believes_holds / has_token split in src/raymond/model_t.rs.

What Chubby has that this does not: a deployed system, sessions and KeepAlives, failover, caching with invalidations, a filesystem namespace, ACLs, events, and liveness of any kind. This model proves safety only, and says so.

The state machine

#![allow(unused)]
fn main() {
// Id is `crate::id::Id`, a newtype around a `u128` (a UUID or a ULID converts to one);
// a model names a host, and an actor, by it directly. (An actor was a `nat` here
// before; the theorems now quantify over the `u128` actors a host always was, not
// over unbounded ones. No theorem relied on there being more.)
pub type Epoch   = nat;

pub enum OwnershipState {
    Owned        { owner: Id, epoch: Epoch },
    Transferring { from: Id, to: Id, old_epoch: Epoch, new_epoch: Epoch },
    Unowned      { epoch: Epoch, intended_owner: Id },
}
}

Ownership never moves atomically. A handover is four protocol transitions:

Owned(A, 41)
      |  BeginTransfer(A -> B)         epoch 42 is allocated here
Transferring(A, B, 41, 42)
      |  CompleteRelease
Unowned(42, B)
      |  Acquire(B)
Owned(B, 42)

Two deliberate design points:

• The epoch advances at the start of a handover, not at the end. From the moment A agrees to transfer, current_epoch is 42, so A’s epoch-41 authority is already fenced out. A does not have to be reachable, or even alive, for this to take effect.
• During the two middle stages nobody has authority at all. That is the trade this design makes: it gives up availability during a handover so that double ownership is not representable. It is acceptable for neither node to have mutable authority during a transfer; it is never acceptable for both to.

The two specification functions

#![allow(unused)]
fn main() {
// Who may perform an authoritative mutation.
spec fn may_mutate(s: OwnershipState, node: Id, epoch: Epoch) -> bool {
    match s {
        Owned { owner, epoch: e } => node == owner && epoch == e,
        Transferring { .. }       => false,
        Unowned { .. }            => false,
    }
}

// The fence check a server performs on an incoming request.
spec fn valid_fence(s: OwnershipState, e: Epoch) -> bool { e >= current_epoch(s) }
}

current_epoch reports new_epoch while Transferring, which is what makes the outgoing owner stale immediately.

Capability tokens

A Token { actor, epoch, holder } is a physical artifact. It can be copied, it survives a crash, and a node that was partitioned away for an hour can come back still clutching one. The model reflects that: System::issued is the set of every token ever issued and it never shrinks.

Whether a token confers authority is a completely separate question, answered by token_authorized, which consults the actor’s current state. Stale physical tokens exist; they are inert.

Failure model

These are the assumptions the proofs rest on. They are part of the system model, not hidden side conditions.

What is not claimed: liveness. Nothing here says a transfer completes, that a request is eventually served, or that an actor ever becomes owned again. Under arbitrary crashes and partitions none of those are achievable anyway. Safety survives every case above; progress does not, and is treated separately.

Claimed invariants and the proofs that establish them

Every row names a proof fn that Verus checks in CI. If a row’s proof stops verifying, the build fails.

“Reachability” means the hypothesis reachable(sys), i.e. some finite execution starting from an init state ends in sys. It is discharged once and for all by theorem_reachable_inv.

Privilege movement is partitioned by cooperation

A holder that acts hands the privilege on (ComposedStep::PassToken, which requires pre.own.live.contains(n) and believes_holds); a holder that does not has it taken (ComposedStep::SeizeToken). composed::proofs::coupling::theorem_token_movement_is_partitioned proves there is no third way: routing steps, ownership transitions, acquisition and reconciliation all leave possession exactly as they found it.

The SeizeToken arm used to claim !pre.own.live.contains(m) as well, because seizure was guarded on it. It no longer is, and the arm now says only what is true and checkable: the privilege moved away from m without m taking a step. That is the distinction a deployment can act on — a coordinator knows whether it is forcing the transfer; it does not know whether the node is alive. See Seizure needs no oracle.

The liveness guard on PassToken stays, and means something different: it is not a detection requirement but a statement about who is acting. ray_assign_privilege models the holder choosing to hand the privilege to the head of its queue, and a crashed node cannot choose anything.

A seized node must reconcile before it returns

A seizure leaves the seized node’s holder and using entries exactly as they were — nobody can reach into a machine that is down — and Step::Recover’s contract says a node comes back with no knowledge of what happened meanwhile. So a node that is simply allowed to recover comes back still believing holder[n] == n, and can enter its Raymond critical section beside the new holder. Ownership stays safe, because the epoch fences it; Raymond’s critical section has no epoch.

So Composed carries seized, the set of nodes whose privilege was taken and whose belief has not yet been repaired, and composed_inv ties it to reality: every stale holder owes a reconciliation. cs_own refuses Step::Recover for a node in that set, and ComposedStep::Reconcile is the only way out.

The reconciliation a real deployment must perform — re-read the routing state rather than trust what you remember — is therefore a modelled transition with content, not a marker: it is the step in which the belief is dropped, the critical section left, and the holder pointer re-aimed at the node that actually holds the privilege. scenario_composed_crash_takeover runs it through to A rejoining afterwards, so the guard is a discipline rather than an unreachable restriction.

It is not guarded on the node being down. Seizure is no longer restricted to crashed nodes, so a live node can be left stale by a coordinator that suspected it wrongly, and must be able to learn the truth too. What the ordering rule still enforces is the crashed case: you cannot come back and start acting on a belief you never corrected.

Seizure needs no oracle: belief versus authority

An earlier version of this model guarded ComposedStep::SeizeToken on !pre.own.live.contains(from), with this argument: RevokeOwner may fire against a perfectly healthy owner, so without a liveness guard a seizure could fire against a live node inside its Raymond critical section; ray_seize clears using[from], so the model would report exclusivity while two nodes were really inside.

The analysis was right and the conclusion was wrong, twice over.

It conflated two guarantees. Ownership safety is fenced by the epoch, which is burned before the seizure fires, so it never needed the node to be dead. Only Raymond’s critical-section exclusivity needed anything, and what it needs is a condition on the state — ray_no_stale_holders — not a guard on the step. The difference matters: a state condition is something a deployment can restore, by reconciling; a step guard is something it must evaluate.

And !live is ground truth, which no coordinator has. It has a suspicion — which is exactly why RevokeOwner is modelled as firing against healthy nodes. Guarding the forcible path on perfect failure detection put the composed machine’s strongest theorems out of reach of any real deployment, in a clause that read like an ordinary guard.

The repair was the one the ownership layer had already made once. issued keeps a crashed node’s capability for ever and token_authorized decides whether it still confers anything; the routing layer now makes the same split:

ray_seize now touches only the new holder. from’s holder, using and asked entries are left exactly as they are, because they live on a machine nobody can reach — editing them was modelling something no implementation can do. What that creates is a stale holder: a node that believes it holds the privilege, does not, and may still be inside its critical section believing that too.

That state is the point. It could not previously be written down, because ray_unique_token was an inductive invariant over the holder pointers and the state violated it outright — the invariant held partly because the dangerous state was unrepresentable, which is the pattern the ownership layer takes such care to avoid. Uniqueness is now structural (privilege is one value), the stale state is representable, and theorem_stale_holder_confers_no_authority proves it inert: couples is written against possession, so belief confers nothing however firm it is.

The rule this leaves behind. Not all liveness guards are oracles, and the difference is which node the step makes act:

Liveness may guard the nodes a step makes act, and may not guard the ones it does not.

A guard on an acting node is a statement about who takes part — nobody has to determine anything, because if the node is down the exchange simply does not happen. A guard on a non-acting node is an oracle, because something must evaluate it before the step may fire. !live(from) was the second kind, which is why it had to go; live(n) on cs_pass_token was always the first kind.

Applying the rule uniformly closed two more holes of exactly the shape the review found, on the receiving side:

• cs_pass_token now guards head as well as n. ray_assign_privilege has head record holder[head] := head, so if head crashed after its request reached n, the old step installed a belief in a node that could not receive it — and a later Recover(head) framed it in, modelling the node as knowing about an event it never observed.
• cs_seize_token guards to for the same reason: the coordinator hands it the privilege and it records that, so it is acting.

The rule covers the ownership layer too, and enumerating it there found the last gap: tr_begin_transfer is documented as “the current owner agrees to hand actor over”, which is an action by from, and it had no liveness guard. So Acquire(A) → Crash(A) → BeginTransfer(A, B) was accepted — a crashed node volunteering. That one matters beyond tidiness: RevokeOwner and SeizeToken exist precisely for the case where the owner cannot cooperate, and a model in which the dead cooperate does not need them.

The full audit, by who acts:

That is all twelve variants of Step, which is the point: a table that omits one cannot support a coverage argument, however right the rows it does contain are. This one omitted ReassignUnowned and Stutter when first published.

RevokeOwner being unguarded is the design, not an oversight: it is the step that fires without the owner’s cooperation, against a node that may be perfectly healthy. ReassignUnowned is the same shape — the coordinator re-offering an actor that nobody owns, burning an epoch to do it.

cs_ray guards whichever node the Raymond step makes act (ray_step_actor), which is the carrier that has most of them. Without it a crashed node could queue requests, forward them, and — the serious case — enter its critical section: after Crash(A) → RevokeOwner → SeizeToken(A, B), Ray { EnterCs(A) } fired on A’s untouched holder and queue while A was still down and still marked, walking straight past the reconciliation-before-acting discipline. ReceiveRequest acts at at; from sent its request earlier and takes no part in the delivery.

cs_reconcile guards nobody, and that is not an exception to the rule but a consequence of what live means here. live is participating in the protocol, not powered on — the field’s documentation said “currently up” until this was chased down, which was a second meaning hiding in one set. Reconciliation is the boundary step — the node re-reading authoritative state as part of coming back, before it resumes participating — which is why it may fire while !live and why Recover is a separate step that follows it. A node that was seized while live may also reconcile at any time, since it is acting either way.

Granting the privilege discharges the debt. Both grant steps now clear the recipient from seized, because receiving the privilege is the node learning the truth: it is live, it records holder := itself, and it really does hold, so its belief is correct again. Without that, a node marked by an earlier seizure and later handed the privilege back would stop being stale while staying marked — and cs_reconcile requires is_stale_holder, so the marker could never be cleared and recovers_a_seized_node would reject that node’s recovery for ever.

That state became reachable only when the !live(from) guard came off. Before, a marked node was always dead and had to reconcile before rejoining, so it could never be a live grant target; afterwards it can be. A guard removed for good reasons opened a path that had to be closed somewhere else.

Three consequences worth stating plainly:

• cs_seize_token has no liveness guard at all. Ownership safety survives seizure from a node that is perfectly healthy and wrongly suspected, which is the case a deployment will actually hit.
• Raymond’s mutual exclusion has a window. Between a seizure and the seized node’s reconciliation, two nodes can be inside their critical sections. That is true of any system that takes a privilege away from a node it cannot reach, and the model now says so instead of hiding it.
• cs_reconcile acquired its content. It used to remove a marker and change nothing else; the work it claimed to model had already been done at seizure time, by the coordinator, to a node it could not talk to. Now it is where the belief is dropped — by the node that holds it.

Chubby reaches the same place from the other direction: a sequencer’s validity is checked “against the server’s Chubby cache or … the most recent sequencer that the server has observed”, which is belief checked against authority. See Relation to Chubby.

A node cannot fence itself

Row E is narrower than it looks, and the gap is worth stating plainly rather than leaving a reader to infer it.

FenceGuard::accepts consults the node’s own belief about the actor — whatever generation it last observed. A partitioned A still holding FenceGuard::new(A, 41) gets accepts(A, 41) == true while the system has already moved to Owned { B, 42 }. The stale owner from the headline scenario passes its own fence, every time.

That is not a contradiction: the postcondition promises may_mutate(self.view(), ..), and view() is exactly that stale belief. But the safety property proved here is about the system’s state (can_mutate(sys, ..)), and nothing in src/ownership/exec_v.rs connects a guard to it. What a guard buys is node-local staleness rejection, not fencing.

Real fencing has to happen where the effect lands, against authoritative state: the storage layer refusing a write whose epoch is superseded, or a reply gate that re-reads the ownership record after a write is durable and before acknowledging it, refusing the acknowledgement if the record no longer names this node at this epoch. That check is what turns exclusivity into a property an outsider can rely on. It is not in this crate, and proving the protocol says nothing about whether an implementation performs it.

The Raymond layer

src/raymond/model_t.rs models Raymond’s distributed mutual-exclusion algorithm as a routing layer, kept strictly separate from ownership semantics. Per node it tracks a holder pointer (that node’s belief about the next hop towards the privilege), a request queue, an asked flag (outstanding request) and using (inside the critical section). Alongside them, and deliberately not derived from them, is Raymond::privilege: the node that actually holds it.

That split is the routing counterpart of issued versus token_authorized in the ownership layer, and it is what lets a seizure take the privilege from a node without reaching into it. believes_holds(r, n) is belief, has_token(r, n) is authority, and is_stale_holder(r, n) is the gap — see Seizure needs no oracle.

Requests in flight are explicit state: Raymond::requests records every request ever sent as (originator, destination), never shrinks, and is not consumed by delivery — the same modelling choice the ownership layer makes for network. The destination is resolved at send time, which is what lets a request be delivered after the token has moved and the holder pointers it was routed against are gone. A guard phrased against the live holder[from] would instead drop such a request silently, so “arbitrary delay” would have been claimed but not modelled.

Requests travel hop-by-hop towards the token and the token travels back along the reverse of the request path:

request:  D -> B -> A -> C[token]
token:    C -> A -> B -> D

Routing and ownership are glued by one predicate:

#![allow(unused)]
fn main() {
spec fn couples(r: Raymond, s: OwnershipState) -> bool {
    forall|n: Id, e: Epoch| may_mutate(s, n, e) ==> has_token(r, n)
}
}

Note the direction: routing never grants authority, it only constrains who could possibly have it. Authority still comes exclusively from the ownership state and its epoch. That is why a routing step - including a duplicated or reordered request - cannot manufacture an owner: it does not touch holder at all, so it cannot even change who could be the owner.

On its own, though, couples is only a predicate: ray_assign_privilege never sees the ownership state, so nothing in the routing layer stops a token from moving out from under a node that still has authority. src/composed/model_t.rs closes that gap by defining a single state machine over both layers in which the synchronisation is a guard:

• PassToken may only fire while the actor is Unowned — ownership must be genuinely released before the token is allowed to move. (Transferring also satisfies !is_owned, so guarding on that weaker condition would let the token move while a handover was still in flight and the outgoing owner had not yet acknowledged the revoke.);
• AcquireUnderToken may only fire for a node that holds the token — authority cannot be taken by a node routing has not elected;
• Ray carries every Raymond step that does not move the token — request routing and critical-section entry/exit alike — and Own carries every ownership transition that does not create authority over the actor.

The Ray carrier is guarded on preserves_token, deliberately wider than is_routing_step: if it admitted only routing, no composed execution could ever enter a critical section, every composed-reachable state would keep using uniformly false, and the theorems below would cover only a degenerate fragment of the real behaviour. scenario_composed_critical_section rules that out the only way that really counts — by building an execution from composed_init that reaches a state with using set, rather than assuming the entry transition and checking it type-checks as a composed step.

couples is then an invariant of that machine rather than a side condition, which is what makes “token transfer preserves ownership safety” a claim about the system instead of a hypothetical.

Every composed theorem is of the form “every reachable composed state satisfies …”, and such statements are worthless if nothing interesting is reachable. Two executions close that off, both built from composed_init via lemma_composed_reachable_step:

• scenario_composed_handover — a complete handover driven through both layers at once, ending in a reachable state where B genuinely owns the actor at epoch 42 and holds the token, while A’s epoch-41 token is still issued and powerless;
• scenario_composed_critical_section — a reachable state in which a node is actually inside the critical section.

Raymond’s liveness (every request is eventually served) needs FIFO, reliable links and no crashes. None of those are assumed here and none of it is claimed.

Raft: the same statement, bought by counting

The failure-model table’s first row is the strongest assumption this repository makes — ownership records are updated atomically — and it says outright that a real deployment has to buy that from consensus, or from a store with compare-and-swap. src/raft/ is the first half of buying it.

Raft’s Election Safety is the exclusivity theorem with two words changed, and it is bought a completely different way:

ownership:  at most one authoritative owner per epoch, because a single
            atomic registry hands the epoch out
raft:       at most one leader per term, because any two quorums share a
            voter and a voter votes once per term

The difference is worth dwelling on, because it is the whole reason both are here. ownership::proofs::exclusivity is structural: may_mutate is true in exactly one shape, Owned { owner, epoch }, so two owners is not a state the model can represent, and all the work is in showing the transitions never reach a bad one. In raft::model nothing is structural. A Cluster can perfectly well hold two servers both believing they lead term 7 — that state is representable, and ruling it out is a counting argument over a set that no single participant can see. Side by side, the two say what a coordinator costs.

The argument is three sentences (C1–C3), and the interesting clause is the one that is not in it. inv_vote_implies_term (C4) says a cast vote is never ahead of its voter’s term, and without it the induction fails at the most ordinary step in the protocol: a server timing out into term t + 1 votes for itself there, and only this clause rules out an earlier vote of its own already sitting in that term.

The log, and the line between modelled and proved

The model has a log. tr_client_request stamps an entry with its leader’s term, tr_append_entries carries one entry under the consistency check and truncates whatever diverged, tr_advance_commit advances the commit point under figure 8’s restriction, and tr_grant_vote carries the lastLogIndex/lastLogTerm up-to-date comparison. All four are in raft_next, so every run of raft_reachable may use them and every theorem above holds across them.

C12–C19 are what follows from a single step — a leader only appends, a follower agrees before it accepts, an entry is copied rather than invented, a commit needs a majority of the committing leader’s own term. Log Matching is proved too (C26), and getting there needed something the model did not have.

Ruling out a second entry at the same (index, term) is a fact about the run’s history, not about any one state. At tr_client_request the leader appends at the end of its own log, and nothing in the state says no leader of that term ever appended at that index before.

So Cluster carries ghost fields — four of them now, and each exists because some question about the run has no answer in any single state. led, every (server, term) ever led; created, every entry any leader ever made, keyed by the slot naming it and recording its value and the term of the entry before it; committed (C44–C47), every entry any leader ever committed, because Server::commit is a count that retreats; and voted_with (C49–C50), every vote together with the voter’s log as it stood when the vote was cast, because tr_grant_vote’s guard compares against a log that has since moved on. created’s second component is what makes Log Matching an induction rather than a wish. That second component is what makes Log Matching an induction rather than a wish: two servers whose entries at an index carry the same term are reading the same slot, so they agree on the value and on the recorded predecessor, which is the same question one index down. Repeat to zero.

Two moments are worth pointing at. At tr_become_leader the freshness clause (C24) holds because a term being won now has never been led — that is C22, and the middle of its chain is a fact about a server that may have stepped down long ago, which is where the history earns its keep. And at tr_append_entries the record survives because the follower’s entry at prefix - 1 has the same term as the leader’s: that is the consistency check, already in the protocol since the log went in, and it turns out to be exactly the guard the proof wants rather than something added for it (C25).

The ghost state is not an escape hatch, and that is a theorem (C21): for any history whatsoever — all four records, not merely the two this section introduces — every step still fires from the same real state and lands in the same real state. A guard that read the history could not satisfy that. The fields are written and never read, which is what makes them auxiliary variables in the standard sense.

Leader Completeness is still not proved, and the sections that follow are the six pushes that narrowed the gap rather than six restatements of it. Read them in order: C39–C43 the ground it stands on, C44–C47 what was committed, C49–C50 what a vote was a judgement of, C51–C52 what the summary that vote judged was a summary of, C53–C54 why the entry was still there to be judged. By the end, State Machine Safety holds with one hypothesis (C46), all three of the induction’s steps are theorems about the same objects, and only the induction that assembles them is missing.

The fourth record is the last one. C51 needed no fifth, because the thing it wanted — the candidate’s log at the moment it asked — is recoverable from a field that was already there: messages never shrinks, so the network is a history variable too, and the link could be proved instead of recorded.

A follower here will still truncate entries it had committed, which is faithful Raft — the protection against that is supposed to come from the election restriction, and the election restriction is now half a theorem (C43) rather than an absence.

The ground that induction has to stand on (C39–C43)

src/raft/proofs/terms_v.rs is not that induction. It is the part of it that can be proved without any new ghost state, and each piece is a theorem rather than a step of a larger argument that only makes sense once the argument exists.

The one to read is C41. A follower that already agrees with the leader at index i keeps its entry at i — and the proof splits on where the leader is writing. If the leader writes at or below i, Log Matching says the two logs agree at that index too, so the conditional in appended_log fires and the follower’s log is not touched at all. If it writes above i, the truncation is above i. Either way the entry stays.

That is the first commit on this branch earning something it was not made for. The conditional truncation went in because an unconditional one described a step the service would not take; it turns out to be what makes this theorem true, and this theorem is what rules out a committed entry vanishing from a voter’s log between the commit and the next election. Under an unconditional truncation a duplicate AppendEntries for an early index deletes the entry, and the induction has no base.

C43 is the other half that is provable now: a voter holding any entry of term T refuses every candidate whose last term is below T, so the vote cannot be granted at all. With C40 that is one line, and it is exactly half of what Leader Completeness needs — a candidate cannot win on a log that is behind on terms.

What is still missing is the other case, and it is worth being precise about which one. When the candidate’s last term is at or above the voter’s, C43 says nothing: the candidate is not refused, and the committed entry has to be shown present in its log by a different argument — its own last entry was created by some leader of a term between the commit’s and this election’s, and a strong induction over terms says that leader already held the entry. Three things that argument needs and this repository does not have:

• a record of what was committed. commit is a count per server and says nothing about which entry a quorum once held.
• a record of the voter’s log at the moment of the vote, because tr_grant_vote compares against a log that has since moved on.
• the strong induction over terms itself — the part of Raft that took Verdi a person-scale Coq development.

C42 and C43 are the two lemmas that induction will call. The induction is not written, and nothing here pretends otherwise.

What was committed, as a fact that survives the state (C44–C47)

The first of those three missing pieces is now there. Cluster carries a third ghost field, committed, written at tr_advance_commit and never removed from, and src/raft/proofs/commit_v.rs is what it buys.

Why the state could not say it. Server::commit is a count on one server, and two things are wrong with it as the subject of a safety property. It says how much is committed, not what — and Leader Completeness is a claim about a particular entry at a particular index. And it retreats: C38 proves exactly when, and proves that when it does, a committed entry was deleted. After that retreat nothing anywhere in the state records that the entry was ever committed, so a theorem about committed entries has nothing left to quantify over in the one state where it matters most.

The ghost field is still not an escape hatch, and still as a theorem rather than a promise: C21’s theorem_history_does_not_gate_the_protocol now quantifies over all three histories, so for any created, led and committed whatsoever every step is available from the same real state and lands in the same real state.

The record is a recursion, not a comprehension, and the reason is worth recording because it is not a matter of taste. In the pinned vstd, Set is the finite set type — ISet is the unrestricted one — so Set::new(|k| ..) returns Option<Set<A>>, None when the predicate picks out infinitely many elements. The obvious comprehension would therefore have to discharge finiteness at every use. Built up one index at a time, committed_by is finite structurally, with nothing to discharge, and the price — membership is no longer syntactic — is paid once by lemma_committed_by_members.

C46 is the one to read, and it is worth being exact about what it does and does not say. State Machine Safety is “if two servers apply the entry at index i, they apply the same one”. C46 is that sentence with one hypothesis added: that the two commits agree on the entry’s term. So the whole of the remaining risk is concentrated into a single question — can two leaders commit entries of different terms at one index? — and that question is Leader Completeness.

See how little is left over. The value half is free: one (term, index) names one act of creation by one leader, which Election Safety (C13) and the creation record (C22) give unconditionally. Nothing about values, quorums or counting is missing. What is missing is the argument that a later leader’s log cannot carry a different term at an index a quorum has already agreed on, and that argument has three steps:

1. the leader of term T' won a quorum in T', and that quorum meets the commit-time quorum of C45 in some voter;
2. that voter still held the entry when it voted;
3. so the candidate’s log was at least as up to date as a log holding that entry, and C43 closes the case where its last term is behind.

Step 2 is conditional, and its condition is the induction itself — an earlier version of this section said step 2 was already a theorem, citing C42, and that was wrong in a way worth keeping on the record. C42 carries a hypothesis: the replicating leader must already agree with the voter at that index. Discharging that for every intervening leader is Leader Completeness at the intervening terms. C48 is the run-level form, and it puts the condition in the signature rather than in a paragraph, so it cannot be read as free-standing again.

So: step 1 is a theorem; step 2 is a theorem with a hypothesis the induction discharges; step 3 is half a theorem, because the case where the candidate’s last term is at or above the voter’s needs the induction hypothesis at the intermediate term.

All three records are now in place — and the induction still is not (C49–C50)

The third, Cluster::voted_with, records every vote with the voter’s log as it stood when the vote was cast and the candidate summary it was judged against. tr_grant_vote’s guard is a comparison at an instant, and by the time anything asks what it was, the voter’s log has moved on.

C49 promotes that guard from a side-condition on one transition to a fact about every reachable state, and adds the clause that makes quantifying over the record mean anything: every vote is on it, self-votes included. C50 spends it — quorum intersection that hands back not just a shared voter but what that voter saw.

It is worth being exact about why this is not the induction. Every theorem here is about one state. The induction relates a commit in term T to an election in a later term T', and it has to compare the quorum that held the entry at commit time with the quorum that voted at election time across the run between them — which is C48’s job, and C48’s hypothesis is discharged only by the induction hypothesis at the intervening terms.

So the materials are all here and the argument that assembles them is not. That is a smaller gap than it was three pushes ago, and it is still a gap.

So the materials are all here — they were not, and C52 is the one that was missing

That sentence stood for one push, and it was wrong in a way worth keeping rather than editing away, because it is the third time the same mistake has been made in this README and the first time it was found by reading the signatures instead of the prose.

C50 ends with at_least_as_up_to_date(ct, ci, lg). Read it: ct and ci are two numbers. They came off a RequestVote, and nothing in C50, or anywhere before it, said they had anything to do with the winner’s log. So the induction’s third step — the winner’s log dominates what the voter had — was not a theorem here; what was a theorem was the winner’s summary dominates what the voter had, and a summary is a pair of integers that arrived over the network. As far as the machine-checked content went, a candidate could have been elected on a summary it made up.

C51 closes it without a fifth ghost record. The first four exist because the state throws information away. This one does not need to, because messages never shrinks: the RequestVote the candidate sent is still there, carrying the summary, so the link is provable. Both writing transitions make the first clause true by construction — tr_timeout sends the message it records, and tr_grant_vote is guarded by the message whose summary it copies — and the second clause holds because nothing that can change a server’s log leaves it a candidate: tr_append_entries demotes its receiver and tr_client_request needs a leader.

The clause that looks like bookkeeping is the one doing the work. A RequestVote never names a term its sender has not reached is what makes the snapshot clause inductive, and the case it settles is tr_timeout itself: a server stepping up to t becomes a candidate of t, so every RequestVote for (t, n) on the wire now has to summarise its new log. The one it just sent does. An older one would not have to, and would sink the invariant — and there is none, because a server enters a term once. That last sentence is the whole of the third clause.

C52 is C50 restated about a log, at tr_become_leader — the last instant at which the winner is still a candidate, and so the last instant at which its summary is its log. Afterwards the log grows and the RequestVote is spent, which is faithful rather than a limitation.

What is still missing is the induction’s second step, unchanged: the voter has to have still held the entry when it voted, which is C48 and its hypothesis. The difference C52 makes is that when that lands there is now something for it to meet — a statement about the new leader’s log rather than about two integers.

The second step, and the difference between a translation and a paragraph (C53–C54)

The previous section ends “what is still missing is the induction’s second step, unchanged”. That is what C53 and C54 close, and the way they close it is the part worth reading.

C48 was never wrong; it was in the wrong language. It says an entry survives a run whenever every leader replicating to its holder already agrees with it there, and its hypothesis is a quantifier over steps. The induction hypothesis is a statement about leaders of terms: every leader of a term between the commit and the election holds the entry. Those are not the same sentence, and for two pushes this document bridged them with the words “C48’s hypothesis is discharged only by the induction hypothesis at the intervening terms” — which is true, and is a claim about a translation rather than a translation.

C53 is the translation, and it turns on a guard. tr_append_entries is the only transition that can shorten a log, and it requires the leader’s current_term to equal the follower’s. So if a server is known to be at term T or beyond, only a leader at T or beyond can write to it. And a member of a commit’s quorum is at T or beyond, because figure 8’s restriction says the last entry of the committed prefix carries the committing leader’s own term, the quorum member holds that prefix, and no entry’s term exceeds its holder’s.

That is three short steps, and the middle one is where the figure-8 guard earns something it is not usually credited with. It is normally explained as ruling out a specific counterexample — a leader committing an old entry on a bare majority. Here it is what makes “the quorum is at term T” true, and without that the reduction from steps to leaders does not exist.

C54 is C48 restated in the induction’s own words. replicators_hold is the tight form — every standing leader that could replicate to the holder right now — and it carries no term bound, because persistence does not need one; leaders_within_hold is what the induction supplies, Leader Completeness over the closed range [t0, t1]; and theorem_a_commit_quorum_still_holds_it composes that with the commit-time quorum. The hypothesis is still a hypothesis — an intervening leader that does not hold the entry will truncate it away, which is faithful Raft — but it is now the induction hypothesis rather than something a sentence asserts is equivalent to it.

The upper bound is there because the first version did not have it. @codex found that, and the finding is the most interesting thing in the push. Strong induction on the election’s term T supplies Leader Completeness for terms below T; a predicate reading “every standing leader of a term at or past t0” demands it for terms above T too. Those leaders exist — nothing in this model orders terms cluster-wide, since tr_grant_vote only requires the request’s term to be at least the voter’s own, so a leader of a far higher term can be running elsewhere while a delayed campaign at T is still collecting votes. They are harmless, because tr_append_entries needs equal terms and so they cannot reach a voter at a lower term. But the old predicate demanded they hold the entry anyway, and C54 could not have been discharged from the induction hypothesis without assuming Leader Completeness at terms the induction had not reached.

A hypothesis stronger than the argument needs is not a safe over-approximation when the hypothesis is what somebody else has to supply. That is the general form of the lesson, and it is the fourth time on this branch that the machine-checked content was fine and the claim about it was not.

Where the two bounds come from is asymmetric, and worth reading. The lower one is established at the window’s start — C53 puts the quorum at T or beyond, and terms never fall. The upper one is established at the window’s end: in the use the induction will make of this, the window closes when the voter grants its vote in term t1, and tr_grant_vote requires the request’s term to be at least the voter’s own, so the voter is at t1 or below then — and monotonicity carries it backwards over the whole window. The upper bound is not an extra assumption about the run; it is the vote.

And the t1 endpoint is an open obligation, stated in the theorem’s own docs rather than deferred to a paragraph: the range is closed, so the induction needs its case at t1 before it may use C54 at t1, and a leader of t1 can exist before this voter has voted in t1, because winning t1 needs a quorum and not this one. Either the induction establishes t1 first, or it restricts the window to end strictly before any leader of t1 exists. This push does not settle which.

So all three steps now speak about the same objects — an entry, an index, a term, a log:

1. a quorum held the entry at commit time (C45);
2. a member of that quorum still held it when it voted (C54, given Leader Completeness at the intervening terms);
3. the winner’s own log dominates that voter’s (C52).

What is left is a strong induction over terms and nothing else. That is a claim about shape, and it is worth being explicit that it is not a claim that the induction is proved. It is not. But the previous four sections each ended by naming a missing object — a record, a link, a translation — and this one does not: there is no missing object, only the argument.

C38 is what that gap costs, stated concretely. Because the model may not assume that state unreachable, it has to handle it, and handling it means a follower’s commit index can retreat — one Raft property given up to keep another. C38 confines the retreat to exactly the state Leader Completeness would rule out, so the gap has a boundary and a name rather than being a general caveat. Closing that proof closes this too.

There is no reconfiguration, deliberately: membership is fixed and no transition changes it. Joint consensus is a separate protocol with its own well-known unsafety, and modelling it half-way would be worse than not modelling it.

A log that truncates, on a device that cannot

Raft’s log shrinks. Figure 2’s rule 3 deletes a conflicting entry and everything after it, and appended_log is that rule. Every durable log worth trusting grows: vendor/verified-storage/pmemlog’s abstract state offers append and advance_head — put bytes on the end, or forget bytes from the front — and nothing that takes the tail back.

That is not a gap in the vendored crate. It is what makes a crash-consistent log cheap: an append that either happened or did not is one write, while a tail that moves backwards is a state the device has to be able to be caught in the middle of.

src/raft/store_v.rs reconciles them in four lines of idea:

1. the device holds a sequence of Records, and only ever grows;
2. a truncation is a record, Record::Truncate { len }, appended like any other;
3. the log is replay of the records, computed on recovery;
4. therefore the physical log is append-only and the logical log truncates.

C27–C31 are what that buys. The one to read first is C27, and it is worth reading for how boring its proof is: the recovery case of “memory agrees with the device” is discharged by the transition’s own definition, because store_recover defines the recovered log as replay of what survived. A design where recovery has to reconcile two sources is a design where that proof is the hard one. Here there is one source.

C29 is where the protocol and the storage layer turn out to want the same thing. Accepting a replicated entry costs two records when the entry at prefix conflicts, and zero when it does not — the no-conflict branch writes nothing at all. That branch exists because of C25: the conditional truncation is what keeps the creation record true, and it is what makes Log Matching provable. It is also, it turns out, what makes the common case — a duplicate or reordered AppendEntries, which under heartbeats is most of them — a read and no write. The check that makes the protocol safe is the check that makes the steady state free.

The commit point, and the one Raft property this model gives up

Raft’s commit index is monotone. This model’s is not, in exactly one case, and the case is worth understanding because it is the shape of what is still missing.

accepted_commit clamps the commit index to the length of the log. A follower with commit = 5 told to replace the entry at index 0 ends with a one-entry log, and something has to give: either its commit point still says 5 — naming four entries that no longer exist — or it retreats to 1. This model retreats. A commit point past the end of the log is a state no later reader can make sense of, since every query about what has been applied reads off the end; a commit point that went backwards is a broken promise, but a readable one, and the breach is visible rather than latent.

An earlier version of this comment claimed both “never backwards” and “never past the end of the log”, which cannot both hold. That was a review finding and it was correct.

What replaced it is C38, which says precisely when the retreat happens: commit is monotone whenever the truncation point is at or above it — every step of a healthy cluster — and when it retreats, the leader asked the follower to delete an entry it had committed. Not “commit might go backwards sometimes”, but “commit goes backwards only in the state whose unreachability is the missing theorem”.

That missing theorem is Leader Completeness. When it lands, C38’s hypothesis becomes vacuous and monotonicity becomes unconditional. Until then the model may not treat the case as unreachable — so it handles it, and says how.

The byte layer, and the theorem it exists for

C27–C31 are about records; pmemlog appends bytes. src/raft/wire_v.rs is the layer between, and it exists to make one statement provable.

C28 says a crash leaves a prefix of the records. A device leaves a prefix of the bytes, and a byte prefix can cut a record in half. Without a theorem joining the two, C28’s hypothesis is an assumption about how writes land wearing the clothes of a definition.

C32 is that theorem: for every k at all — not multiples of seventeen — parse(encode(rs).take(k)) == rs.take(k / 17). The tear may land in the middle of a u64. That is what the fixed width buys, and it is why the format is seventeen flat bytes rather than a length prefix or a varint: a log whose recovery depends on the parser being clever is a log whose recovery has a bug in it. There is no checksum here either, because pmemlog CRCs what it stores and a second one at this layer would add bytes and no guarantee.

The chain is then: a device keeps a byte prefix (C32) → that is a record prefix (C28) → replay of a record prefix is a log the store had (C27). No step asks the device for more than “you keep a prefix of what I wrote”.

The line a crash may not cross

C27 and C28 as first written said “a crash keeps a prefix” — which permits the empty prefix. After any completed append, a restart could discard every record the store had reported durable, including entries a leader committed on the strength of that acknowledgement. That is strictly weaker than the device underneath: pmemlog’s append shows a crash either the log before it or the log after it and nothing older. A layer whose whole job is to be no weaker than pmemlog was weaker than pmemlog, and no test caught it because every crash the suite simulates happens to be an honest one.

Store carries durable, and the model now separates what the device offers — store_write, one record on the device with the line unmoved, and store_sync, the only thing that moves it — from what a caller gets: store_append and store_truncate, durable before they return, which is what LogStore already promised in prose. theorem_an_append_is_a_write_then_a_sync is the proof that the promise is kept by the two primitives and not by a third thing the model invented.

C35 is the theorem that buys. Read the second clause: the line never retreats and everything below it is unchanged record for record. A store that kept the right number of records while rewriting one of them would satisfy the first and fail the second. And read the third statement in it, which is where this module meets Raft’s commit rule — a follower that answers Accepted has written the entry down, so a leader counting that answer toward a majority is counting something that cannot be taken back. Remove the durability hypothesis and the conclusion fails immediately; that is what it is there to show.

Compaction has a middle state

theorem_compaction_replays_the_same says replay(compacted(log)) == log, which is true and licenses nothing. It covers the case where the rewrite has already replaced what came before — the case that needs no proof. The procedure is two steps on an append-only device, write the new generation and then reclaim the old one, and a crash between them leaves old_records ++ compacted(log), which replays to log + log. Every entry twice.

compaction_batch is a leading Truncate { len: 0 } and then the log, and that marker is what makes the staged generation self-sufficient: it clears whatever preceded it, so the device replays to log with the old records still there and to log once they are gone. Both crash views agree, which is what turns the reclaim from a change into a no-op (C36).

It has to land atomically, and that is not a preference. A crash inside the batch leaves the marker — which has already cleared everything — plus a prefix of the log, so recovery produces a shorter log than the store had. C36b proves the rewind is exact: a crash after k of the batch’s entries recovers exactly k, because a partial batch is not arbitrary damage, it is the compaction of a shorter log. Data loss on an operation whose entire purpose is to change nothing.

So the batch is one store_write_batch: on pmemlog a single append, whose crash view is the log before it or the log after it and nothing between. That is the one property of the device this design asks for and cannot itself check, and it is the property pmemlog was built to have. RecordLogStore installs the batch in one step; a_batch_written_one_record_at_a_time_would_rewind_the_log walks every cut inside it and checks the real compact produces none of them.

This was a review finding and it was a bug in the code, not the model: the executable store appended the batch a record at a time under a doc comment saying it must not. The model had no word for “atomically”, which is why the two could drift with nothing to catch it — store_write_batch is that word.

Two limitations, stated rather than assumed away:

• The 64-bit boundary. Record’s fields are nat, because the model’s terms are unbounded and a model that caps them has an overflow bug the protocol does not. Bytes are not unbounded. records_fit is therefore a guard on the write transitions and a clause of the store invariant, not merely a precondition on C32 and C33 — stated only on the theorems it would filter which theorems may be invoked while leaving the unencodable state reachable, so the store half and the wire half could not be composed at all (C37). A cluster reaching term 2^64 now has a store that cannot advance, rather than one that silently writes the wrong record.
• The device grows even when the log does not, because nothing schedules compaction — closed. A follower thrashing between two leaders writes a record per round, and worth_compacting now fires at records > 2 * (entries + 1): amortised O(1), with the bound asserted every round over sixty rounds of the worst shape. C31 says the rewrite is sound; compact_if_worthwhile is what makes it happen.
• Nothing in src/ depends on vendor/verified-storage/pmemlog yet, and the reason is no longer “the executable layer does not exist” — replay_exec, encode_exec and parse_exec do. What is missing is a device, and the obstacle there is not an interface but a crash model: pmemlog’s persistence_chunk_size is 8 and a write must be safe for any subset of 8-byte chunks having flushed, which POSIX does not promise for a write crossing a chunk. An fsync-per-write file would not satisfy it. That needs a target platform — real PM, O_DIRECT with aligned single-sector writes, or an explicitly weaker documented device. Until one exists, pmemlog’s two corruption assumptions are not assumptions of anything proved here.

The consensus service

The election record is verified code; the log, the commit point and the shell are not (CE1–CE2). Peer keeps an exec::ElectionCore behind its lock — role, term, whom it voted for, and the votes it has counted — and stand_for_election, the vote handling in request_vote, step_down_to, yield_at and the tally in count_ballot all go through it, so each is the model’s step by contract and each refusal a step the model could not take. What is not proved: the log and the up-to-date comparison (an argument to the core), the commit point and replication progress (record_match and the figure-8 rule are plain Rust), the roster, the lock, the audit log, and the durable store — the core calls persist with the term and vote before it moves, and that order is the code’s, not a theorem.

src/raft/service.rs serves it: request_vote with the up-to-date comparison, append_entries with the consistency check and the truncation, heartbeat, standing. As in the ownership service, no method takes a server number — the candidate asking for a vote is whoever opened the connection — and that matters more here, because a protocol whose entire safety argument is “a server votes once per term” is exactly the one you do not want taking the voter’s or the candidate’s identity from a field. Standing for election, tallying, taking a term, appending a command and advancing the commit point are inherent methods rather than RPCs, for the reason force is inherent on the ownership registry: a peer that could trigger them could keep the cluster in a permanent election, or declare somebody’s entry committed.

The log itself is a trait, LogStore, with MemoryLogStore as the mock the tests run against. A real log is a file with a format, an fsync policy and a truncation story, none of which belongs in the protocol; the protocol’s own behaviour is exactly what you want to exercise without a disk in the way.

Replies are protocol steps too. Raft’s term rule is about “RPC request or response”, and a Ballot::Refused(2) reaching a term-1 candidate carries the same news as an inbound request would. count_ballot, observe_standing and observe_appended are that side of it, and they take the reply itself rather than a summary: there is no way into a candidate’s tally except by handing over a Ballot::Granted for the term being stood in. A method taking only (peer, term) would let a caller count a peer that refused — a majority assembled out of nothing, and a leader the model never elected.

And the same durability finding, arrived at from the other end. Raft’s own figure 2 requires currentTerm and votedFor on stable storage before responding to RPCs. That is the requirement the ownership registry’s epoch floor turned out to have, and it is load-bearing for the same reason: a server that grants a vote, replies, restarts having forgotten, and grants again has voted twice in one term — two candidates can then each hold a majority, and Election Safety is gone. Not because the proof is wrong, but because already_voted was reported false when the model’s has_voted was true. tests/raft_election.rs runs that in both directions: a restarted voter that refuses the second request, and a forgetful one that grants it and elects two leaders.

Actor: a journal fenced by ownership

An actor in a single process is single-threaded by construction, so it never has to say what it guarantees. Spread over machines it does, and the guarantees are exactly the ones a single process gets for free: one thing at a time, each message once, in the order sent, and state that survives moving.

src/actor/ proves those four, and it does so by one decision: the actor’s state is not held by its host. It is a journal — the ordered sequence of messages the actor has accepted — and the state is a fold over it (actor::model::state_of). Appending to the journal is the one thing a host does that matters, and it is fenced by the ownership protocol: as_accept requires ownership::spec::can_mutate at the epoch the host presents, which is Owned { host, epoch } and nothing else. A host that is not the owner, or owns a generation that has been superseded, cannot append. Nothing about the actor needs a second fence; the journal write is the mutation the ownership protocol fences.

Everything else follows from three facts: only the owner at the current epoch can append (the ownership layer’s exclusivity and fencing, used as-is); an append is accepted only if the message’s sequence number is exactly the number already accepted from its sender (so a duplicate and a message ahead of its turn are the same refusal); and the journal is only ever extended.

The network may delay, duplicate and reorder — ActorSystem::sent never shrinks, so a message can be offered to the host any number of times, in any order. None of that is a separate failure mode: it is what as_accept is already quantified over.

All of A5–A13 rest on one inductive invariant (actor::proofs::invariant::actor_inv) whose six clauses are the inductive forms of the guarantees: nothing invented, sequence numbers equal prior counts, epochs bounded by the actor’s current one, epochs ordered along the journal, one host per epoch, and — the clause that makes the last one provable — an entry written at the actor’s current epoch was written by its current owner. lemma_step_preserves_inv shows every step preserves it, and theorem_reachable_inv that it holds in every reachable state.

What this is not. It is a set of safety properties. Nothing says a message is ever delivered, or that a sender retries. An out-of-order arrival is refused, not buffered, so the sender (or a mailbox in front of the host) must retry in order for anything to make progress — the same line the other protocols here draw between safety and liveness. And the journal is assumed durable and linear: the model has no crash that loses an accepted entry, which is the actor’s counterpart of the atomic-registry assumption the ownership layer makes, and the service keeps the journal in memory (see The actor). Delivery to the host is the next section’s subject.

The mailbox, and the first liveness theorem

The paragraph above says the actor proves nothing about a message ever being offered to its host. src/actor/mailbox/ is the queue that would offer it, and it is where the lost-wakeup problem lives: a drain that is scheduled rather than polling must be woken by the sender that finds it asleep, and every sender checks, then acts, with other senders and the drain acting in between.

The machine is the protocol of Apple’s swift-distributed-actors mailbox, which keeps it as a PlusCal/TLA+ model (Models/mailbox.tla), with the same three flags (has, processing, scheduled) and the same step boundaries. A sender takes three steps — enqueue; read-and-set has; schedule if has was clear and the drain is not running — and the drain takes three — claim (clear has, mark running); take the queue; finish (stay scheduled exactly when has was set meanwhile). The TLA+ model fixes two senders, five messages each, and a drain that stops after ten, so a model checker can exhaust it. Here a sender is an operation tracked in Mailbox::ops rather than a process, so any number of senders each sending any number of messages are covered at once; the bound is what the proof removes.

Safety is a corollary of one invariant. Liveness is a different kind of claim, and the proof says so: it is a statement about the infinite run, it is false of the bare machine (a run in which the drain is never given a turn processes nothing), and so it is stated under a fairness assumption written down as a definition (mailbox_fair) rather than left implicit. The temporal logic it uses is src/temporal_t.rs, in the idiom of verus-tla (Anvil’s embedding of TLA in Verus) — executions as functions from step number to state, leads_to, weak fairness, and the WF1 rule — rebuilt in-crate rather than depended on, because verus --crate-type=lib src/lib.rs links vstd and nothing else. Every rule is proved, not assumed.

What this does not do. The model’s proofs are about the model, and MB10–MB11 connect the core to it. The protocol is run now — service::Mailbox wraps that core in a lock, and The mailbox as a transport says how it is used — but the lock, the capacity and permits, the wakers and the notification are plain Rust the tests exercise, and so is requeue, which puts back what a dropped round never handed out and is not a model step. Nothing checks that callers follow the sender’s three steps; MB10 takes it as a hypothesis. And Host does not sit behind it yet: Host keeps the sent set of the actor’s model and the owning node calls accept. The fairness assumption is weak fairness of those steps and nothing stronger, and it is an assumption about the scheduler, not something the protocol can enforce — a drain that is never run delivers nothing, which MB9 exhibits. And the mailbox hands the actor an ordered stream; the ownership fence that decides whether the actor may append it is the previous section’s, unchanged.

SWIM: gossip membership, bought by merge rather than majority

Ownership and Raft both spend a majority round-trip to get one authoritative answer. SWIM does not try to agree on anything: every node keeps its own view of who else is alive, those views disagree constantly, and the protocol’s only promise is that disagreements resolve rather than compound. That is a different kind of promise from Election Safety or exclusive ownership, and it is bought a different way — by an algebraic property of a merge rule, not by quorum intersection.

This is the first piece, not the whole protocol, in the same sense src/raft/model_t.rs was the first piece of Raft: the state space and one transition, proved correct on their own terms, with the probe timer, indirect-ping fallback and dissemination piggyback still to come. The piece chosen first is the one everything else depends on being right: state.go’s merge rule, the one function every gossip message, probe timeout and self-refutation in hashicorp/memberlist ultimately calls.

The record, and the rule for merging two of them

A MemberRecord is an incarnation number and a status — Alive, Suspect or Dead — and key_geq compares two of them: a higher incarnation always wins, and at equal incarnations the more-dead status wins. merge keeps whichever side has the larger key. That is the entire rule; tr_gossip is merge applied to whatever a peer’s own view already holds and whatever record just arrived, and a probe timeout or a self-refutation is only a different choice of which record arrived, not a different rule for applying it.

| S10 | The node’s table is the model. exec::SwimTable — what a node keeps — reads the model’s record_of (no entry is the fresh record), and learn writes merge of what is held and what arrived and changes nothing else; a table standing for a cluster that learns a record stands for the cluster tr_gossip leads to, and a fresh table stands for swim_init | swim::proofs::table::theorem_new_table_is_the_initial_cluster, theorem_learn_is_a_gossip_step | the table is well formed (each member once) | | S11 | Hearing an accusation about oneself is two gossip steps. SwimTable::hear merges the record and, if it was the node’s own that changed, merges the refutation on top of it; the model sees tr_gossip twice, and the table ends up believing the refutation. At the top of the incarnation space the second step is refused and the first has happened | swim::proofs::table::theorem_hearing_oneself_accused_is_two_gossip_steps | the table stands for the cluster | | S12 | A table never believes less than it did, and always stands for a reachable cluster. Whatever it learns, what it then holds for any member out-ranks or equals what it held; and a reachable cluster plus a learned record is a reachable cluster, so S5 is a statement about what the table holds | swim::proofs::table::theorem_learning_never_lowers_a_belief, theorem_a_table_stands_for_a_reachable_cluster_after_learning | the table stands for a reachable cluster | | S13 | A departure outlasts every report at or below its incarnation. Left ranks above Dead, so a suspicion timer that was already running, a late Dead verdict, or an old Alive cannot turn a node that announced its leaving into a failure or a recovery; merging any record at the same or an older incarnation into a Left record returns it unchanged. The one same-incarnation record that is itself Left is the same record, so repeating it changes nothing | swim::proofs::merge::theorem_a_departure_outlasts_every_report_at_or_below_it | none | | S14 | Only a higher incarnation brings a departed member back. The converse of S13 in the form a service uses: if hearing a record changed what a node believed about a member that had left, the record carried a higher incarnation. Not claimed: that only that member can produce one. In the crash-fault model it does, by refuting; the service believes any member’s word about any other, so a lying member can revive a departed one | swim::proofs::merge::theorem_only_a_higher_incarnation_revives_a_departure | none beyond S13 |

What S10–S14 do not cover. The table is a verified core, and Node is the shell around it: the roster and the admission policy (which numbers are members, who may speak and who may join), the lock, the audit log, the batch limit, and the order a batch is applied in are plain Rust that the tests exercise. The theorems are about one record at a time. In particular nothing proves that Node::leave writes the departure without answering it with a refutation: it does so by calling the table’s own learn rather than the path a received message takes, and tests/swim_dynamic.rs::a_node_does_not_refute_its_own_departure is what fails if that changes.

Joining and leaving. The model never assumed a fixed membership: a node absent from the view is exactly a node at the fresh record. What was fixed was the service’s roster. Node::new still builds that closed cluster. Node::admitting builds one that grows: a caller whose address is not yet known is put to an Admission policy, a function from the connection’s address to the member number that address may be, and is admitted if the policy names one and there is room. There is no join call: a join is the first ping or sync from an address the policy lets in, the sync reply is the whole table, and the others hear of the newcomer by gossip. The member number comes out of the policy and the connection, never out of the request. Node::leave records the node as Left at its held incarnation and returns that record for the caller to tell its peers. What this does not do: nothing decides who the policy should admit (the example’s admits every loopback address; a deployment writes its own); where a member lives is the deployment’s mapping from member number to address, not something SWIM gossips; members are never forgotten, so a departed member’s record is kept (it is what keeps S13 true) and counts against the same bound of MAX_UPDATES members, which any one member can fill by gossiping that many made-up numbers, so a cluster that admits a member admits its good behaviour; a live member is never given a second address, but one that has left or been declared dead may come back from a different address, which then replaces the old; a refused request admits nobody; the policy runs with the node’s lock held and must be quick; and a node that leaves and tells nobody is, to the cluster, a node that died.

S4 is worth pausing on, because the asymmetry it dismisses is real. key_geq(a, b) and key_geq(b, a) are different expressions, and reading merge’s definition — if key_geq(incoming, local) { incoming } else { local } — the incoming side breaks a tie. So merge(a, b) and merge(b, a) each hand a different call the tie-breaking advantage. What makes the theorem true anyway is status_rank’s injectivity: a MemberRecord is exactly its incarnation and its status, and if two records tie on key_geq — equal incarnation, equal rank — then by injectivity they have equal status too, so they were never two different records to begin with. lemma_rank_is_injective is a case split on the four enum variants; S4 is the only theorem in this module that spends it.

What the proofs are not is a claim that gossip converges in practice. Convergence needs every node’s view to eventually receive every update, which is a property of the dissemination schedule — how often a node piggybacks which records onto which probes — and that schedule is not modelled here at all. S5 is the half of the argument that has nothing to do with scheduling: whatever arrives, however late or however duplicated, can only move things forward. The other half — that something eventually arrives — is exactly the network-timing piece that is still future work.

The service

src/swim/service/ serves the protocol over Jetstream RPC: #[service] trait Membership with ping and sync, implemented by a Node whose table is written in exactly one place, by exec::SwimTable::hear — the verified table, whose merge is steps::merge_step (S10–S12).

Both methods do the same thing to the receiver — merge every Update in the message — and differ in the reply. ping answers with the receiver’s records for the members the message mentioned plus its own (SWIM’s ping/ack, with the dissemination riding on it); sync answers with the whole table (memberlist’s push/pull, the anti-entropy that repairs what a piggyback missed). As in the other two services, no method takes the sender’s number: who is calling is the Context, and an Update’s node field names the member being spoken about, which has to be content.

Suspecting, declaring dead and refuting are not on the wire, for the reason Raft’s stand_for_election is not on its: they are things a node does about its own view, and putting them in the trait would let any caller make this node believe anything. Node::suspect and Node::declare_dead are what the caller’s probe loop calls when a probe times out, and both take the incarnation the probe or timer began with — a refutation can land while either is running, and a timer that re-read the table would kill an incarnation nobody suspected; the refutation happens inside the merge, the moment the record that changed is the node’s own.

The node writes nothing down, and that is deliberate. Raft’s server and the ownership registry both keep a durable record because forgetting it breaks their safety. Incarnations are self-correcting: a node restarted at incarnation 0, whose peers remember it dead at 3, is told so by the first message that mentions it, and answers with 4 (a_restarted_node_is_told_what_it_was_and_outranks_it).

tests/swim_membership.rs delivers one set of updates in all 120 orders, with every message repeated, and checks the table is the same each time — S2, S4 and S6 exercised through the service rather than assumed of it. tests/swim_turmoil.rs runs SWIM’s own story across a simulated network: a node that cannot reach a peer suspects it, the partition heals, the suspicion reaches the suspected node, which is alive and refutes it, and the refutation comes back in the reply and clears the suspicion. tests/swim_dynamic.rs is the growing cluster: a join is a first call and the reply is the cluster, a stranger the policy refuses stays a stranger, a closed node still refuses to learn of members it was not built with, a second address cannot speak as an existing member, the cluster is bounded, a departure survives a late suspicion and a late Dead, a node does not refute its own departure but does refute one it did not announce, and a departed member returns at a higher incarnation. The same file’s wire test in tests/swim_turmoil.rs has a node join through a member that is not the first, the rest hear of it by gossip, and a departure arrive as one.

What the service does not have, and what it does not claim. A caller is identified by address, against the roster the node holds (fixed for Node::new, growing by policy for Node::admitting), and an address is not a credential (the stated assumption every service here makes) — and SWIM sharpens it, because any member may gossip about any member, so a member that lies about a third party is believed. SWIM’s failure model is crash faults, not Byzantine ones. There is no probe timer, no indirect-ping fallback (ping_req), and no piggyback budget: a node sends what its caller hands it. That loop — pick a peer, note its incarnation, wait out a timeout, call suspect with the incarnation it noted — is where timing lives, and nothing in swim::model says anything about timing.

HyParView: two small views

HyParView keeps no table of the cluster. A node holds an active view (the peers it gossips with, at most active_cap) and a passive view (a reserve of nodes it has heard of, at most passive_cap), and nothing else. This page is what is claimed about the node that holds them, and what is not.

It is one node, and it is the first piece, built the way SWIM was: the four handlers that build and prune the active view, with the model, the executable table and the refinement between them. src/hyparview/model_t.rs is the model, src/hyparview/exec_v.rs the table, and src/hyparview/proofs/invariant_v.rs the theorems.

What is proved

What is not claimed

• Symmetry of active views. The paper’s central property is that if a is in b’s active view then b is in a’s. That is a property of how several nodes are connected, and this model is one node. It is not stated here and is not proved. The Neighbor request that a terminal ForwardJoin sends is the mechanism that makes links two-sided, and what it sends is proved (H4); that the other end acts on it is the network’s.
• Connectivity, or a random sample. Nothing here says the overlay stays connected, or that a node’s peers are uniformly random. The picks are arguments, so how random they are is the caller’s.
• Shuffle, and promotion on failure. Not built. Without them a passive view only ever receives what forwarded joins and demotions give it, and a vacated active slot is not refilled. Promotion is what would use a failure detector’s verdict, and nothing here has one.
• Neighbor is always granted. The paper’s low-priority request, which an active-full node refuses and answers, is part of promotion and so not here.
• A ForwardJoin that ends a walk sends Neighbor to the newcomer. The paper leaves the two-sidedness of the link to the connection that carries the walk; the model says it as a message so that it has a name and is replay-safe.
• The network. sent only grows and a message may be delivered any number of times, so the handlers are proved safe on replays. Delivery itself, authentication of who is speaking, and the lock around a table are the service’s, which is plain Rust.

Protocol: the shape every model has

Every model in this crate is a labelled-step state machine: a state, a label for each kind of step, an initial predicate, and a relation saying which labelled steps are allowed. Each module spelled that differently (init/next, raft_init/raft_next, ray_init/ray_next, swim_init, actor_init, mb_init, composed_init), so nothing in the types said what a protocol is.

protocol::Protocol (src/protocol_t.rs, trusted) is that shape, written once: an associated Config, State and Step, an init, a step, and a provided next that is “some step”. Each model implements it at the bottom of its own model_t.rs. The agreement lemmas (src/protocol_v.rs, verified) pin each instance to the model it describes.

What is proved

What this does not say

• It is a shape, not a relationship. No theorem here relates two protocols. In particular the composed machine’s Protocol instance is written by hand; it is not derived from the ownership and Raymond instances. Deriving it is the generic composition tracked in #67.
• There is no observable view. What a consumer of a protocol may read (a membership protocol’s peers, a log’s committed prefix) is defined alongside the first property that reads it, in the membership contract (#65).
• No liveness for the other protocols. runs_of exists, but only the mailbox states a liveness theorem against it (P3). Giving the others one is separate work per protocol, and each needs its own fairness assumption.
• Nothing about the services. The service code is plain Rust and does not implement Protocol; it calls the verified step functions, which the refinement rows in the per-protocol chapters tie to the models.

The protocol as a Jetstream service

Every algorithm in this repository has a service, and each is a #[service] trait over Jetstream RPC implemented by a type that holds the algorithm’s state behind one lock and calls the algorithm’s verified step functions:

The shape is the same each time, and so is what it buys: no method takes the acting node’s number, because who is calling is the Context and a caller cannot forge it; and what a node does to itself is not something a peer can ask it to do on the wire. The sections below go through ownership in detail, and SWIM has its own service section; Raymond and the composed machine are summarised here.

Everything above is a model and a simulation of it. src/ownership/service.rs is the protocol served over Jetstream RPC — a #[service] trait Ownership with poll, acquire, write, begin_transfer and release, implemented by a Registry that performs the fence with ownership::exec::FenceGuard.

The service form removes a class of defect rather than guarding against it. The line protocol in tests/ carries the sender as a field — WRITE 0 41 claims to be node 0 — so the registry has to be told to believe the connection rather than the claim, and every request is a place to get that wrong. Four rounds of review on that suite were spent hardening exactly that rule. Here no method takes a node number at all. Who is calling is the Context, which Jetstream fills in from the transport: “The context is the transport’s, not the frame’s” (jetstream_rpc::server). A caller cannot forge it, so “the line lied about who sent it” is not defended against — it is unrepresentable.

force is absent from the trait for the same reason. It is the coordinator’s own transition, and the line protocol needed a dedicated control connection to stop a node sending it; a node-facing service simply does not offer it.

The assumption, stated rather than assumed. Context::peer() is the authenticated identity and is None over plain TCP — jetstream’s own comment says a plain stream authenticates nothing. The authenticated forms are a TLS certificate or an iroh NodeId, and NodeId’s value is private with no accessor outside jetstream_rpc, so neither is usable yet. The service therefore identifies a caller by address, against a roster fixed at construction. An address is not a credential. In a simulated network nothing can spoof one; on a real network it is worth very little. Replacing it with TLS identity is the first thing to do, and what does not change when it is replaced is the shape: identity arrives with the connection, never in an argument.

Neither durable nor replicated — and one of those is now fixed. The registry’s state lives in an Arc<Mutex<..>>, which supplies the atomic half of the model’s strongest assumption and none of the durable half. That gap is not a tidiness problem: every fencing theorem assumes epochs only go up, and a registry that comes back not knowing where it was can offer an epoch it already burned. A partitioned owner still holding that epoch is then unfenced — not because the fence failed, but because it was asked about a world that had been rewound.

So the starting epoch is no longer a number from the caller. It is read from an EpochFloor: a durable, monotone high-water mark of every epoch the registry has ever used. Registry::new starts strictly above it and writes that down before serving, and each later burn is recorded before the state depending on it is visible, so a registry that dies mid-decision skips an epoch — the safe direction, since epochs must not repeat but need not be consecutive. tests/ownership_durability.rs runs the same handover against a floor that remembers and against one that forgot, and asserts in the second case that the already-fenced owner writes again at the burned epoch while the node holding the later epoch is the one refused.

What is still missing is replication. Two registries sharing one floor would both read it and both believe they had allocated the next epoch: durability and atomicity want to come from the same place, which is why the row above says a real deployment keeps the ownership record in a store with compare-and-swap. This is the same class of caveat as the address-identity one, and it breaks the same guarantee.

What is verified about it, precisely. Every decision the service makes about the actor and every grant it publishes, and nothing else. poll, acquire, write, begin_transfer, release and force each go through a method of ownership::registry::RegistryCore, which hands the actor’s record to a function in jetstream_distributed::ownership::steps, stores what comes back, and publishes the grant the model’s transition publishes (E8–E9). The step functions are executable u64 code with postconditions stated in terms of the model, and ownership::proofs::refinement is where the postconditions are tied to tr_acquire, tr_begin_transfer, tr_handle_revoke, tr_complete_release, tr_revoke_owner, tr_reassign_unowned, tr_abort_transfer and tr_issue_grant — rows E1 to E6 above.

Two things are worth being exact about. First, the refinement is stated in both directions where the notion makes sense: a step function that refused everything would satisfy “whenever it fires, the model steps” perfectly, so the theorems also say that a refusal means the model’s step is not enabled. Second, what is left outside is named rather than left to be discovered: the lock, the identity lookup, the durable epoch floor and the audit log are not verified. They are the server’s business, and a step function that also resolved identity would have quietly folded an unverified lookup inside a verified transition.

The couplings that connect one actor’s u64 record to a whole System are hypotheses of the theorems rather than silent assumptions — the registry’s issued-grant set stands for network.contains(Grant { .. }), its roster for nodes.contains(..), an open connection for live.contains(..) — and the module docs of ownership::proofs::refinement tabulate which part of the service discharges each one.

The grant coupling is the one a server can break, and one did. granted is an input to the verified acquire step, so the registry’s set has to hold every grant the model’s network would — and four transitions publish one, not just the poll: tr_complete_release, tr_revoke_owner, tr_reassign_unowned and tr_abort_transfer each offer the actor on as part of moving it. A registry that recorded only the poll’s grant was applying the refusal theorem under a hypothesis that did not hold, which is worth nothing at all. The visible symptom was much smaller than the real one: a node that took the actor without polling first was refused, although the model had already published its grant.

Status. The service is pinned to the Jetstream working tree rather than to a release — 16.3.1 is not on crates.io, which the dependency resolution caught. Its dependency graph resolves, but the environment it was written in cannot reach crates.io’s tarballs, so CI is the first place it is compiled. That is the same footing the fuzz target was on when it was added, and it is stated here rather than discovered.

Raymond and the composed machine

The record is verified code; the shell is not (R16–R17). Router keeps an exec::RayTable behind its lock, and every routing method goes through it, so each is the model’s step by contract and each refusal is a step the model could not take. What is not proved: building the table (new, add_node) is not a model step, and that the finished table is ray_init — every other node points somewhere, the pointers reach the root — is checked by Router::new at start-up; the roster (which connection is which node), the lock, the audit log, and who may call seize and reconcile (the composed coordinator, which checks the token) are plain Rust the tests exercise.

Raymond’s Router hosts the whole routing record in one process, the way the ownership Registry hosts System::actors. That is the model’s own shape — Raymond is one struct — and it is what lets the router tell privilege (where the privilege is) from holder (what a node believes), the split the whole stale-holder analysis rests on. It is also a limit worth saying plainly: this checks Raymond’s rules, it does not distribute them. A deployment where each node keeps only its own entries and messages carry the rest is a different system with a different failure model, and nothing in raymond::model says it is refined by this one. Routing has one method per labelled model step a node takes (request_cs, make_request, receive_request, assign_privilege, enter_cs, exit_cs), each acting on the caller’s own entries. receive_request does take a from, and that is not the same thing as naming the acting node: it is the node the request is about, checked against the router’s own record of what has been sent, so naming a node that never sent one is refused rather than believed.

The composed Coordinator is the two services and the guards between them. Almost all of it is delegation, because cs_own and cs_ray carry a step the layers have already proved (C9). What it adds is the coupling: the privilege moves only once the actor has been released (assign_privilege), authority is taken only by the node holding the privilege (acquire), and the privilege can be seized from a holder that does not cooperate (Coordinator::seize_token, inherent — no node may cause it) leaving that holder owing a reconciliation (reconcile). Every method takes one gate first, because the coupling reads both layers’ state in one decision: with two locks taken one after the other, an acquire could slip in between the registry’s “unowned” and the privilege moving, stranding authority at a node that no longer holds the privilege.

What the composed service does not claim. The composed model guards some steps on own.live, which is ground truth — whether a node has crashed is not something any process can evaluate. The service has no Crash or Recover, so the steps it calls refine the composed machine’s crash-free executions, where every liveness guard is vacuously true (the service around those steps is plain Rust and tested); C8 states live.contains(..) as a hypothesis rather than dropping it. That cut does not lose the case the machine exists for: SeizeToken has no liveness guard on the node it takes the privilege from, so seizing from a holder that is merely unreachable — the wrongly-suspected node a real coordinator cannot tell from a dead one — is inside the fragment. And a standalone Router never creates a stale holder; seizure is the composed machine’s step, because the revocation that justifies it is visible there.

The coupling’s steps are data, and the coordinator runs them through one function. composed::service::Command is Seize { to }, Pass { me }, Acquire { node, epoch } and Reconcile { node }: the model’s SeizeToken, PassToken, AcquireUnderToken and Reconcile with the acting node written in. apply is a dispatch to the verified function of the same name (exec::seize_token, pass_token, acquire_under_token, reconcile), and every coupling method of the Coordinator builds a command and runs it through apply; what is left in the coordinator is taking the locks and writing the audit logs. This is a change of shape, not of behaviour, and the composed tests pass unchanged. apply is plain Rust: each arm is a verified function, and that the arm matches the command is read, not checked by Verus.

What it is for, and what it is not. A closure run under a lock cannot be proposed to a log, replayed, or applied on another machine; a command can. That is the first thing a replicated coordinator would need, and nothing here is replicated: the coordinator does not survive the loss of its process, as before. Four things are open, and are the reason there is no trait for “something that applies commands” yet (it is extracted when a second implementation exists, #77):

• The unit of replication is the composed state. The coupling reads both layers in one decision, so under replication the two layers’ records and the debts would have to be one replicated state with one log; two logs would make the coupling non-atomic, which is the race the gate closes today.
• Only the coupling’s four steps are commands. The single-layer calls the coordinator carries (write, begin_transfer, release, the routing calls) are still methods on Registry and Router, each with its own log and, for the registry, its epoch floor. The model’s Own and Ray labels are their commands, and a replicated registry needs them as such.
• Durability. Registry’s epoch floor is a separate durability concern today; a replicated log would replace it, and nothing says here that the two are equivalent.
• Reads and identity. poll, standing, the logs and well_formed need a stated consistency, and a command that did not come from the connection carries an identity somebody else vouched for (#66).

tests/raymond_routing.rs runs the textbook request path (D -> B -> A -> C and the privilege back) and every refusal; tests/composed_handover.rs checks the refusals that make the composition mean something — the privilege will not move while the actor is held, a node offered the actor without the privilege cannot take it, a seized holder is fenced and must reconcile. tests/raymond_turmoil.rs and tests/composed_turmoil.rs run the same stories across simulated hosts, one host per node, so the coordinator learns who is acting from the connection.

The actor

actor::service::Host holds an actor’s journal and a mailbox of what has been sent, and fences every append with the ownership Registry it is built around — the same registry, with the same epoch floor, that the Ownership service serves. The actor adds nothing to the ownership protocol; it uses it. Four of Actor’s methods are the ownership calls, delegated (poll, acquire, begin_transfer, release); the others are send (the caller numbers its own messages, so a retry after a lost reply is the same message), accept, two reads (state, journal), and receive, which ends at once because the model’s actor has no outputs. accept takes the sender whose message is being processed, and that is not the same thing as naming the acting node: it is checked against the mailbox, so a message that was never sent is refused rather than believed.

An append reads the registry (is this host the owner at this epoch?) and writes the journal, so the registry is built inside Host::new from the one roster and every method takes a gate first — the same construction, for the same reason, as composed::service. The fence is asked first and about the registry’s own record (Registry::may_write, which is may_write_step, which is can_mutate), so a host that is not the owner learns nothing about the journal. The behaviour is applied by the service, not the host: accept returns the state it produced, and a host that has just taken the actor catches up by reading the journal, not a copy of the previous host’s memory.

What the actor service does not claim.

• Its journal is in memory. The model assumes the journal is durable and linear — it has no crash that loses an accepted entry — and the service does not meet that: a restarted Host has an empty journal and an epoch floor that remembers only epochs. Durability is the next layer, and raft::store’s record store is the shape it would take. Until then the guarantees hold for the lifetime of the process, and not across its death.
• Crash-free executions only, as in composed::service: no Crash or Recover, because liveness is ground truth a process cannot evaluate.
• The behaviour is a pure fold. The model’s apply is a function from state and message to state, taken modulo a machine word so the executable version is not narrower. A real actor performs effects when it handles a message; nothing here says what an effect does if its host is fenced halfway through. The guarantee is about the journal, which is where the fence is.

tests/actor_journal.rs runs the guarantees through Jetstream — every call goes over a generated client channel and session to the generated server in front of the Host (Host::pipe, an in-memory stream whose peer address the caller names, as a TLS adapter supplies its handshake’s identity) — redelivery, messages ahead of their turn, the fence asked first, a handover that keeps the journal and fences the old host, a forced revocation, and all 24 orders of four messages from two senders each attempted twice, checked to give a well-formed journal whose state is the fold of whatever it holds. tests/actor_turmoil.rs runs the whole story across simulated hosts: a sender sends, the owner accepts, the actor is handed to another node, the old owner — still believing — is refused, and the new owner catches up from the journal.

Over any byte stream

Host::serve(io, peer) serves one connection over any AsyncRead + AsyncWrite stream, and Connection::new(io) is the client end: TCP, turmoil, QUIC or an iroh stream pair all fit. The one thing a stream may not be able to say is who is on the other end, so serve takes it as the peer Context — an accept loop reads it off the socket, a TLS adapter supplies its handshake’s identity — and the host believes it, so it must come from the transport and never from the peer. Host::pipe is the same wiring over an in-memory stream, for tests and examples, where the caller names the peer. The roster that maps a peer to a node is still keyed on IpAddr, so only RemoteAddr::IpAddr identities are accepted today.

A Connection owns the session as well as the channel, and has to: dropping a SingleLaneSession cancels its lane.

The mailbox as a transport

The mailbox of the previous section is what a call goes through, not something a caller sees. Given #[service] trait ActorB, a caller holding an ActorB — a generated ActorBChannel, or the implementation itself — writes self.b.b(ctx).await either way and cannot tell which:

caller ── ActorBChannel ── Session ──▶ Mailbox ──▶ serve ── ActorBService ── impl
                              ◀── reply ──────────────────────┘

• Mailbox<T> is the protocol’s six steps on real threads, each method one model step under one lock: a sender’s enqueue (through a Permit), set_state and schedule, and the drain’s claim, take and finish.
• Session<P> is a ClientTransport, which is all a generated channel asks of what it sits on. poll_ready reserves a slot, start_send enqueues, and poll_flush runs the rest of the sender’s operation, which is where the drain is woken.
• serve(mailbox, &mut service) is the drain. It takes rounds from the mailbox and hands each request to the service in the order queued, one at a time, so the service sees one request at a time and each sender’s requests in the order it sent them. Identity is read off the delivery, not the lane: a mailbox has many senders and one drain, and Server::rpc takes the Context per call. A request in flight when the drain is aborted is answered with an error, and only that one.
• serve_fenced(mailbox, &mut service, &fence) is serve asking a Fence before it starts each request. A request the fence refuses is answered FENCED to its sender and never reaches the service; the drain goes on, so a host that regains the epoch serves again. The fence is meant to be the registry’s may_write(host, epoch) about the host’s own claim, so it turns false when the epoch moves, whether by BeginTransfer or RevokeOwner. It is checked between requests: a handler already running finishes, so a handover waits for nothing. Tested, not proved (tests/actor_fence.rs): the ownership fence is proved, that this loop asks it first is not. What a running handler does outside the fence, the fence cannot stop, and a request that ran but whose reply was lost will be retried at the new owner (at-least-once).
• Supervisor owns the actors that run on a node (LocalSupervisor is the in-process sketch): spawn takes a required Fence and serves through serve_fenced, status says Running, Stopped (the handler panicked, so the drain ended) or Absent, and spawning over a Stopped id restarts it. Where an actor lives is the scheduler’s existing Discovery trait asked about an ActorRef; a supervisor answers for its own node only. Discovery may be stale and nothing relies on it: a request to a host that no longer owns the actor is answered FENCED. What the caller then does is not implemented here: a caller is expected to ask Discovery again and retry, and no caller in this slice does (the fence test checks only that FENCED comes back). Restarting a Stopped actor reuses its mailbox when the protocol is the same, so sessions obtained before the stop, and the requests already queued, reach the new drain; until it is restarted they wait, and a new transport is refused. drain(id) is the cooperative stop: it closes the actor’s fence (so it starts nothing, and what is queued is answered FENCED), waits for a handler that is already running to finish, drops the service, and returns; the status goes Running, Draining, Retired. The mailbox is kept, with a small task on it that answers every request FENCED, so a session made before the drain is told rather than left waiting, and spawn over a Retired actor takes the same mailbox over. A handler that panics while the actor drains makes it Stopped, and drain says so. Delivery stays at-least-once: a request that ran but whose reply was lost is retried at the new owner. Tested, not proved (tests/actor_supervisor.rs, tests/actor_drain.rs). Not here: a lane to a remote host, the retrying caller, who decides to drain (a composition with the ownership layer), and tying the fence to a registry, host and epoch.
• Backpressure. A mailbox is built with a Capacity, which is always the caller’s to say: Bounded(n) makes poll_ready wait for a free slot (the drain wakes it), Unbounded never does, and there is no default and no number that means “no limit”. The model’s queue is unbounded and a full mailbox is a sender that has not begun its operation, which the model reads as a stutter — so the safety proofs carry over, and the liveness theorem owes progress only to operations already begun. That is an argument about the mapping, not a proof.

What it does not claim.

• Only the core is a refinement. Verus checks exec::MailboxCore against the model (MB10–MB11); it does not check the lock, capacity, permits, wakers or notification around it, requeue, or that callers follow the sender’s three steps. Those rest on the tests (tests/actor_mailbox.rs and the unit tests in mailbox.rs: many senders into a small mailbox lose nothing and keep their order, a full one holds its callers back and not its queue, and an aborted drain answers only the request it dropped).
• serve does not check the ownership epoch. It hands each request to the service. The fence belongs around Server::rpc, and Host does not sit behind a mailbox yet.
• A bound is a place to deadlock, and a cycle already is. The drain runs one message at a time, so a handler waiting on an actor whose handler is waiting on it holds both drains whatever the capacity. A bounded mailbox adds a way in: a sender inside a handler waiting for a slot. Do not wait on another actor inside a turn that another actor can be waiting on.
• No subscriptions. Streaming methods are served by jetstream_rpc’s run on a lane; a mailbox delivers one request and takes one response. The reply path from the drain to each session is not bounded.

cargo run --example actor_basic runs two actors, each behind its own mailbox, with the first calling the second.

Network resiliency: the model, run for real

Everything above is a claim about a transition relation. It says nothing about whether an implementation follows it, and the gap has always been listed under future work. tests/ closes part of it by simulation rather than by proof.

Under turmoil — a deterministic, seeded, simulated network with a simulated clock — an executable ownership protocol runs over real sockets: a coordinator holding the registry, and three nodes polling, acquiring, writing and releasing. Partitions, delays and reordering happen underneath it while the model’s own theorems are checked as runtime oracles over the coordinator’s audit log:

The last row is different in kind from the seven above it and is listed separately for that reason. Every theorem in this repository has the form “this cannot happen”: none of them says a write is ever accepted, and none could — that is liveness, and it is not what the proofs are about. The consequence is a hole with a definite shape. A coordinator whose WRITE arm answered FENCED unconditionally satisfies all seven oracles above, because each is a claim about writes that got through and there would not be any. So the eighth checks the other direction of may_mutate’s definition — the registry accepts exactly when the actor is Owned by that node at that epoch, so a refusal aimed at the current owner is a state the model does not have. It is derived from a definition rather than from a proof, which is weaker provenance than the rest of the table, and it is the reason the table has a row the “claim it comes from” column cannot fill honestly.

The search over what arrives, not over what a correct node sends

The largest category of defect this suite found was a guard the search structurally could not reach. Action::from_pair emits only well-formed requests, and a named story drives the same node agent, which sends what a correct node would send — so a guard against a handover to the sender itself, a release from the node receiving the actor, or a line that does not parse is invisible to the scenario walk however long it counts. Not “not yet found”: unreachable. Six of them were written by hand, one test each, after a reviewer pointed at each in turn.

tests/protocol_lines.rs makes the malformed request something the search produces rather than something somebody remembered. It generates a connection and a line — well formed, corrupted, or arbitrary bytes — and drives the registry directly, asserting that no sequence of arbitrary lines from arbitrary peers can drive it into a state whose audit log the oracles reject. That is the property each of those six tests checks a single instance of.

Getting it to reach anything took four rounds of measurement, and the numbers are worth keeping because they are what a generator looks like when it is lying to you:

Every version passed the oracles. The first one passed them while reaching no write at all — it was refused at the parser 17 871 times out of 17 993 and would have looked like diligence. What caught it was a vacuity floor on requests that got through, and what caught the three after it was a floor on writes specifically, since polls alone satisfy the first floor while the run never gets as far as holding the actor.

The last change is the one to understand. A generator that could not echo the epoch it was just granted could not reach a write, because reaching one means quoting an epoch something else has usually just burned — so a minority of fields are filled from the registry’s last reply rather than from a table. That is what a node knows, not what the registry knows: giving the generator the actual state would make it emit only requests that succeed, which is the action alphabet again.

The floors are on what the generator produced, not on what came back. The first version of this walk floored refusals, on the reasoning that a refusal is evidence of malformed input. It is not. NONE, NO and FENCED are ordinary answers to well-formed, authenticated requests — a poll when the actor is held, an acquire that was never offered, a write at a burned epoch. Deleting every malformed generation mode and leaving only well_formed left this walk green with a higher refusal count than before, over more served requests. The check written specifically to stop a check from saying nothing was itself saying nothing. Each mode is now counted where it is built, and deleting any one of them takes its count to zero and fails. The limit of that is worth stating: the counters measure the label a step was generated under, so they catch a mode being removed and would not catch one hollowed out while keeping its label.

The oracles cannot see a request, only a log. They audit what the registry did, and a request that should have been refused and was executed instead leaves a perfectly legal log — it is a thing the registry is allowed to do, done for the wrong reason. So each step also carries an obligation, decided from the line and the connection alone: an unknown verb, the wrong field count, a field that is not a u64, or a FORCE off the control path must be refused in every state. Only unconditional refusals belong there; whether ACQUIRE 0 41 should succeed depends on the registry’s state and is the oracles’ business.

That obligation is the only thing in this walk that catches the parser defect filter_map was. It needed one generation mode to reach it. Every other corruption here changes the field count, which even the lenient parser rejected by accident; the shape that parser turned back into a valid request is a surplus non-number, inserted rather than substituted — POLL junk 0 arriving as POLL 0, right arity, executed. Measured both ways: with that mode deleted and the parser regressed, 20 000 seeds stay green; with it present, the walk fails on seed 0.

A refusal also has to be in the words that request uses. The reply check started as a flat set of the protocol’s tokens, which accepts any of them for any request — and a wrong-vocabulary refusal leaves the log unchanged, which is exactly what a refusal is supposed to leave behind, so no log-reading oracle can see it. Measured: with a refused RELEASE answered FENCED, and again with a refused ACQUIRE answered NONE, this search passed 20 000 seeds apiece while the registry spoke a protocol no node parses. The vocabulary is now per verb, read off what each request asks rather than off the handler’s branches: a poll is answered with a grant, a revocation or nothing; a write either lands carrying the sequence number it landed at or is stopped by the fence; everything else takes effect or does not. NO and ERR stay universal, because when a refusal is owed is the obligation’s business, not the vocabulary’s. An unwarranted refusal is a separate question, and I got it wrong once. A refusal moves no state and writes no log entry, and I concluded from that that no such refusal is judged anywhere — liveness, out of scope. That is wrong. may_mutate (refusals) judges exactly this for writes: a registry that refuses its own current owner, which is what oracles_catch_an_overfencing_coordinator exists for. The real distinction is not safety against liveness but logged against unlogged — that oracle fires on Event::Fenced, so the same refusal spelled NO or ERR walks straight past it, and the aggregate floors are no help against a defect that is selective rather than total.

Which generalises, and the general form is the useful part:

Any correct behaviour whose absence leaves the log unchanged is invisible to an oracle that reads the log.

So the same hole existed in every transition, not just the write. Measured, one legitimate request in three refused with an unlogged NO, before the check existed — each of these passed 20 000 seeds, over half a million requests, with every floor satisfied:

Standing reconstructs the registry’s state from the audit log and answers whether the model permits a request. It is the same reconstruction may_mutate (refusals) was already doing for one question, made whole and shared with it rather than copied. After the check, 200 000 seeds pass with counts identical to before it — so it rejects nothing legitimate.

And the dual of it, which that fix was missing. The check above catches a registry that does nothing and says no. It says nothing about one that says yes and does nothing — an ACQUIRE answered OK with no acquire logged, a POLL answered GRANT 41 with no grant issued. An unchanged log is a perfectly valid log, so no oracle handed the finished run can see it, and each of those passed 20 000 seeds.

Together the two halves say the whole thing:

The reply and the log must agree. Every reply names a transition or names none, and the events the step appended have to be exactly that.

That correspondence can only be checked during the run. An oracle handed a finished log cannot tell which entry belongs to which request — which is precisely the information a lie about success destroys. Five lies are checked both ways, including a write’s OK carrying a sequence number one off from the one it landed at. It costs about eighteen per cent more wall clock, which is the only reason to mention it.

Provenance, stated because it is weaker than most of this file. No Verus theorem says any request is ever accepted; the proofs are all of the form “this cannot happen”, and liveness is not what they are about. may_mutate (refusals) already crossed that line deliberately, for writes, and this extends the same argument to the other transitions. It inherits the same weaker provenance rather than pretending otherwise.

What is genuinely out of scope is a good POLL answered NO. tr_issue_grant being enabled is not the model requiring it to fire, and NONE answers any poll, so a registry that refused every one would satisfy every oracle here.

Writing that obligation down went wrong three times, the same way each time, and none of the three was caught by reading it. The two refusal reasons are independent, so every one that can be established has to be: an obligation that drops a reason it could have known demands one exact refusal where two are defensible, and then reports a sound registry as defective for choosing the other. FORCE 41.0 from a node is both unparseable and unauthorised, and deciding the fields first demanded ERR from a registry that refuses strangers before parsing their input — which is the better order, not a fault. Fixing that for FORCE and stopping there was one case short of the rule: WRITE 0 junk on the control connection is the same shape, because the sender field is legible even though the epoch is not. Fixing that for the sender field and stopping there was one field short again: BEGIN junk 99 names a successor that does not exist and FORCE 99 junk does too, and an all-or-nothing parse let one illegible field hide what the legible ones carried. Three catches of one mistake, each a field further out, so it is written down as the rule instead of as a third case: a permission check uses its own field’s parse result, never the whole line’s. Authority is decided from whatever is legible, before the line is judged well formed at all, and the tests pin it in both directions — relaxing an obligation is only safe while the strict cases stay strict.

Still thin. Completed handovers are reached 5 times in 1 024 runs, so claim 4 is barely exercised here — it is covered by the scenario walk and the named stories instead. That count is reported and deliberately not asserted on: a floor on a rate that low would be a flaky test rather than an informative one.

CI walks 100 000 of these seeds — 2.7 million requests in twelve seconds, against forty-six for the 256 simulated scenarios in the same job. The window is fixed so a red result means the change did it; JETSTREAM_PROTOCOL_START moves it. The default stays at 1 024 so a contributor’s cargo test is instant.

fuzz/ is the coverage-guided front end to the same generator, registry and oracles, run for a minute on every pull request, and is the arm that explores somewhere new on every run. It needs nightly, so it is its own workspace and its own job; the pinned stable toolchain the proofs are built with is never in question for it.

Two searches reach them. turmoil_ownership.rs holds named stories, each of which asserts what it was supposed to reach — the headline one is A owning the actor at epoch 41, being cut off, the coordinator handing the actor to B at 42, and A returning still holding a guard that says yes. turmoil_scenarios.rs counts seeds upwards, generating action sequences it has no opinion about, and replays every seed in tests/seeds/scenarios.txt first so a fixed bug stays fixed. Both drive the same runner and the same oracles. Scenario::from_bytes is the entry point a coverage-guided fuzzer would use to drive that same runner; the fuzz target that exists drives the protocol-line generator instead, for the reason given above — the action alphabet cannot express the inputs most of these guards are about.

What this is evidence of. A divergence is one of two things: an implementation that does not follow the protocol, or a protocol whose proof rests on something the network does not give you. Both are findings. What it is not is a check on the proofs — those are static, and no simulation can contradict them. It is also not a substitute for a refinement: the coordinator in tests/ is hand-written to match the model and nothing machine-checks that it does — which is exactly the gap src/ownership/steps_v.rs closes for the Jetstream service in src/ownership/service.rs, and the reason the two coordinators are worth keeping side by side.

Would the oracles notice? A suite that cannot fail is indistinguishable from one that passes, so oracles_catch_an_unfenced_coordinator runs one story twice with a single bit changed — the coordinator stops checking writes against the registry — and requires the oracles to reject the second run. Same actions, same seed, same network, same oracles; what separates them is exactly the check src/ownership/exec_v.rs says has to happen where the effect lands. oracles_catch_a_write_at_a_burned_epoch does the same for the fencing oracle, on the case the others cannot see: a stale write with nothing written after it. oracles_catch_an_overfencing_coordinator is the mirror of the first: the same story again with the fence jammed on rather than off, which is the failure none of the seven proof-derived oracles can see, and which the eighth exists for. The write floor in the seed walk catches the totally degenerate version of it by counting accepted writes across the window, but a registry that fenced only one node, or one request in three, clears that floor comfortably.

Beyond those two, every oracle in the table has a witness: a hand-built log that it, and not one of its neighbours, rejects — paired where it matters with a nearly identical log it accepts, so a check cannot pass by rejecting everything. The logs are hand-built on purpose. Several are ones this coordinator cannot produce, and that is the point: an oracle which is sound only because the thing it audits is correct is not auditing anything. Writing those witnesses is what found most of the defects in this table: of the six oracles that existed when the audit started, three were checking something weaker than the theorem they named, and one of those was checking the wrong thing entirely — the P5/P6 oracle read write epochs, which is a consequence of “an epoch determines its owner” rather than the claim, and accepted an epoch changing hands with nothing burned between.

That second one exists because the first version of check_invariants did not catch it. Comparing writes against writes notices a stale write only once the replacement owner has written too, so Acquire(0)@41, Force→42, Write(0)@41 had one writer per epoch, a strictly increasing burn and an acquire behind every write — and sailed past every check, which is precisely the failure the epoch exists to prevent. A burn is what makes an epoch stale, so a burn is what the high-water mark has to follow.

Where the executable code lives, and why. Entirely in tests/. CI greps src/ for verifier::external, so unverified protocol code there would need that attribute and would fail the build by design. The one piece of src/ the simulation uses is FenceGuard, because it is the node-local check a real node performs — and watching a stale guard say yes while the coordinator says no is precisely the asymmetry src/ownership/exec_v.rs documents.

Where the model makes a node act, the simulation makes that node send the request. tr_begin_transfer carries pre.live.contains(from) — agreeing to hand over is an action by the owner — so BEGIN originates at the owner’s host and names itself, and the registry checks the sender. A partitioned owner’s agreement is swallowed by the partition, which is what that liveness guard means here. Routing it through the driver instead would let a node nobody can reach volunteer, reopening in the simulation the exact hole the guard was added to the model to close.

For the same reason, the three ways the coordinator forces progress are kept distinct rather than merged: tr_revoke_owner from Owned, tr_reassign_unowned from Unowned, and tr_abort_transfer from Transferring. Only the first two take a successor from the caller; an aborted transfer returns the actor to the node it was being taken from, and a coordinator that redirected it anywhere else would be stepping outside the transition relation.

One place where the simulator is kinder than a network. turmoil knows whether a route exists, so a request made across a partition that is already in place fails immediately at the sender. A real partition drops the packet and the sender learns nothing until its own deadline expires. The node-side counters keep the two apart — writes_failed against writes_timed_out — and the seed walk prints both, so the difference is visible rather than assumed.

Printing them is how the gap was found. A run reported 284 writes sent across 256 seeds with zero unanswered at the deadline: every failure was a removed route, so the node’s deadline had never once fired and the scenarios contained no request that was accepted for delivery and then ignored. Since “duplicate, reordered and arbitrarily delayed requests are safe” is one of the claims in the table above, a search that could not produce a delayed request was not reaching it. Stall and Resume use turmoil’s hold/release to do exactly that.

Three stories then split the case apart, because one story could not carry it. a_held_request_expires_and_the_node_carries_on shows the node giving up and going on working. That alone is satisfied by a run in which nothing is ever delivered late, so a_delayed_write_arrives_at_a_registry_that_moved_on releases the hold while the node is still waiting: the write is delivered into a registry that burned its epoch meanwhile, and is fenced on arrival, which is the claim itself. And a_timeout_is_not_evidence_the_write_did_not_land covers the direction no network behaviour produces — the registry applies the write and answers after the caller has given up, so a node that read its own timeout as a verdict would be wrong about a write that had already landed. It costs nothing here only because nothing in the protocol reads them: a node that distinguished “no route” from “no reply” would hold information a real one does not, and treating either as a decision about ownership is exactly the mistake the fence exists to make unnecessary.

Two places where the simulation is deliberately coarser than what was proved, stated rather than glossed:

• tr_handle_revoke and tr_complete_release are folded into one RELEASE request, so the simulation never occupies the intermediate state the model distinguishes;
• the registry is a Mutex, which is the executable form of the model’s load-bearing assumption that ownership records are updated atomically. A deployment buys that from consensus or a compare-and-swap store. Saying so is the point: the assumption is visible rather than smuggled in.

cargo test --test turmoil_ownership -- --nocapture   # the named stories
cargo test --test turmoil_scenarios -- --nocapture   # the seed search

# search further: a moving, non-overlapping window
JETSTREAM_SCENARIO_START=100000 JETSTREAM_SCENARIO_SEEDS=20000 \
  cargo test --test turmoil_scenarios --release

A third CI job runs both on every pull request. It needs no Verus toolchain: ordinary rustc erases the ghost code in verus! and leaves FenceGuard behind.

Status: proven, modelled, future work

Against the pinned Verus release, verus --crate-type=lib src/lib.rs verifies the whole crate with no errors. CI writes the current count into each run’s job summary, which is the authoritative figure — the snapshot in prose drifts, the job summary does not.

Machine-checked (every proof fn in src/{algorithm}/proofs/ is checked by Verus in CI, with no assume/admit/external_body/axiom):

• exclusive mutable ownership, in every reachable state;
• unique authoritative epoch (existence and uniqueness);
• stale-owner fencing, including the headline A@41 / B@42 / A returns scenario as a concrete eleven-state reachable execution;
• epoch monotonicity, per step, per next, and along whole executions;
• transfer safety - the inductive invariant is preserved by every transition, and no stage of a handover admits two owners;
• token uniqueness, both “at most one token confers authority per (actor, Epoch)” and the stronger “at most one token is ever issued per (actor, Epoch)”;
• stale tokens surviving crash, partition and recovery confer no authority;
• the ownership registry’s record, grants included: each of its methods takes the model’s step and publishes the grant the model’s transition publishes, and a refusal is a step the model could not take (E8–E9);
• Raymond: at most one token, routing cannot manufacture ownership, duplicate, reordered and arbitrarily delayed requests are safe, and token transfer preserves the coupling to the ownership layer;
• the coupling itself, as an invariant of the composed machine: in every reachable composed state the only node that may mutate the actor is the node holding the token;
• Raft: Election Safety (C1–C11), Log Matching (C26) and the single-step log properties (C12–C19);
• Raft’s term structure and the election restriction: a log’s terms never decrease and none exceeds its holder’s own, so the last term is the largest; a follower that already agrees with the leader at an index keeps its entry there, which is what makes figure 2’s conditional truncation load-bearing rather than merely faithful; and a candidate behind on terms cannot collect a vote at all (C39–C43);
• State Machine Safety, with exactly one hypothesis — that two commits at an index agree on the entry’s term (C46). The value half is unconditional, because one (term, index) names one act of creation by one leader. Nothing about values, quorums or counting is missing;
• what a commit was: a majority held that entry at that index, entry for entry rather than as a prefix length, and the record of it never shrinks (C44–C47, C50, C52);
• what a vote was a judgement of: every vote is on the record with the voter’s log as it stood, and every recorded vote went to a candidate at least as up to date as that log (C49) — and what the summary it was judged against was a summary of, so that a winner’s own log, rather than a pair of integers off the network, is what dominates its voters’ logs (C51–C52);
• why the entry was still there to be judged: a commit’s quorum is already at the commit’s term, so only a leader at or past it can ever overwrite them, and the entry survives for as long as those leaders hold it (C53–C54). The condition is the induction hypothesis, stated as one;
• the durable log: recovery is exact, a crash can only rewind, and a byte prefix of the device parses back to a record prefix — so figure 2’s suffix deletion is implementable on a device that deletes nothing;
• SWIM’s merge rule: idempotent, absorbs a repeated message, never accepts a record that does not out-rank the local one, is commutative and associative — and, lifted through every step of a run, no node’s record about any peer ever moves backward (S1–S6); the executable merge is that rule, and a refutation out-ranks the accusation it answers and is itself a gossip step (S7–S9); and the node’s table is checked to learn by the model’s tr_gossip, a refutation being a second one (S10–S12);
• the Raymond routing steps and the composed machine’s coupling guards agree with their models in both directions — each fires exactly when the model’s transition is enabled — and a step a layer already proved is carried by the composed machine without a second proof (R15, C8–C9); and the routing record the service keeps is checked to take the model’s steps and to refuse where it cannot (R16–R17), and the composed coupling’s four steps over both layers’ records and the reconciliation debts are the composed model’s (CX1–CX2);
• the distributed actor: at most one host appends, now and across handovers (one host per epoch; nothing written under a superseded epoch); each message once, in the order sent, none invented; the journal is append-only and the state is a fold that a handover preserves; and the executable steps agree with the model (A1–A15);
• the actor’s mailbox: nothing lost, repeated or reordered; each sender’s messages numbered without gaps, in the very form the actor’s accept guard counts; and — the first liveness theorem here — every enqueued message is eventually processed under weak fairness of the drain’s and each sender’s steps, with the fairness rules proved in temporal and both the fair run that satisfies the assumption and the unfair one that shows it is needed exhibited (MB1–MB9); and the executable mailbox core, whose every step is checked to be the model’s (MB10–MB11).

Modelled but not proven (present in the state machine, no theorem beyond invariant preservation):

• the specific message shapes (Revoke / Released / Grant) - safety does not depend on them, which is itself the point, but no separate theorem says the message flow is the only way to make progress;

• Raymond’s holder pointers have a unique root but are not proven acyclic — both halves of that were wrong by the time it was written, in opposite directions. Acyclicity is proved: ray_acyclic is part of ray_inv and every transition preserves it (R11). And the pointers do not have a unique root: after SeizeToken(A, B) both holder[A] == A and holder[B] == B, and that is deliberate — A is a stale holder whose belief nobody could reach in to correct. Uniqueness belongs to Raymond::privilege, the authoritative field, not to the belief graph.

  So the unconditional guarantee is an acyclic forest of beliefs plus a single authoritative holder. Reaching that holder by following pointers (R12) needs ray_no_stale_holders on top, which is exactly what reconciliation restores. Routing termination would need the liveness the model does not claim.

• The durable log is not wired to a device, and the reason has moved. The executable layer exists — replay_exec, encode_exec and parse_exec refine their spec counterparts, and verifying them found two bugs no test could have. What is missing is a device, and the obstacle is a crash model, not an interface: pmemlog’s persistence_chunk_size is 8 and a write must be safe for any subset of 8-byte chunks having flushed, which POSIX does not promise for a write crossing a chunk. Until a device supplies it, pmemlog’s two corruption assumptions are not assumptions of anything proved here.

• Compaction is proved sound and is not scheduled — closed by worth_compacting at records > 2 * (entries + 1). Left struck through rather than deleted because it stood here for three PRs after the policy landed.

Not modelled at all (a gap, stated rather than papered over):

• Raymond itself has no crash model. The ownership layer models crash, recovery and unreliable failure detection; Raymond’s own steps do not. A Raymond in which nobody holds the privilege is not reachable, because Raymond::privilege always names a node and ray_wf keeps it inside nodes — which is now structural rather than an inductive invariant.

  What is now modelled is the case that matters for the composed claim: ComposedStep::SeizeToken re-establishes the token at another node without the holder acting, so crash-driven takeover is reachable rather than requiring a dead node to cooperate. Before that existed, the only token movement in the composed machine was PassToken, which requires has_token(pre.ray, from) and models from voluntarily handing the privilege on — so theorem_composed_reachable_inv was quantified over executions in which the token always moves voluntarily, and crash-driven takeover, the case epochs exist for, was not among them. That was a real narrowing of the composed claim, and it is fixed rather than documented away (scenario_composed_crash_takeover exhibits the execution).

• SWIM has no probe scheduler, no indirect-ping fallback and no dissemination piggyback budget. swim::model is the merge rule and one transition, and swim::service is a table that obeys it; a real deployment’s failure detection and gossip timing — how often, and by piggybacking on what — is not modelled at all, so nothing here says gossip eventually arrives, only that whatever arrives cannot move a view of the world backward (S5). See SWIM for which half of the convergence argument that is.

• The actor’s journal is assumed durable and linear, and the service’s is in memory. The model has no crash that loses an accepted entry; the service’s journal dies with its process, so the guarantees hold for the lifetime of the process and not across its death. Durability is the next layer.

• The actor proves safety; the mailbox proves delivery, but Host does not sit behind the mailbox. The actor’s own model says nothing about a message ever being offered to its host, and an out-of-order arrival is refused, not buffered. actor::mailbox proves that a queue in front of it delivers every enqueued message, in order, under a stated fairness assumption. service::Mailbox, Session and serve run that protocol and deliver to any generated service, but only the queue-and-flags core under their lock is a verified refinement (the lock, capacity and wakeups are not), serve does not yet check the ownership epoch around each call, and Host still keeps the actor’s sent set and relies on its caller to call accept. Subscriptions are not served through the mailbox, and the reply path is not bounded. The actor’s behaviour is a pure fold, so what a message does beyond changing the state — an effect, a reply — is not modelled, and neither is what an effect does if its host is fenced halfway through.

• The actor service refines the crash-free executions only, for the reason the composed service does.

• The Raymond and composed services host the global record in one process. raymond::service::Router holds every node’s entries under one lock because the model’s Raymond is one struct, and the composed Coordinator serialises both layers behind a gate because the coupling reads both. They check Raymond’s rules; they do not distribute them. A deployment where each node keeps only its own entries is a different system, and nothing here says it is refined by this one.

• The composed service refines the crash-free executions only. The composed model guards some steps on own.live, which is ground truth and not something a process can evaluate; the service has no Crash or Recover, and C8 states liveness as a hypothesis. Seizing from a holder that is merely unreachable is inside the fragment, because SeizeToken has no liveness guard on the node it takes the privilege from.

• SWIM’s Left is simpler than memberlist’s StateLeft. memberlist gives a graceful departure its own precedence and rejoin rules. swim::model::Status has Left, ranked above Dead so that a failure verdict cannot undo a departure (S13, S14), but a rejoining node is an ordinary node that hears it is gone and refutes with a higher incarnation, exactly as after Dead. There is no separate rejoin handshake. Members are never forgotten, so a departed member’s record stays and counts against the bound of MAX_UPDATES members.

Future work (deliberately out of scope):

• liveness of either layer - progress, fairness, termination of a handover, and Raymond’s “every request is eventually served”. These need assumptions (reliable FIFO links, eventual failure detection) that this model does not make.

• done, for the registry’s transitions: the refinement from the nat-valued model to an executable u64 implementation, with the epoch-exhaustion case handled, is src/ownership/steps_v.rs and src/ownership/proofs/refinement_v.rs — see rows E1 to E6. What remains unrefined is the node side: src/ownership/exec_v.rs still offers no way to advance a node’s fence guard, only to consult it, so that no executable API can perform a handover the model does not;

• the actual actor runtime: networking, persistence, and the code that obeys the protocol. Verifying the protocol says nothing about whether an implementation follows it. tests/ now exercises a hand-written one against the model’s own theorems on a simulated network (see Network resiliency), which is evidence rather than proof: nothing machine-checks that the coordinator in tests/ refines the transition relation in src/;

• Raft’s Leader Completeness, and with it State Machine Safety unconditionally. This is now a much smaller gap than the sentence that used to sit here, and worth stating precisely rather than as a caveat.

  State Machine Safety already holds with one hypothesis (C46): that two commits at an index agree on the entry’s term. So the whole of the remaining risk is one question — can two leaders commit entries of different terms at one index? — and that question is Leader Completeness.

  All three ghost records the induction needs are in place: what was committed (C44–C47), the voter’s log as it stood at the vote (C49–C50), and the creation/leadership history Log Matching is built on (C20–C26). No fifth was needed for the summary that vote was judged against, because messages never shrinks (C51). So are the theorems the induction will call:

  • C45 — a majority held the entry at commit time, entry for entry;
  • C54 — that voter still held it when it voted. Still conditional, and the condition is the induction hypothesis over the closed range of terms from the commit’s to the election’s: a quantifier over the leaders of those terms, rather than C48’s quantifier over steps with a paragraph claiming the two are the same thing. C53 performs the translation. The upper endpoint is an obligation, not a formality — a leader of the election’s term can exist before this voter has voted in it — so the induction must settle its own case at that term before using C54 there, or close the window earlier;
  • C50/C52 — the winner’s voters meet any quorum, with the judgement attached, and the judgement is about the winner’s own log. C50 alone was not enough for this step and the earlier version of this list said it was: its conclusion is about the pair of integers a RequestVote carried, and C52 is what ties those to the log;
  • C43 — a candidate behind on terms is refused.

  What is missing is the strong induction over terms that assembles them. Every theorem above is about one state or one step; the induction relates a commit in term T to an election in a later T' and has to carry the commit-time quorum across the run between them, which is exactly what C48’s hypothesis is. Until it lands, the registry’s contents agree where servers overlap but are not yet guaranteed to survive a leader change — the half of the atomicity assumption that is load-bearing for System::actors;

• reconfiguration. Membership is fixed. Joint consensus is a real and well-known source of Raft unsafety and is not attempted here.

• the rest of SWIM. The probe timer and its schedule, the indirect-ping fallback a probe target’s neighbours run when a direct probe times out, and the piggyback selection that decides which records ride on which probe. The merge core, its executable steps and the Membership service are done; what is left is the part with a clock in it. The SWIM section above says what is and is not claimed.

The holder graph is a tree, and now says so

ray_unique_token and ray_token_exists together say there is exactly one root. That is not the same as the holder graph being a tree: nothing stopped a set of non-root nodes from pointing at each other in a cycle, off to one side of the real root. ray_init permitted it too — it forbids only a non-root pointing at itself, so A → B, B → A beside a root C → C satisfied it.

The consequence was visible in src/raymond/model_t.rs’s own opening comment: “requests travel hop-by-hop towards the token” is false for a node inside such a cycle, whose request would circle for ever. Nothing in the safety proofs depended on the claim, which is exactly why it went unchecked for eight review rounds.

ray_acyclic is now part of both ray_inv and ray_init, stated as the existence of a rank — a nat per node that strictly decreases along every non-root edge, which is well-foundedness and so admits no cycle. The existential is the form the proofs want, because a step preserves acyclicity by exhibiting a new rank. For both token movers that rank is the old one shifted up by one with the new root sent to zero, and lemma_repoint_acyclic proves it once for both: they rewrite exactly the same two pointers, and neither the old token position nor any parent-child relationship between the two nodes is needed.

theorem_every_node_reaches_the_token is the payoff, by induction on the rank. It is still a safety property — the route exists in the current state — and not liveness, which would need the assumptions listed above.

Scenarios export labelled runs, not endpoints

The recurring defect on this PR was a scenario whose postcondition described the world afterwards but never how it got there — and “how it got there” is the entire content of a scenario. The repair went through three stages, and only the third one holds:

1. ensures true — a scenario that proved nothing.

2. An exported step — better, but a step and an endpoint exported as independent existentials can come from different executions.

3. A reachability-from relation tying them together — better still, and still not enough: composed_reachable_from(c, d) says some run joins c to d, but which steps that run took is hidden inside composed_next’s existential. Every scenario built this way turned out to be satisfiable by a substitute execution, and each repair excluded only the one substitute that had been found:

   Scenario	Substitute execution that satisfied it
   crash takeover	Acquire(A@41) → BeginTransfer → HandleRevoke → CompleteRelease → Crash(A) → SeizeToken → Acquire(B@42) — A gave the actor up voluntarily, and no RevokeOwner occurred at all
   voluntary handover	an unrelated A → B transfer at epochs 39 → 40, then Acquire(A@41), then RevokeOwner to reach B@42 — the advertised 41 → 42 release never happened
   request routing	A, B and D each call RequestCs independently and then serve their own queue heads — D’s request is never forwarded B → A → C

4. The labelled run. composed_run(tr, labels) and ray_run(tr, labels) carry the step labels alongside the states, and a scenario exports the whole object. Fixing every entry of labels says exactly which steps the run consists of and in what order, so no other run can satisfy it — not because each alternative was anticipated and ruled out, but because nothing is left free to vary.

lemma_composed_labelled_execution_is_execution and lemma_ray_run_is_segment show the labelled forms imply the unlabelled ones, so every theorem stated over composed_reachable still applies; the scenarios only got stronger.

What labels do not carry is data the step takes from the state it fires in. ComposedStep::Own { own_step: Step::BeginTransfer { actor, from, to } } names no epochs, so the handover’s label sequence alone is satisfied by a 39 → 40 transfer. The scenario therefore also exports the Transferring state at the index it occupies:

The phases that keep these proofs tractable thread the run rather than an anchor: each takes the run built so far, appends its own steps with their labels, and hands the whole thing on, so splitting a scenario for the solver’s benefit costs nothing in what the scenario claims.

No escape hatches

The proofs in src/ use no assume, admit, external_body, axiom, or any other way of asserting something Verus did not check. CI enforces it by grep on every pull request.

bit_vector and nonlinear_arith are not escape hatches

raft::proofs::wire uses both: by(bit_vector) for the little-endian round trip, by(nonlinear_arith) for the division bookkeeping in C32. Neither asserts anything. They hand the goal to a different decision procedure — bit-blasting for the first, a nonlinear arithmetic solver for the second — because the default encoding is poor at bits and at multiplication. The obligation is discharged, not waived: a false goal fails under either.

They are named here because “no escape hatches” should mean something precise, and a reader who greps for assume should also know what by(...) does.

IdSet rests on vstd’s HashSet specification

id::IdSet is a std::collections::HashSet<u128> — the number inside each Id — whose view is Set<Id>, by a lift spec function and one lemma that an id is in the lifted set exactly when its number is in the stored one; the Raft tally and the composed machine’s debts are IdSets. What it promises (insert, remove, contains, len, is_empty are the set’s) is proved from vstd’s specification of HashSet, and that specification is trusted, not proved: in particular vstd::std_specs::hash::obeys_key_model::<u128>(), that the default hasher behaves as a function on keys. The axiom lives in vstd, so CI’s grep over src/ does not see it, and it is named here so that nobody has to find it. The set stores the u128 and not the Id because vstd states that axiom for the built-in key types only; for a type of ours it could be assumed only with an assume, which CI rejects. The Vec scans it replaced rested on Vec’s specification alone.

Id itself adds nothing to trust. Its == is defined in the language, with vstd’s PartialEqSpecImpl (obeys_eq_spec is true and eq_spec is equality of the numbers), and id::value::lemma_id_eq says so.

The one exception, and it is not in src/

vendor/verified-storage/pmemlog is Microsoft’s verified persistent-memory log, vendored unmodified, and it has six. Three are I/O primitives and a CRC computation — the code that actually touches the device, with nothing beneath it to verify against. Two are assumptions about the physical world, and anything this repository ever proves on top of that log is conditional on them:

• axiom_bytes_uncorrupted: if y is the CRC of x, and a read gives back x_c and y_c with y_c the CRC of x_c, then x_c == x. This says a CRC detects the corruptions the device actually produces. It is not provable and it is not free: a device whose corruptions are CRC-preserving violates it, and every guarantee resting on it.
• axiom_corruption_detecting_boolean: the two flag values CRC(b"0") and CRC(b"1") are far enough apart that corruption cannot turn one into the other.

These are stated here rather than buried because the repository’s rule is that an assumption may be an explicit documented part of the system model and may not be a way of making verification pass. These are the former; they are enumerated one by one in vendor/README.md; and the CI grep covers src/ and not vendor/ for exactly this reason, with the reason written into the workflow.

Nothing in src/ depends on vendor/verified-storage/pmemlog yet. When something does, this section is where the conditional lives.

There are also no raised solver budgets: no #[verifier::rlimit] anywhere. The long concrete scenarios are kept tractable purely by splitting them:

• scenario_composed_handover = handover_phase_release + handover_phase_request + handover_phase_pass_token + handover_phase_acquire;
• scenario_request_and_token_routing = routing_phase_requests + routing_phase_token_hops + routing_phase_delivery, with the token hops themselves delegated to routing_one_hop, proved once against an abstract state.

Each phase hands the intermediate state to the next as an abstract characterisation, so no single query reasons about a dozen nested Map/Set literals at once, and every phase verifies within Verus’s default budget. Two phases previously carried #[verifier::rlimit(40)], and between them dominated the cost of the entire proof run; splitting them removed the need. (rlimit would not have been an escape hatch — it is a solver budget and cannot admit an unproven fact — but a proof that needs a raised ceiling is usually a proof that wants splitting.)

Splitting also surfaced a genuine defect in the specification. Reduced to a single AssignPrivilege step, routing_one_hop still exceeded the solver’s limit — a cost that scaled with nothing in the proof. verus --profile named the cause: ray_wf was a matching loop. Under the trigger r.nodes.contains(n), its conclusion r.nodes.contains(r.holder[n]) matched that same trigger at r.holder[n], and so on without bound — 171,941 instantiations of one quantifier, 40% of 419,801 in a single proof.

ray_wf is now ray_maps_total (entries exist, triggered on r.nodes.contains(n)) and ray_holder_closed (pointers stay in the cluster, triggered on r.holder[n]). The second trigger fires only for holder pointers some term already mentions, and its conclusion creates no new holder[_] term, so nothing regenerates it. This mattered beyond speed: a matching loop makes proofs pass or fail according to how many instantiations the solver burns before it stumbles on the argument, which is precisely the kind of fragility a proof suite should not have.

Every quantifier in src/ has since been audited for the same defect, and three more were found and fixed: ray_init’s non-root clause and ray_holder_closed regenerated each other across two quantifiers, and valid_execution / composed_valid_execution walked off the end of a sequence (tr[i] introduces tr[i + 1], which matches the trigger at i + 1; the i < tr.len() - 1 antecedent is checked after instantiation, so it does not stop e-matching). Both now use multi-triggers naming the terms that must already exist.

The same care applies to assert forall, which carries whatever trigger is written at the assertion site — lemma_ray_frame_inv and lemma_reachable_step had each rebuilt a loop locally that the specification no longer contained.

What that audit is and is not. It is manual inspection plus the absence of resource-limit blowups; it is not a check anything enforces, and the distinction matters because nothing would fail if a future quantifier reintroduced a loop until it happened to exhaust a budget. Of the 176 quantifiers in src/, 151 carry an explicit #[trigger] or #![trigger …]; the remaining 25 rely on Verus’s inference, and are the ones where the inferred trigger is a single application term with nothing to regenerate (exists|s| step(pre, post, s) and the like). CI additionally passes --triggers-mode silent, which suppresses the notes Verus would otherwise print about automatically chosen triggers — good for signal-to-noise in the log, and worth knowing before treating the build’s silence as evidence about triggers. It is not.

CI greps src/ for the real escape hatches and fails the build if any appear. Everything the proofs rely on that is not derived is a modelled transition or an explicitly documented entry in the failure-model table above.

That grep now runs over a src/ that also holds two Jetstream services, and it still means what it said. The services are behind a feature that is off when the proofs are checked, so Verus never compiles them and none of them needs a #[verifier::external] to be kept out — which is why the feature exists rather than being a packaging preference. If a service ever did need one, this grep would fail the build, and that is the right outcome: an unverified module inside a verified crate should be excluded by the build, not waved through by an attribute.

Repository layout

jetstream_distributed/
├── Cargo.toml              one crate (plus the vendored pmemlog); the services are behind the `service` feature (on by default; the proofs build without it)
├── rust-toolchain.toml
├── README.md
├── fuzz/                   the coverage-guided front end to the protocol-line search (its own workspace, nightly)
├── src/
│   ├── lib.rs
│   ├── protocol_t.rs       the Protocol trait: the labelled-step shape every model has
│   ├── protocol_v.rs       each model's instance is its model (next, init); the mailbox run is a run of the protocol
│   ├── temporal_t.rs       leads-to, weak fairness and WF1: what a liveness proof is stated in
│   ├── ownership/          exclusive mutable ownership with epoch fencing
│   │   ├── model_t.rs      state space + transition relation (no specification)
│   │   ├── spec_t.rs       may_mutate, tokens, the system invariant
│   │   ├── fencing_t.rs    current_epoch, valid_fence, staleness
│   │   ├── transfer_v.rs   the multi-step handover and its lemmas
│   │   ├── steps_v.rs      the transitions as executable u64 functions
│   │   ├── exec_v.rs       the u64 fence check a node runs on its own belief
│   │   ├── registry_v.rs   RegistryCore: the record, the grants published, the writes; one method per step
│   │   ├── service.rs      the protocol over Jetstream RPC   [feature = "service"]
│   │   └── proofs/
│   │       ├── invariant_v.rs    init ==> inv, inv /\ next ==> inv, reachable ==> inv
│   │       ├── properties_v.rs   structural, temporal and capability properties
│   │       ├── exclusivity_v.rs  claim 1
│   │       ├── fencing_v.rs      claims 2, 3, 5
│   │       ├── transfer_v.rs     claim 4
│   │       ├── tokens_v.rs       claim 6
│   │       ├── adversarial_v.rs  concrete adversarial executions
│   │       ├── refinement_v.rs   steps_v.rs agrees with the model's tr_* transitions
│   │       └── registry_v.rs     the registry's record, grants included, takes the model's steps
│   ├── raymond/            Raymond's mutual-exclusion routing layer
│   │   ├── model_t.rs
│   │   ├── steps_v.rs      the routing decisions as executable u64 functions
│   │   ├── exec_v.rs       RayTable: the routing record as verified code, one method per step
│   │   ├── service/        the protocol over Jetstream RPC   [feature = "service"]
│   │   │   ├── mod.rs      the Routing trait and what a node can see of itself
│   │   │   ├── router.rs   the whole routing record, behind one lock
│   │   │   └── refusal.rs  the refusals, in the line protocol's alphabet
│   │   └── proofs/{routing_layer_v.rs, routing_run_v.rs, refinement_v.rs}
│   ├── composed/           ownership and Raymond as one machine
│   │   ├── model_t.rs      the coupling enforced by guards, not assumed
│   │   ├── steps_v.rs      the coupling guards as executable functions
│   │   ├── exec_v.rs       the four coupled steps over the layers' records, and the debts
│   │   ├── service/        the two layers behind one coordinator [feature = "service"]
│   │   │   ├── mod.rs      the Composed trait: ownership + routing + the coupling
│   │   │   ├── command.rs  the coupling's four steps as data, and `apply`, the dispatch to the verified steps
│   │   │   ├── coordinator.rs  both layers, and the gate that serialises them
│   │   │   └── refusal.rs  the refusals, in the line protocol's alphabet
│   │   └── proofs/{coupling_v.rs, epoch_v.rs, scenario_v.rs, refinement_v.rs, exec_v.rs}
│   ├── actor/              a distributed actor: a journal fenced by ownership
│   │   ├── model_t.rs      envelopes, the journal, send / accept, the fold that is the state
│   │   ├── steps_v.rs      accept, send and the behaviour as executable u64 functions
│   │   ├── mailbox/        the queue in front of the actor, and its wakeup protocol
│   │   │   ├── model_t.rs  the three flags, six steps, and the step boundaries between them
│   │   │   ├── exec_v.rs   MailboxCore: the protocol as verified code, one method per step
│   │   │   └── proofs/
│   │   │       ├── invariant_v.rs  the six-clause invariant, and that every step preserves it
│   │   │       ├── safety_v.rs     nothing lost or repeated; per-sender order; no gaps
│   │   │       ├── liveness_v.rs   a message enqueued is a message processed, under fairness
│   │   │       ├── refinement_v.rs the executable core takes the model's steps, and refuses where it cannot
│   │   │       └── scenario_v.rs   a fair run that delivers; an unfair one that does not
│   │   ├── service/        the actor over Jetstream RPC   [feature = "service"]
│   │   │   ├── mod.rs      the Actor trait and what goes on the wire
│   │   │   ├── host.rs     the journal, the sent set, and the registry that fences them
│   │   │   ├── transport.rs Host::serve and Connection::new over any byte stream; Host::pipe in memory
│   │   │   ├── mailbox.rs  the mailbox protocol on real threads: Mailbox, Permit, Capacity, Round
│   │   │   ├── session.rs  Session (a ClientTransport over a mailbox) and serve (the drain)
│   │   │   └── refusal.rs  the refusals, in the line protocol's alphabet
│   │   ├── examples/
│   │   │   └── basic.rs    two actors, each behind its own mailbox, one calling the other
│   │   └── proofs/
│   │       ├── journal_v.rs      counting and folding over push and take
│   │       ├── invariant_v.rs    the six-clause invariant, and that every step preserves it
│   │       ├── exclusive_v.rs    one host at a time; nothing written under a superseded epoch
│   │       ├── delivery_v.rs     each message once, in order, none invented
│   │       ├── state_v.rs        append-only; the state is a fold and survives a handover
│   │       ├── refinement_v.rs   steps_v.rs agrees with the model's transitions
│   │       └── scenario_v.rs     a run through a whole handover, and the refusals at its end
│   ├── raft/               consensus: terms, votes, quorums, the log
│   │   ├── model_t.rs      state space + transition relation
│   │   ├── steps_v.rs      the election decisions as executable u64 functions
│   │   ├── exec_v.rs       ElectionCore: role, term, vote and tally as verified code, one method per step
│   │   ├── store_v.rs      a log that truncates, on a device that cannot
│   │   ├── wire_v.rs       the record encoding, and what a torn write leaves
│   │   ├── service.rs      the protocol over Jetstream RPC   [feature = "service"]
│   │   └── proofs/
│   │       ├── election_v.rs     Election Safety, via quorum intersection
│   │       ├── election_core_v.rs the election record takes the model's steps, vote and tally included
│   │       ├── history_v.rs      the ghost record, and Log Matching out of it
│   │       ├── log_v.rs          what one replication step gives you (and what it does not)
│   │       ├── terms_v.rs        term structure, entry durability, the election restriction
│   │       ├── commit_v.rs       what was committed, and State Machine Safety minus one hypothesis
│   │       ├── votes_v.rs        what a vote was a judgement of
│   │       ├── summary_v.rs      the summary a voter judged, tied back to the log it summarised
│   │       ├── persistence_v.rs  why the entry was still there when the voter judged it
│   │       ├── refinement_v.rs   steps_v.rs agrees with the model's tr_* transitions
│   │       ├── scenario_v.rs     a run in which an election actually happens
│   │       ├── store_v.rs        recovery is exact; a crash can only rewind
│   │       └── wire_v.rs         cut the bytes anywhere; a record prefix comes back
│   ├── hyparview/          membership by two small views: one node, so far
│   │   ├── model_t.rs      the views, the four handlers, the messages they send
│   │   ├── exec_v.rs       HvTable: the views as verified code; each handler is a step of the model
│   │   └── proofs/invariant_v.rs   the views stay bounded, disjoint, free of the node itself
│   └── swim/               gossip membership: merge, not majority
│       ├── model_t.rs      the record, the merge rule, one transition
│       ├── steps_v.rs      the merge and the refutation as executable u64 functions
│       ├── exec_v.rs       SwimTable: the node's table as verified code, learn and hear
│       ├── service/        the protocol over Jetstream RPC   [feature = "service"]
│       │   ├── mod.rs          the Membership trait and what goes on the wire
│       │   ├── node.rs         the table, and the merge into it
│       │   └── refusal.rs      the refusals, in the line protocol's alphabet
│       └── proofs/
│           ├── merge_v.rs      idempotent, absorbs a repeat, never regresses, commutative, associative
│           ├── monotone_v.rs   lifted through a step and then through a run
│           ├── refinement_v.rs steps_v.rs agrees with the model's tr_gossip
│           └── table_v.rs      the table learns by tr_gossip; a refutation is a second one
├── tests/
│   ├── scenario_body/mod.rs    the executable protocol + the runtime oracles
│   ├── turmoil_ownership.rs    named stories, each with an expected ending
│   ├── turmoil_scenarios.rs    the blind seed search + the regression replay
│   ├── protocol_lines.rs       the search over what arrives at the registry
│   ├── ownership_handover.rs   the service's headline story   [feature = "service"]
│   ├── ownership_durability.rs the restart that must not rewind [feature = "service"]
│   ├── raft_election.rs        a split vote elects one leader  [feature = "service"]
│   ├── raft_log.rs             the consistency check and figure 8 [feature = "service"]
│   ├── raft_wire.rs            the service over a simulated network [feature = "service"]
│   ├── actor_journal.rs        the guarantees over a Jetstream session, and every refusal [feature = "service"]
│   ├── actor_turmoil.rs        an actor changes hands across hosts, nothing lost or repeated [feature = "service"]
│   ├── actor_mailbox.rs        A calls B through a mailbox, backpressure, abort and close [feature = "service"]
│   ├── raymond_routing.rs      the textbook request path, and every refusal [feature = "service"]
│   ├── raymond_turmoil.rs      the same path across hosts, on a simulated network [feature = "service"]
│   ├── composed_handover.rs    the coupling: no move while held, no acquire without it [feature = "service"]
│   ├── composed_turmoil.rs     the privilege moves only after the release, across hosts [feature = "service"]
│   ├── swim_membership.rs      the merge rule in every order, and the refutation [feature = "service"]
│   ├── swim_turmoil.rs         a suspicion crosses a healed partition and is refuted [feature = "service"]
│   └── seeds/scenarios.txt     seeds that once broke something
├── vendor/
│   ├── README.md               provenance, what is built, and pmemlog's six assumptions
│   ├── verified-storage/       Microsoft's verified-storage, whole and verbatim (CI diffs it)
│   │   ├── pmemlog/            the verified persistent-memory log [verified by CI]
│   │   ├── multilog/           logs with atomic appends across them [not yet built]
│   │   ├── capybaraKV/         a persistent-memory key-value store [not yet built]
│   │   └── ...                 capybaraNS, soundness_proofs, unverified, LICENSE.txt
│   └── kverus/                 the KVerus agent skills, verbatim (CI diffs it)
│       ├── README.md           provenance, and which skills edit code
│       └── skills/             kverus-review, kverus-eval, ... : what AGENTS.md's reviews follow
├── AGENTS.md                   build and verify commands, the rules, and how to review a change
└── .github/workflows/verify.yml

One directory per algorithm, and each one holds the whole of that algorithm — its model, its proofs, its executable steps and its service. A protocol whose proof lived in one crate and whose implementation lived in another is a protocol where the two can drift without anything noticing; here they are compiled together and the service calls the functions the proofs are about.

The services are behind a service feature, which is on by default so that depending on the crate gives you them, and that feature is what makes one crate workable. verus --crate-type=lib src/lib.rs does not read features, and cargo verus verify --no-default-features turns it off, so the verified build’s dependency graph is vstd and nothing else — no Jetstream, no async runtime for Verus to be asked about, and no need for a single #[verifier::external] to keep service code out of the proofs. With the feature on, the same modules compile against the same verified step functions, under cargo +stable: rust-toolchain.toml pins the Rust release the Verus build was made against so the proofs verify, not so a service is stuck on it.

This differs from a plain proofs/ directory at the repository root: Verus verifies a crate, so every proof file has to be a module of that crate. Keeping them under src/{algorithm}/proofs/ is the ordinary Rust way to express that; a top-level proofs/ would need #[path = "../proofs/..."] attributes for no benefit.

File names follow the verified-storage convention the vendored code uses: a _t.rs file is trusted — the model, the specification, the definitions a claim is stated in, which a reader has to audit because no proof checks them against anything — and a _v.rs file is verified: executable code and proofs, which Verus checks. service/ is plain Rust that Verus never sees and carries no suffix. The suffix is on the file; the module keeps its plain name (#[path = "model_t.rs"] pub mod model;), so crate::raft::model::tr_timeout is still where it was.

Verified executable code is in the steps_v.rs, exec_v.rs and, where an algorithm keeps state, registry_v.rs-style files of each algorithm: small u64-valued functions and the records they act on, each with a postcondition stated in terms of that algorithm’s model and a theorem in its proofs/refinement_v.rs (or the proof file named for the record) discharging it. Unverified executable code is in each algorithm’s service.rs and under tests/, and it is unverified in the plain sense that Verus never compiles it — the feature is off when the proofs are checked — not in the sense that an escape hatch waves it through. exec offers queries only: a FenceGuard has private fields, a single constructor and no setter, so its ghost view is fixed at construction. Were it mutable — by a bump method or by assigning to a public field — its view could drift from Owned(A, e) to Owned(B, e + 1), exactly the atomic ownership assignment this model refuses to admit. Observing a new generation means constructing a new guard. Making a guard follow the protocol needs a refinement of the node side; the registry side is src/ownership/steps_v.rs. Everything else in the crate is specification or proof.

Specification and proof code are kept apart from the model: src/ownership/model_t.rs defines only the state space and the transition relation and does not import the specification layer, so a specification cannot be quietly weakened to fit the model.

Verifying locally

# 1. Install the Rust toolchain that the pinned Verus release was built against
rustup toolchain install 1.98.1-x86_64-unknown-linux-gnu \
  --component rustc-dev,llvm-tools,rust-std,cargo,rustfmt

# 2. Download the pinned Verus release
VERUS=0.2026.09.20.aef82ed
curl -fL -o verus.zip \
  "https://github.com/verus-lang/verus/releases/download/release%2F${VERUS}/verus-${VERUS}-x86-linux.zip"
unzip -q verus.zip && export PATH="$PWD/verus-x86-linux:$PATH"

# 3. Verify
verus --crate-type=lib src/lib.rs

CI (.github/workflows/verify.yml) runs exactly this on every push and pull request, so a PR fails if any proof stops verifying.

A second job runs the same crate through cargo verus verify, which checks it against the vstd version pinned in Cargo.toml rather than the prebuilt one inside the Verus release. That entry point needs

[package.metadata.verus]
verify = true

in Cargo.toml: without it, cargo verus verify compiles this crate with ordinary rustc, verifies only vstd, prints vstd’s verification results line and exits 0. It is a false green that survives a naive grep for the summary, because a summary is present — just not this crate’s. The CI step therefore requires a summary emitted after Cargo starts compiling this crate. It runs with --no-default-features, since service is a default feature and the proof build should not pull Jetstream and tokio in.

A third job, pmemlog proof check, verifies the vendored persistent-memory log (vendor/verified-storage/pmemlog) the same way, and checks that the vendored tree is byte-for-byte Microsoft’s at the pinned commit. See vendor/README.md.

The services and the simulated-network tests are not verified, only run:

cargo test                          # the services, tests/, and the unit tests
cargo run --example actor_basic     # two actors behind mailboxes