[agentultra]

Sel4 microkernel, compcert C compiler, https://bedrocksystems.com/, AWS and Azure both use model checking, https://hackage.haskell.org/package/containers-verified

... basically when you need to be sure certain properties of your system hold.

You can verify only the critical parts, as in a data structure or algorithm, or you can verify higher-level parts of a system. All you're doing with math is thinking (out loud) and writing a proof is constructing a convincing argument. If you need to be certain that a thread doesn't leak addresses in shared memory to other threads then you ought to take the time to think through how you're going to achieve that and prove that your solution works.