MongoDB's Extreme Modeling: Conformance Checking in Practice

MongoDB engineers experimented with TLA+ specifications and two conformance checking techniques (trace checking and test-case generation) to verify their product implementations against specifications. The trace-checking experiment, conducted on the MongoDB server, aimed to validate the implementation of the Raft consensus protocol; the test-case generation experiment, on the MongoDB Mobile SDK, aimed to validate the operational transformation algorithm. Results showed that trace checking failed due to the difficulty of snapshotting the state of a multithreaded program and discrepancies between the specification and implementation, while test-case generation successfully uncovered a bug in the algorithm and achieved 100% branch coverage. The article summarizes lessons learned and presents recent advancements in the field, highlighting the importance of continuous conformance checking for TLA+ mainstream adoption.