Model-Based Testing is a formal approach to testing (software) systems. Input-output conformance, often abbreviated by “ioco”, is one such approach to formal testing. It assumes that implementations can be modelled by input-enabled input-output transition systems, and it formalises when a given implementation conforms to a specification of that implementation. In the context of TNO-related projects, we have been studying (1) the problem of using ioco-based testing in the setting of Verum, and (2) the problem of deriving ‘difference’ specifications that are to be used for minimising the ioco-based testing effort. In this talk, I will explain the basic philosophy and theory behind ioco, discuss some of its peculiarities, and, (preparation) time permitting, I hope to address at least one of the two mentioned TNO-related theoretical problems.