Distributed Systems Research Group
Research in distributed systems particularly by applying formal methods to database design and performance.
Who We Are
We’re committed to improving the correctness, reliability, and efficiency of distributed systems using principled approaches and lightweight formal modeling. We multiply our impact by disseminating research and technology throughout MongoDB and the industry.
_Spot.svg)
Research Areas
Distributed protocols for modern cloud infrastructure
Precisely synchronized clocks, advanced networking, and other technologies are now widely available in the cloud. We research the use of these modern technologies to improve the consistency and performance of distributed protocols.
Formal methods for protocol design and verification
Formal methods and automated reasoning techniques allow for mathematical guarantees of correctness and durability for distributed protocols. Formal modeling also enables model-based verification approaches for verifying complex implementations against high-level abstract specifications.
Fault tolerance in distributed systems
Minor faults in complex systems can trigger cascading failures, leading to prolonged outages and degraded performance. We study fault-tolerance challenges, including metastable failures, to enhance system resilience and reliability.
Our Team
Research Papers
LeaseGuard: Raft Leases Done Right
A. Jesse Jiryu Davis, Lingzhi Deng, Murat Demirbas, SIGMOD, 2026LeaseGuard is a novel, robust Raft leader-lease protocol that ensures strongly consistent reads with zero network overhead while significantly improving availability during leader elections.
Design and Modular Verification of Distributed Transactions in MongoDB
William Schultz, Murat Demirbas, VLDB, 2025In this paper, we describe our experience using modular formal specification techniques in the design and verification of MongoDB’s distributed transactions protocol. We formally specify the protocol and its interface with the underlying storage layer, allowing us to verify high-level protocol properties while also formalizing the contract between these two components. This modular approach also enables an automated, model-based verification technique for testing conformance of the WiredTiger storage implementation to this interface. We also formally analyze permissiveness–how well a transaction protocol maximizes concurrency within a given isolation level–a property not previously examined.
Formal verification of a distributed dynamic reconfiguration protocol
William Schultz, Ian Dardik, Stavros Tripakis, CPP, 2022In this work, we present a formal, machine-checked TLA+ safety proof of the logless dynamic reconfiguration protocol used in the MongoDB replication system. This proof is formalized in the TLA+ proof system (TLAPS) and constitutes the first machine-checked safety proof of a Raft-based reconfiguration protocol.
Design and Analysis of a Logless Dynamic Reconfiguration Protocol
William Schultz, Siyuan Zhou, Ian Dardik, Stavros Tripakis, OPODIS, 2021In this paper, we present a novel dynamic reconfiguration protocol for the MongoDB replication system. The protocol utilizes a logless approach to managing configuration state and decouples the processing of configuration changes from the main database operation log. We provide a safety proof of the protocol, along with a formal specification in TLA+.
eXtreme Modelling in Practice
A. Jesse Jiryu Davis, Max Hirschorn, Judah Schvimer, VLDB, 2020In this paper, we explore model-based testing as a tool for ensuring specification-implementation conformance in complex components of MongoDB. We attempted two case studies: model-based trace-checking (MBTC) in the MongoDB server’s replication protocol and model-based test-case generation (MBTCG) in MongoDB Realm Sync’s operational transformation algorithm. We analyze why one technique succeeded and the other failed and advise future implementers making similar attempts at model-based testing.