9000 » from archive
seL4: «The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is going open source [in about a month].» - http://sel4.systems/
«t will include all of the kernel's source code, all the proofs, plus other code and proofs useful for building highly trustworthy systems. All will be under standard open-source licensing terms.» ‎· 9000
^ This was, I suppose, also formally verified! ‎· 9000