The presence of software is pervasive in the society, and, due to its impact on our routines, the concern about its quality and reliability is a matter of utmost importance, especially when it comes to critical systems. Although software testing is a crucial step in software production, it is typically associated with some risks and elevated costs, particularly, when carried out manually. Model-based testing (MBT) tools are capable of changing this scenario, enabling automatic test design and execution. However, assessing the correctness of these tools, which are also software developed by humans, is a valid concern too. To alleviate this concern, formal testing approaches are proposed, encompassing a well-defined conformance relation, along with test generation and execution strategies. Moreover, it is typically expected a proof of the soundness of the proposed approach. Unfortunately, many of the devised conformance relations are only theoretically defined, or are associated with disconnected implementations, that is, with no rigorous guarantees that the proposed theory is implemented correctly. Here, we show how an industrial-strength interactive theorem prover (Rocq) can be used to simultaneously formalise and provide a correct mechanisation of conformance testing theories; bridging the gap between theory and practice.