You might model software data and operations in some formal system at various levels using a language like "coq" and develop some formal verification proofs. I've not read this book that apparently explores verifications like these: "Certified Programming with Dependent Types: ...".
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.