Formal Verification of Consensus in the Taurus Distributed Database

Distributed database services are an increasingly important part of cloud computing. They are required to satisfy several key properties, including consensus and fault tolerance. Given the highly concurrent nature of these systems, subtle errors can arise that are difficult to discover through traditional testing methods. Formal verification can help in discovering bugs and ensuring correctness of these systems. In this paper, we apply formal methods to specify and verify an industrial distributed database, Taurus, which uses a combination of several fundamental protocols, including Multi-Version Concurrency Control and Raft-based Cluster Management. TLA(+) is used to model an abstraction of the system and specify its properties. The properties are verified using the TLC model checker, as well as by theorem proving using the TLA proof system (TLAPS). We show that model checking is able to reproduce a bug in Taurus that was found during testing. But our most significant result is twofold: we successfully verified an abstract model of Taurus, and convinced our industrial partners of the usefulness of formal methods to industrial systems.