There is a good overview of the topic on the authors page, at http://ertos.nicta.com.au/publications/papers/Klein_09.pdf.
It specifically mentions "the other" big Project in this field, the VeriSoft project ( http://www.verisoft.de/ ). VeriSoft is broader in scope (covering the translation of programs down to machine code level, and also aiming to verify properties of user-space programs), but uses a simpler implementation Language lacking C-pointers, called "C0". C0 is extended with limited support for inline-assembly code for the compilation of the OS ( http://www-wjp.cs.uni-sb.de/publikationen/GHLP05.pdf ).
Slashdot Mirror
There is a good overview of the topic on the authors page, at http://ertos.nicta.com.au/publications/papers/Klein_09.pdf. It specifically mentions "the other" big Project in this field, the VeriSoft project ( http://www.verisoft.de/ ). VeriSoft is broader in scope (covering the translation of programs down to machine code level, and also aiming to verify properties of user-space programs), but uses a simpler implementation Language lacking C-pointers, called "C0". C0 is extended with limited support for inline-assembly code for the compilation of the OS ( http://www-wjp.cs.uni-sb.de/publikationen/GHLP05.pdf ).