Microsoft invests a massive amount of money into MSR, and creates tools out of the most useful results. The Static Driver Verifier depends on Z3, an SMT solver developed at MSR. Other verification tooling like SAL (C/C++ annotations to assert contracts for functions) has a similar history.
