story
I'm not sure what types of enterprises actually use formal verification since it's very costly. Writing software is much faster than verifying it. Embedded auto, aerospace, industrial applications, sure. Facebook? I doubt it.
Such methods could be useful, maybe coupled with fuzzing, for breaking software too. It might suggest avenues for exploit.
Systems like coq are used more naturally in math proofs, but even there it's very hard to apply.