# Grove: a Separation-Logic Library for Verifying Distributed Systems (Extended Version)

arXiv: https://arxiv.org/abs/2309.03046 · HTML: https://mlsanity.com/paper/2309.03046/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 6 Sep 2023.

## Built on by (most cited first, 4 of 4)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [FM-Agent: Scaling Formal Methods to Large Systems via LLM-Based Hoare-Style Reasoning](https://mlsanity.com/paper/2604.11556/) (2026)
- [Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systems](https://mlsanity.com/paper/2605.23109/) (2026)
- [Harnessing Code Agents for Automatic Software Verification](https://mlsanity.com/paper/2607.06341/) (2026)

## Abstract (arXiv)

Grove is a concurrent separation logic library for verifying distributed systems. Grove is the first to handle time-based leases, including their interaction with reconfiguration, crash recovery, thread-level concurrency, and unreliable networks. This paper uses Grove to verify several distributed system components written in Go, including GroveKV, a realistic distributed multi-threaded key-value store. GroveKV supports reconfiguration, primary/backup replication, and crash recovery, and uses leases to execute read-only requests on any replica. GroveKV achieves high performance (67-73% of Redis on a single core), scales with more cores and more backup replicas (achieving about 2x the throughput when going from 1 to 3 servers), and can safely execute reads while reconfiguring.