The Transputer T800 was formally verified. It would also be a great candidate vor hardware isolation, with different processes running on different CPUs, linked via the Transputer's hardware channels.

https://www.cs.bris.ac.uk/~dave/transputer.html

UPDATE: T800 had 250K transistors, Skylake has 1-2 billion, so you could fit around 4K-8K T800s on the same kind of die.