The authors of this paper explore conformance checking, a technique to ensure that an implementation matches its formal specification. They discuss the challenges and limitations of conformance checking and present their experience with two MongoDB products. The authors experimented with two techniques: trace-checking and test-case generation. Trace-checking involves generating execution traces from an implementation and checking if they conform to a specification. However, the authors found that this approach was difficult due to the complexity of the system's state space and the need for precise logging of internal variables. In contrast, test-case generation starts with a formal specification and checks if its behaviors are implemented in the code. The authors successfully used this technique to generate 4913 tests for the MongoDB Mobile SDK, achieving 100% branch coverage of the implementation. They also discuss other research projects that have explored conformance checking techniques, including multi-grained specifications and protocol conformance with Choreographic PlusCal. These projects demonstrate growing interest in conformance checking as a means to ensure the correctness and consistency of complex systems.