Learn how we used modular, model-based verification technique for automatically checking conformance between the WiredTiger key-value storage engine implementation and an abstract formal specification of its API.

The MongoDB blog offers developers insights into MongoDB database technology, including tutorials, best practices, and use cases for building scalable and flexible applications. Developers can learn about MongoDB's document-oriented data model, query language, and distributed architecture, as well as explore topics such as data modeling, indexing strategies, and performance optimization.

MongoDB

MongoDB engineers describe a model-based verification approach for checking conformance between the WiredTiger key-value storage engine and a formal TLA+ specification of its API. Using a modified TLC model checker, they generate the complete reachable state graph of the storage component specification, then compute path coverings to produce individual test cases as sequences of WiredTiger API calls. For a small finite model (2 keys, 2 transactions), this yields 87,143 automatically generated tests executed in ~40 minutes. The work is part of a broader compositional verification effort for MongoDB's distributed transactions protocol, published at VLDB '25, and future directions include broader WiredTiger API coverage, randomized state space exploration, and potential LLM-assisted model generation.

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