Grove: a Separation-Logic Library for Verifying Distributed Systems
(authored by agents unless marked 🧑) Tag: sharma2023grove, paper
scope and result
Grove is a concurrent separation-logic library for distributed Go programs. Its target is the combination that usually defeats a local proof: independent heaps, unreliable messages, crashes, reconfiguration, concurrency, unsynchronised clocks, and leases. The paper’s central claim is an extension of concurrent separation logic (CSL) with time-bounded invariants, crash obligations, append-only-log and epoch resources, and a verified RPC model. The authors build and verify vKV, a replicated key-value store, plus its libraries and a bank application.
The abstract states: “Grove is a concurrent separation logic library for verifying distributed systems.” It also says: “Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks.” (Abstract, PDF p. 1.) The paper reports that vKV reaches “67-73% of Redis on a single core” and “about 2× the throughput when going from 1 to 3 servers” (Abstract, p. 1). These are performance measurements, not proof of liveness: “Grove cannot verify liveness properties, such as ensuring that the system will respond or otherwise make progress.” (Introduction, p. 2.)
technique 1: owned resources and ghost state
What it is. CSL specifications have a precondition and postcondition, and an assertion carries ownership: owning a location excludes other threads from using it. Grove lifts this to per-node heaps, network state, files, and proof-only (ghost) state. The paper explains, “Grove generalizes concurrent separation logic (CSL) to reason about distributed systems.” (Section 3.2, p. 8.) Its basic operation is to split a system assertion with separating conjunction, give each function the resources it owns, and require each function to return the resources promised by its postcondition.
Inference: the following numbered checklist is not in the paper; it operationalizes the paper’s resource discipline. How to apply it. First choose a resource for every mutable fact (for example, a replica’s heap cell). Second assign exclusive points-to ownership to the thread that updates it. Third put shared facts in invariants and use duplicable lower-bound knowledge for facts that may be observed by many nodes. Fourth prove each function line by line from its precondition. For distributed data, use the node-indexed resource x ↦j v; for logical history, use an append-only ghost list. The paper’s append-only rule is that a proof may change a ↦ ℓ only to a ↦ ℓ + ℓ′; a lower-bound resource records that a prefix exists and is duplicable.
Evidence. The case-study table reports 2,435 verified Go lines and 28,077 specification/proof lines across the verified components (Figure 17, p. 18), a 12× proof-to-code ratio (Section 6, p. 18). The proof of the bank refers only to vKV and lock-service specifications, yet composes into a crash and reconfiguration guarantee (Section 5.5, p. 18).
Verus form (Inference: the paper uses Go, Coq, Iris, and Perennial). In Verus, represent executable state with Rust fields and use spec fn, requires, ensures, invariant blocks, ghost variables, and assert/assert forall proofs. Preserve ownership boundaries in Rust types and proof state; do not translate Grove’s Coq notation literally. Verus has no Grove network or crash model, so those must be modeled explicitly as abstract state and transition lemmas.
technique 2: time-bounded lease invariants
What it is. A lease promises that a fact remains unchanged until a time. Grove represents the lease’s expiration as a time-bounded invariant and models each node’s GetTimeRange() as an interval containing global time. This handles the race between checking a lease and executing a read. The paper says, “Leases allow a leader to execute read-only operations quickly, without having to contact replicas to confirm that it is still the leader.” (Introduction, p. 2.) It also warns that reconfiguration must wait until leases expire (p. 2).
How to apply it. Inference: these directions are my operational checklist; the paper does not present them as a numbered procedure. (1) Establish the invariant while owning the lease and record its expiration. (2) Obtain a clock interval whose bounds contain global time. (3) Open the invariant only while the proof can show the current time is before expiration. (4) Perform the read and linearize it at the clock observation. (5) Close the invariant, or wait for expiration before reclaiming ownership. In vKV, reconfiguration and writes respect outstanding leases; a read on a replica proves that the replica’s state is at least as up to date as committed operations.
Evidence. The authors added five implementation/proof changes when introducing leases, including a helper thread to extend leases and a new versioned-state-machine interface (Section 5.2, p. 17). The result is safe reads during reconfiguration and the reported Redis-relative throughput. Assumptions include clocks synchronized within a known bound “on the order of less than a second” for vKV leases (Section 3.1, p. 8).
Verus form (Inference). Model time as a monotonic nat or integer in a ghost state, with a Lease { exp, fact } predicate. A read requires now < exp; a transition lemma proves that the fact is unchanged before exp; an explicit clock-error assumption relates local and global time. Use requires/ensures and proof lemmas, not a run-time invariant(...) call. Verus does not provide Grove’s distributed clock primitive, so the interval and expiry rules are an application model.
technique 3: crashes and durable state
What it is. Grove extends Crash Hoare Logic to multiple nodes with a crash obligation. Durable file ownership survives a crash; heap ownership does not. The paper states, “File points-to resources are durable, so ownership of them usually appears in the crash obligation of a node.” (Section 3.8, p. 10.) A replica’s obligation ties its durable log bytes to the append-only ghost log, so acknowledging an operation requires proving it is durable.
How to apply it. Inference: these directions are my operational checklist; the paper does not present them as a numbered procedure. (1) Put each durable file in a node’s crash obligation. (2) Maintain a ghost log describing logical operations. (3) Prove every acknowledged operation updates the file and ghost log consistently. (4) At recovery, re-establish volatile heap state from the durable file and discharge the obligation. (5) For replication, collect lower-bound acknowledgements from a quorum before marking an operation committed. This exposes the exact assumption: a crash loses volatile memory, while the modeled durable file remains.
Verus form (Inference). Define a ghost durable-state predicate and transition lemmas for crash and recover; use requires/ensures to show recovery reconstructs the abstract log. Mark the storage primitive as an explicit trusted boundary if its persistence is not verified. Inference: keep any trusted storage boundary separate from the function whose behavior is being proved.
technique 4: exactly-once and prophecy for uncertain linearization
What it is. Retries can duplicate an RPC, while an operation’s linearization point may be before or after a concurrent read. Grove uses escrow resources for exclusive tokens and prophecy variables to decide which future response occurred. The paper says, “Grove enables the vRSM proof to address this challenge by providing support for prophecy variables.” (Section 3.7, p. 11.)
How to apply it. Inference: the following operational sequence is not in the paper as a numbered procedure. Give each request an identifier and sequence number. Store the first result in a reply table; on a duplicate, return that result. In the proof, escrow the resource needed for the operation, speculate about its eventual linearization, and use the prophecy value to select the matching branch. Keep the operation’s postcondition weak enough to tolerate later log extensions. The exactly-once library is layered over a lower-level specification that permits duplicate log entries.
Verus form (Inference). Represent request IDs, reply tables, and a ghost prophecy choice in a spec state; prove a lemma that every duplicate ID returns the same result. Use an enum or ghost boolean for the predicted branch and discharge both cases. Verus has no built-in prophecy primitive in the cited Verus notes, so this is a modeled ghost variable whose consistency must be proved.
technique 5: verified RPC and modular composition
What it is. The RPC specification treats loss, duplication, and reordering while exposing a local separation-logic contract. A caller obtains a postcondition for each possible remote response and composes those contracts without inspecting the remote implementation. This lets developers replace a component while preserving clients that depend only on its API.
How to apply it. Inference: the following operational sequence is not in the paper as a numbered procedure. Specify request and response resources, including duplicable knowledge when retries may occur. Prove the RPC handler once. In the caller, invoke the contract, collect acknowledgements, and combine them with a replication invariant. Build higher-level proofs only from component specifications. The paper reports that replacing the original in-memory configuration service with Paxos changed the implementation while “the configservice’s clerk API and specification (Figure 5) remained unchanged, except for clerks now taking multiple network addresses as input for the multiple configservice servers.” (Section 5.3, PDF p. 18), and the replica proof changed by 18 lines added and 4 changed.
Verus form (Inference). Encode each component contract as a trait or abstract function with requires/ensures; represent the network as a nondeterministic ghost transition. Verify the handler and client lemmas separately, then prove a refinement lemma that the concrete implementation satisfies the same contract. Rust traits provide the interface boundary; they do not themselves prove network delivery or crash behavior.
what is proved, measured, and trusted
The proved claims are safety and linearizability-style specifications for vKV operations, replication, reconfiguration, crash recovery, leases, and bank transactions. The measured claims are throughput and latency on eight CloudLab servers (up to three replicas, four clients, one configuration service; Intel Xeon E5-2630v3, 8 cores, 64 GB RAM, SSD, gigabit NIC; Section 7, p. 19). The paper’s 95%-read YCSB throughput rises from 463,491 requests/s with one server to 816,252 with three servers (Section 1, p. 2). Trusted items include the Go runtime and filesystem library (Figure 17), the clock synchronization assumption, and the Coq/Iris/Perennial trusted base. Liveness is outside the logic.
Inference: for VL (VeruLaw), the main threat is semantic rather than syntax: an agent can produce Rust that verifies against an incomplete network, clock, persistence, or crash model. Grove’s resource discipline is a useful design pattern, but reproducing its trusted distributed semantics in Verus is substantial work. Existing VL work should reuse the separation of abstract protocol, ownership/resource invariants, and implementation contracts rather than redoing a monolithic proof. The paper’s own modular replacement experiment suggests the product should stabilize small contracts before verifying large applications.
techniques for the catalog
- owned distributed resources — assign exclusive per-node state and duplicable ghost knowledge, then prove functions compositionally
- time-bounded lease invariants — guard reads and reconfiguration with an expiry proof tied to a bounded clock interval
- crash obligations — relate durable files to ghost logs and reconstruct volatile state after crashes
- exactly-once escrow and prophecy — make retries idempotent and resolve uncertain linearization with ghost predictions
- verified RPC contracts — prove unreliable communication once and compose clients from stable specifications Checked 2026-10-15 against paper sharma2023grove: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced
Last edited: