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

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.