My point was just that formal methods can have a tremendous positive impact even if academics are the only ones using them, as long as the output from those eff

My point was just that formal methods can have a tremendous positive impact even if academics are the only ones using them, as long as the output from those efforts do get used. So I'm not sure distinguishing between "using formally verified software" and "using a formal methods tool directly" is a helpful distinction when measuring industrial impact. Also, formalizing architectural properties for the world's most popular cloud service is probably even rarer a task than formalizing language specifications.