They also created VCC (Verifying C Compiler), which uses their Z3 theorem prover to check for bugs (especially concurrency bugs, which can be really tough to find).

http://vcc.codeplex.com/

SAL and VCC are for making C programs correct. This is related but not the same thing as making the C compiler correct. These source-level tools assume that the compiler translates the programs correctly.

Hopefully we are self hosting at this point and smart enough to apply SAL and VCC to our compiler itself.