Towards Model-based Verification of a Key-Value Storage Engine

Summary

MongoDB developers formalized the interface boundary between their distributed transactions protocol and the underlying WiredTiger key-value storage engine using a compositional TLA+ specification. This modular model established an abstract contract to verify that the storage engine's concrete timestamp-based operations matched the semantics expected by the distributed transaction layer. To check conformance, a modified version of the TLC model checker generates a complete graph of reachable states for finite parameters and computes path coverings. Each identified path is translated into an automated test case consisting of a sequence of storage engine API calls. For a finite model with two keys and two transactions, this workflow generated 87,143 test cases that executed against WiredTiger in approximately 40 minutes.

Context

MongoDB needed to verify that the implementation of its underlying key-value storage engine, WiredTiger, conformed to the abstract behavior and concurrency control semantics expected by its distributed transactions protocol.

Approach / What changed

Using a compositional TLA+ specification, the team formalized the interface contract between the distributed protocol and WiredTiger. They modified the TLC model checker to generate a complete reachable state graph for finite parameters and calculated path coverings across the graph. Each path was automatically converted into a test case executing a sequence of WiredTiger API calls to check conformance against the specification.

Takeaways

• Formalizing the interface boundary between distributed transactions and the WiredTiger storage engine enabled automated conformance verification between abstract semantics and implementation.
• A modified TLC model checker generates a complete state graph for finite parameters, using path coverings to convert abstract execution paths into sequences of storage API test calls.
• For a finite model evaluated with two keys and two transactions, the generation tool produced 87,143 test cases that ran against WiredTiger in approximately 40 minutes.

Related reading

• MongoDB · Sep 25, 2025

  Carrying Complexity, Delivering Agility

  MongoDB centers its engineering architecture around resilience, intelligence, and simplicity to minimize developer cognitive and operational burdens when building distributed applications. Security is enforced through dedicated clusters in isolated virtual private networks alongside Queryable Encryption, which allows equality and range queries on ciphertext without decryption keys ever leaving the client. High availability is built on replica sets across independent availability zones and multi-cloud topologies, utilizing consensus mechanisms that commit writes only after majority acknowledgment in the active term. Operational friction in artificial intelligence workloads is addressed by integrating vector search directly into the core query engine, eliminating brittle extract-transform-load pipelines and separate vector databases.

  Akshat Vig, Ashish Kumar

• MongoDB · Sep 25, 2025

  From Niche NoSQL to Enterprise Powerhouse: The Story of MongoDB's Evolution