From 18f86c13106305302b0cad4a95980f7beb6696d2 Mon Sep 17 00:00:00 2001 From: William Schultz Date: Wed, 10 Sep 2025 14:31:18 -0400 Subject: [PATCH 1/4] Add draft of MongoDB section on industrial use of TLA+ --- content/industry/index.md | 43 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/content/industry/index.md b/content/industry/index.md index c75f3ad..3c10136 100644 --- a/content/industry/index.md +++ b/content/industry/index.md @@ -120,6 +120,49 @@ We couldn't imagine that this would have been discovered through any of our test However, a candidate's knowledge of TLA⁺ is given significant weight in our evaluation. To us, it is a great indicator of those who really care about quality and correctness. +## MongoDB + +MongoDB engineers have applied TLA⁺ to core protocols within the MongoDB database over several years, as early as 2015, including distributed replication, dynamic reconfiguration, and distributed transactions. These are complex and highly concurrent protocols and systems, where testing alone is often not sufficient to catch and reproduce subtle design bugs. + +MongoDB engineers [emphasized](https://youtu.be/x9zSynTfLDE?feature=shared&t=73) the value derived from TLA⁺ in their experience specifying and model checking their core consensus protocol: + +> Without a formal model, it’s nearly impossible to get a complex distributed protocol right. TLA⁺ and TLC are tools that make this possible for practicing software engineers...Even very simple and abstract models can help catch non-trivial bugs. +> + +and in a [post](https://www.mongodb.com/company/blog/technical/rapid-prototyping-safe-logless-reconfiguration-protocol-mongodb-tla-plus) about their specification-driven redesign of a [novel dynamic reconfiguration protocol](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2021.26): + + +> Model checking is an excellent tool for rapidly and precisely answering "what if" design questions. Our efforts also emphasized an important feature of lightweight, design-level formal methods techniques, which is about more than simply ensuring correctness of your system design. Rather, it enables the exploration of protocol optimizations at a level of aggressiveness and velocity that would typically be infeasible with manual design methods. From this perspective, we can view these formal methods tools as not only a means for improving correctness of our systems and protocols, but as a means for efficient exploration of the optimization design space while maintaining a high correctness bar. + +They have also employed TLA⁺ for model-based trace checking and for modular specification and model-based verification of distributed transactions, writing about their experiences in several papers: + +> +> [**Extreme Modeling in Practice**](https://dl.acm.org/doi/10.14778/3397230.3397233) +> +> A. Jesse Jiryu Davis, Max Hirschorn, Judah Schvimer +> +> VLDB 2020 +> +>   +> +> [**Fault-Tolerant Replication with Pull-Based Consensus in MongoDB**](https://www.usenix.org/conference/nsdi21/presentation/zhou) +> +> Siyuan Zhou, Shuai Mu +> +> NSDI 2021 +> +> +>   +> +> [**Design and Modular Verification of Distributed Transactions in MongoDB**](https://www.vldb.org/pvldb/vol18/p5045-schultz.pdf) +> +> William Schultz, Murat Demirbas +> +> VLDB 2025 +> + + + ## OpenComRTOS The European Space Agency's *Rosetta* spacecraft, which flew to a comet, used a real-time operating system called *Virtuoso* to control some of its instruments. From c1abe7956b5102dfa532bd0f57fa1ac69ed25611 Mon Sep 17 00:00:00 2001 From: William Schultz Date: Wed, 10 Sep 2025 17:24:16 -0400 Subject: [PATCH 2/4] Minor edits --- content/industry/index.md | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/content/industry/index.md b/content/industry/index.md index 3c10136..5bcaef4 100644 --- a/content/industry/index.md +++ b/content/industry/index.md @@ -125,18 +125,17 @@ To us, it is a great indicator of those who really care about quality and correc MongoDB engineers have applied TLA⁺ to core protocols within the MongoDB database over several years, as early as 2015, including distributed replication, dynamic reconfiguration, and distributed transactions. These are complex and highly concurrent protocols and systems, where testing alone is often not sufficient to catch and reproduce subtle design bugs. MongoDB engineers [emphasized](https://youtu.be/x9zSynTfLDE?feature=shared&t=73) the value derived from TLA⁺ in their experience specifying and model checking their core consensus protocol: - + > Without a formal model, it’s nearly impossible to get a complex distributed protocol right. TLA⁺ and TLC are tools that make this possible for practicing software engineers...Even very simple and abstract models can help catch non-trivial bugs. -> -and in a [post](https://www.mongodb.com/company/blog/technical/rapid-prototyping-safe-logless-reconfiguration-protocol-mongodb-tla-plus) about their specification-driven redesign of a [novel dynamic reconfiguration protocol](https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.OPODIS.2021.26): +They also note the value of these tools for accelerating rigorous design of complex protocols, +specifically during their [development of a novel dynamic reconfiguration protocol](https://www.mongodb.com/company/blog/technical/rapid-prototyping-safe-logless-reconfiguration-protocol-mongodb-tla-plus): > Model checking is an excellent tool for rapidly and precisely answering "what if" design questions. Our efforts also emphasized an important feature of lightweight, design-level formal methods techniques, which is about more than simply ensuring correctness of your system design. Rather, it enables the exploration of protocol optimizations at a level of aggressiveness and velocity that would typically be infeasible with manual design methods. From this perspective, we can view these formal methods tools as not only a means for improving correctness of our systems and protocols, but as a means for efficient exploration of the optimization design space while maintaining a high correctness bar. They have also employed TLA⁺ for model-based trace checking and for modular specification and model-based verification of distributed transactions, writing about their experiences in several papers: -> > [**Extreme Modeling in Practice**](https://dl.acm.org/doi/10.14778/3397230.3397233) > > A. Jesse Jiryu Davis, Max Hirschorn, Judah Schvimer @@ -159,7 +158,6 @@ They have also employed TLA⁺ for model-based trace checking and for modular sp > William Schultz, Murat Demirbas > > VLDB 2025 -> From d5e92d3387014a14a497f34cd85b3bd86071ffc9 Mon Sep 17 00:00:00 2001 From: William Schultz Date: Wed, 10 Sep 2025 21:14:21 -0400 Subject: [PATCH 3/4] Condense references and minor edits --- content/industry/index.md | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/content/industry/index.md b/content/industry/index.md index 5bcaef4..2761440 100644 --- a/content/industry/index.md +++ b/content/industry/index.md @@ -122,13 +122,13 @@ To us, it is a great indicator of those who really care about quality and correc ## MongoDB -MongoDB engineers have applied TLA⁺ to core protocols within the MongoDB database over several years, as early as 2015, including distributed replication, dynamic reconfiguration, and distributed transactions. These are complex and highly concurrent protocols and systems, where testing alone is often not sufficient to catch and reproduce subtle design bugs. +MongoDB has applied TLA⁺ to core protocols within the MongoDB database over several years, as early as 2015, including distributed replication, dynamic reconfiguration, and distributed transactions. These are complex and highly concurrent protocols and systems, where testing alone is often not sufficient to catch and reproduce subtle design bugs. MongoDB engineers [emphasized](https://youtu.be/x9zSynTfLDE?feature=shared&t=73) the value derived from TLA⁺ in their experience specifying and model checking their core consensus protocol: > Without a formal model, it’s nearly impossible to get a complex distributed protocol right. TLA⁺ and TLC are tools that make this possible for practicing software engineers...Even very simple and abstract models can help catch non-trivial bugs. -They also note the value of these tools for accelerating rigorous design of complex protocols, +They also noted the value of these tools for accelerating rigorous design of complex protocols, specifically during their [development of a novel dynamic reconfiguration protocol](https://www.mongodb.com/company/blog/technical/rapid-prototyping-safe-logless-reconfiguration-protocol-mongodb-tla-plus): @@ -138,26 +138,21 @@ They have also employed TLA⁺ for model-based trace checking and for modular sp > [**Extreme Modeling in Practice**](https://dl.acm.org/doi/10.14778/3397230.3397233) > -> A. Jesse Jiryu Davis, Max Hirschorn, Judah Schvimer +> A. Jesse Jiryu Davis, Max Hirschorn, Judah Schvimer, VLDB 2020 > -> VLDB 2020 > ->   +> > > [**Fault-Tolerant Replication with Pull-Based Consensus in MongoDB**](https://www.usenix.org/conference/nsdi21/presentation/zhou) > -> Siyuan Zhou, Shuai Mu +> Siyuan Zhou, Shuai Mu, NSDI 2021 > -> NSDI 2021 > -> ->   -> > [**Design and Modular Verification of Distributed Transactions in MongoDB**](https://www.vldb.org/pvldb/vol18/p5045-schultz.pdf) > -> William Schultz, Murat Demirbas +> William Schultz, Murat Demirbas, VLDB 2025 +> > -> VLDB 2025 From bd27eab866738b7490293a5451c3e08c26fb4350 Mon Sep 17 00:00:00 2001 From: William Schultz Date: Wed, 10 Sep 2025 21:17:15 -0400 Subject: [PATCH 4/4] Condense lines --- content/industry/index.md | 7 ------- 1 file changed, 7 deletions(-) diff --git a/content/industry/index.md b/content/industry/index.md index 2761440..dd74782 100644 --- a/content/industry/index.md +++ b/content/industry/index.md @@ -140,20 +140,13 @@ They have also employed TLA⁺ for model-based trace checking and for modular sp > > A. Jesse Jiryu Davis, Max Hirschorn, Judah Schvimer, VLDB 2020 > -> -> -> > [**Fault-Tolerant Replication with Pull-Based Consensus in MongoDB**](https://www.usenix.org/conference/nsdi21/presentation/zhou) > > Siyuan Zhou, Shuai Mu, NSDI 2021 > -> > [**Design and Modular Verification of Distributed Transactions in MongoDB**](https://www.vldb.org/pvldb/vol18/p5045-schultz.pdf) > > William Schultz, Murat Demirbas, VLDB 2025 -> -> - ## OpenComRTOS