Comment by nine_k

Isolation is one thing, correctness is another. You may have architecturally perfect, hardware-assisted isolation, but triggering a bug would breach it. This is how a typical break out of a VM, or a container, or a privilege escalation, happens.

There is a difference between a provably secure-by-design system, and a formally proven secure implementation, like Sel4.