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

In a follow-up to a previous discussion on MongoDB's distributed transactions protocol, this text delves into the modular verification process used to ensure that the implementation of the WiredTiger storage engine aligns with its formal specification. By formalizing the interface between the distributed transactions protocol and the underlying storage engine, MongoDB developed a tool to automatically generate test cases to verify this conformance. Using a modified TLC model checker, the storage component's state space is explored to produce tens of thousands of test cases that verify the consistency of the WiredTiger implementation with the abstract model. This method not only provides a rigorous approach to verifying correctness across system layers but also opens up future possibilities for further exploration using techniques such as randomized path sampling. The article highlights the potential role of large language models (LLMs) in automating aspects of this verification process. More technical details and resources are available in the referenced VLDB ‘25 paper and associated GitHub repository.