The seL4 operating system microkernel also aims to be formally correct. http://www.ertos.nicta.com.au/research/l4.verified/