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-

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 http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf Later on, the separation kernels: https://arxiv.org/pdf/1701.01535 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/2016/02/pldi117-yang.pdf 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/ https://muen.sk/