Design and Modular Verification of Distributed Transactions in MongoDB

Summary: Modular formal specifications verify MongoDB’s distributed transaction protocol and its contract with WiredTiger’s snapshot-isolated engine. Explicit-state model checking generates conformance tests for the storage implementation and enables analysis of isolation and permissiveness. (summarized by gpt-5.6-luna on Jul 24 2026)

Paper ID: 14294
Venue: VLDB
Year: 2025
Pagerank: 5.093636e-05
Overall Rank: 11,010 | 24.47%
DOI: 10.14778/3750601.3750626

Incoming Non-self Citations Over Time

No non-self incoming citations found for this paper in this database.

Authors

1. William Schultz (MongoDB)
2. Murat Demirbas (MongoDB)

BibTeX Citation

@article{schultz_vldb25,
        title = {{Design and Modular Verification of Distributed Transactions in MongoDB}},
        author = {Schultz, William and Demirbas, Murat},
        journal = {PVLDB},
        series = {{VLDB} '25},
        volume = {18},
        number = {12},
        pages = {5045--5058},
        doi = {10.14778/3750601.3750626},
        url = {https://doi.org/10.14778/3750601.3750626},
        year = {2025}
}

Incoming Citations (Sorted by Pagerank)

Showing 0 of 0 citing papers.

Rank	Citing Paper	Year	Venue	Pagerank

Outgoing Citations (Sorted by Pagerank)

Showing 12 of 12 cited papers.

Citations counted here include only citations to other VLDB/SIGMOD/CIDR/PODS papers in this database.

Rank	Cited Paper	Year	Venue	Pagerank
19	A Critique of ANSI SQL Isolation Levels	1995	SIGMOD	0.00058720861
57	Calvin: Fast Distributed Transactions for Partitioned Database Systems	2012	SIGMOD	0.00040139242
144	Megastore: Providing Scalable, Highly Available Storage for Interactive Services	2011	CIDR	0.00029554682
208	CockroachDB: The Resilient Geo-Distributed SQL Database	2020	SIGMOD	0.00024968157
245	Serializable Isolation for Snapshot Databases	2008	SIGMOD	0.00023458287
271	TiDB: A Raft-based HTAP Database	2020	VLDB	0.00022703024
1,080	Elle: Inferring Isolation Anomalies from Experimental Observations	2021	VLDB	0.00012257972
1,463	Amazon Aurora: On Avoiding Distributed Consensus for I/Os, Commits, and Membership Changes	2018	SIGMOD	0.00010700936
2,368	What Are We Doing With Our Lives? Nobody Cares About Our Concurrency Control Research	2017	SIGMOD	8.6827828e-05
3,418	Implementation of Cluster-wide Logical Clock and Causal Consistency in MongoDB	2019	SIGMOD	7.429422e-05
4,523	Tunable Consistency in MongoDB	2019	VLDB	6.6463056e-05
7,481	eXtreme Modelling in Practice	2020	VLDB	5.6078973e-05

Semantically Similar Papers

#	Overall Rank	Paper	Year	Venue
1	13,232	Specification and Verification of Abstract Database Types	1984	PODS
2	14,533	Transactions Modeling	1982	SIGMOD
3	5,194	Cooperative Transaction Hierarchies: A Transaction Model to Support Design Applications	1990	VLDB
4	13,079	Ensuring Transaction Atomicity in Multidatabase Systems	1992	PODS
5	6,983	Ensuring Relaxed Atomicity for Flexible Transactions in Multidatabase Systems	1994	SIGMOD
6	14,121	Correctness in General Configurations of Transactional Components	1999	PODS
7	3,418	Implementation of Cluster-wide Logical Clock and Causal Consistency in MongoDB	2019	SIGMOD
8	4,523	Tunable Consistency in MongoDB	2019	VLDB
9	7,288	Adapting TPC-C Benchmark to Measure Performance of Multi-Document Transactions in MongoDB	2019	VLDB
10	7,481	eXtreme Modelling in Practice	2020	VLDB