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

In our previous post, we talked about our process of specifying MongoDB’s distributed transactions protocol and how it enabled novel analysis of its performance characteristics. In this follow-up,...