There's been a long, long tradition of software verification at Microsoft; look for SLAM (the original research backing the Static Driver Verifier), Yogi (SDV b

There's been a long, long tradition of software verification at Microsoft; look for SLAM (the original research backing the Static Driver Verifier), Yogi (SDV backend V2), Slayer (generic memory safety) and Terminator (termination of system code). All of the research is out in the open, often with reference implementations. The problem with all of these things (as with FramaC) is that they only work if you restrict the fragment of programs that you're looking at. Kernel modules work out surprisingly well, because they are not allowed to do a whole lot by convention.