current tools, verifying C code like seL4? never going to happen. but i'm hopeful about new techniques, things like the work Amal Ahmed http://www.ccs.neu.edu/home/amal/ is doing. you don't need to formally verify the entire codebase for basic properties like "can compose with the sel4 proofs" if your runtime/compiler/language/OS is all participating. right now you have to fight against the fact that none of the software of interest is well-understood mechanically by other software.