Conformance Checking at MongoDB: Testing That Our Code Matches Our TLA+ Specs

This post details the application of trace-checking to the MongoDB server's Raft-like replication protocol, using JavaScript integration tests and a randomized 'rollback fuzzer' to generate execution traces. These traces are translated into TLA+ and checked against the RaftMongo.tla specification to verify conformance. It describes the workflow, including running randomized tests, collecting execution traces, translating them into TLA+, and checking them with TLC model checking. The implementation of a Python script to reconstruct system state and generate Trace.tla is also described.