seL4 has a formal correctness prof that was developed by NICTA. The project started in 2006 and the formal proof and artifact was submitted in 2009. The elements of the implementation and resulting qualities present during run time are well defined but are limited to exactly those properties the project chose, like lack of dead and livelocks, arithmetic based exceptions, and buffer overruns.
L4 is less a simplified kernel and more of a microkernel, but it is fully general purpose.
One of the neat things they did was transport memory/resource management to userland and maintain a strict capabilities scheme for ensuring correctness. The other was the cost estimate they claim, which was something like a 60% cost saving for doing the formally verified programming compared to standard ‘high assurance’ programming.
It was a cool project but is not often used to support further pushes into more general systems level applicability of ‘theorem proving’ based programming languages.
Working on a number of platforms, verified on some. Multicore support is an ongoing effort afaict.
An OS built on this kernel is still subject to some assumptions (like, hardware working correctly, bootloader doing its job, etc). But mostly those assumptions are less of a problem / easier to prove than the properties of a complex software system.
As I understand it, guarantees that seL4 does provide, go well beyond anything else currently out there.
Also a C compiler (https://compcert.org/). I did exaggerate bit in saying that anything non-trivial is "nearly impossible".
However, both CompCert and sel4 took a few years to develop, whereas it would only take months if not weeks to make versions of both which aren't formally verified but heavily tested.
It takes years to develop a quality C compiler. I am a professional compiler writer and the difference between a toy compiler and a production compiler is vast.
It demonstrates that proving a full featured operating system, as complex as Windows 7 for example, is within the realm of possibility. It would just likely take a Manhattan project equivalent, with a truly unlimited budget.
