Now that we can formally verify software models, why do we still need protection? Protection from programming errors and protection from hardware errors. The key reason is that formal models are abstractions and programmers are humans with an illogical brain using illogical and error-prone dynamic programming languages. In addition, software runs on a shared resource, called a processor and that processor exists in the real physical world, whereby external influences like cosmic rays can change its state. Hence, protection has to be seen in the context of increasing the trustworthiness (as defined by the ARRL criterion) of the system. The key is to do it in such a way that we don’t jeopardise the properties we expect from a system in absence of the errors mentioned above. This was the rationale for developing VirtuosoNext, offering fine-grain and space partitioning with some help of the hardware.