Leslie Lamport's TLA+ comes from MSR. You have likely directly benefited from this project, since it's been used to prove the correctness of many distributed systems, including pieces of AWS.
Z3 is a very popular open source SMT solver, also originating from MSR.
There's probably dozens of similar examples. You might not know about some of the work coming out of MSR, but it's probably impacting you indirectly.
It's similar to how we indirectly benefit from fundamental nuclear physics. Places like CERN have to solve engineering issues and those solutions trickle down to everyone.
Z3 is a very popular open source SMT solver, also originating from MSR.
There's probably dozens of similar examples. You might not know about some of the work coming out of MSR, but it's probably impacting you indirectly.
It's similar to how we indirectly benefit from fundamental nuclear physics. Places like CERN have to solve engineering issues and those solutions trickle down to everyone.