Add draft of MongoDB section on industrial use of TLA+ #34
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
ajdavis
suggested changes
Sep 10, 2025
content/industry/index.md
Outdated
| 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: | ||
| <!-- As they discuss in a talk on specifying and model checking their core consensus protocol: --> |
content/industry/index.md
Outdated
| > 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): |
content/industry/index.md
Outdated
| 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: | ||
|
|
||
| > |
There was a problem hiding this comment.
There's some extra vertical whitespace here and below.
lemmy
reviewed
Sep 10, 2025
| 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) |
Member
There was a problem hiding this comment.
Can we (visually) compress the references to free up screen real estate?
Contributor
Author
There was a problem hiding this comment.
Done. Can we also make sure to squash all commits in the PR when merging?
Member
There was a problem hiding this comment.
Sure, is this ready to merge from your (Mongo DB's) end?
Member
|
Thanks guys! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
@muratdem @ajdavis