Formal Verification of a Distributed Dynamic Reconfiguration Protocol

TL;DR

This paper provides a formal, machine-checked safety proof of MongoRaftReconfig, a dynamic reconfiguration protocol for MongoDB based on Raft, ensuring its safety properties through TLA+ verification.

Contribution

First formal inductive invariant and safety proof for a Raft-based dynamic reconfiguration protocol using TLA+ and TLAPS.

Findings

Formal proof of LeaderCompleteness property

Formal proof of StateMachineSafety property

First machine-checked safety verification for such protocols

Abstract

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.