In practice, a medium or high assurance evaluation would also require testing of about everything, covert-channel analysis to spot leaks, verification the object code matches the source, and independent team re-running those with a pentest on top. INTEGRITY-178B and VxWorks MILS are separation kernels that are finished with or in evaluation with all that data. seL4 has strongest formal methods on code and assembly but other stuff is still being done at R&D lab with no evaluation. Both it and Muen were integrated into Genode OS framework with all three needing more review, pentestimg, and improvements.
http://os.inf.tu-dresden.de/papers_ps/nizza.pdf
Survey in 2017 of most separation kernels with verification methods:
https://arxiv.org/pdf/1701.01535.pdf
This one is a medium-assurance kernel that tries to knock out most errors or injections using SPARK Ada.
https://en.m.wikipedia.org/wiki/SPARK_(programming_language)
In practice, a medium or high assurance evaluation would also require testing of about everything, covert-channel analysis to spot leaks, verification the object code matches the source, and independent team re-running those with a pentest on top. INTEGRITY-178B and VxWorks MILS are separation kernels that are finished with or in evaluation with all that data. seL4 has strongest formal methods on code and assembly but other stuff is still being done at R&D lab with no evaluation. Both it and Muen were integrated into Genode OS framework with all three needing more review, pentestimg, and improvements.