Modelling the behaviour of a system, and stepwise refining that model until it has become sufficiently detailed to generate executable implementation is an appealing approach to software development, advocated by companies such as, e.g. Verum. The approach is rooted in solid mathematics and supported by tools, such as mCRL2, that help the developer. Under the assumption that these tools are correct, the remaining point of attention in this approach is in correctly generating and executing the implementation from a model. Since it is very hard to reason formally about the implementation and the platform on which it runs, arguing that the generated software is ready to be shipped is tricky. In a standard software development trajectory, this is often decided by running test cases against the implementation. In this talk, I will entertain the idea of testing the generated implementation using model-based testing, exploiting the already existing models.