U [soylentnews.org] writes:
seL4 [sel4.systems], a formally verified ("bug-free") L4 microkernel variant designed to provide strong security properties, has been released under the GPLv2. The proof is written in Isabelle and the code in C. Both the C code and the binaries produced from it
have been proven to meet a formal specification [sel4.systems]. Further, it has been proven that the specification can be used to enforce the properties of integrity and confidentiality. (The proof currently only applies to the ARM port, and
a list of proof assumptions and limitations [sel4.systems] is available.)
Original Submission
