Most of the kernels that try very hard to achieve correctness (in the embedded / real-time space that would be used in military or aerospace applications) are m

Most of the kernels that try very hard to achieve correctness (in the embedded / real-time space that would be used in military or aerospace applications) are microkernels. Microkernels have a smaller number of primitives that are more orthogonal, so they are easier to implement correctly and audit them, and you get some amount of preemptibility for free. Also, as far as I know, the only kernel that has been proven correct with a mechanically verifiable proof is an L4 variant.