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

[MongoDB](https://yomu.fyi/company/mongodb) · Will Schultz, Murat Demirbas · Feb 27, 2026

**Type:** Problem & solution

## 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.

**Tags:** [Architecture](https://yomu.fyi/topic/architecture), [Reliability](https://yomu.fyi/topic/reliability), [Testing](https://yomu.fyi/topic/testing)

[Read original post](https://www.mongodb.com/company/blog/engineering/towards-model-based-verification-key-value-storage-engine)