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.
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.