Today there is an interesting situation in that there exist microkernels with an amount of published formal proofs such as the one by NICTA in this thread and,

Today there is an interesting situation in that there exist microkernels with an amount of published formal proofs such as the one by NICTA in this thread and, then, that there exist DO-178B avionics certified microkernels and separation kernels (often with very little published artefacts). I think that the current hot field for microkernels is to bring both formal methods and certification together, which is indeed starting to happen for DO-178C see for example https://sites.google.com/site/fmstandardsworkshop/ https://sites.google.com/site/fmstandardsworkshop/ . Holger Disclaimer: not completely unbiased here (e.g. http://www.uni-koblenz.de/~beckert/pub/safecomp2009.pdf http://www.uni-koblenz.de/~beckert/pub/safecomp2009.pdf).