[nickpsecurity]

Depends on if you mean design or code. In old days, there was STOP, GEMSOS, and LOCK. I have a description of two of them:

http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf

Later on, the separation kernels:

https://arxiv.org/pdf/1701.01535

VerveOS was verified at least for safety down to assembly:

https://www.microsoft.com/en-us/research/wp-content/uploads/...

The Muen separation kernel and hypervisor is verified to be free of common problems:

https://muen.sk/