# Formal Verification of a Distributed Dynamic Reconfiguration Protocol

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 24 Sep 2021.

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

- [TLA-Verus: Generating and Solving Temporal Proof Obligations with LLM Agents](https://mlsanity.com/paper/2610.14923/) (2026)

## Abstract (arXiv)

We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and implemented in MongoDB, a distributed database whose replication protocol is derived from the Raft consensus algorithm. We present an inductive invariant for MongoRaftReconfig that is formalized in TLA+ and formally proved using the TLA+ proof system (TLAPS). We also present a formal TLAPS proof of two key safety properties of MongoRaftReconfig, LeaderCompleteness and StateMachineSafety. To our knowledge, these are the first machine checked inductive invariant and safety proof of a dynamic reconfiguration protocol for a Raft based replication system.