Also, it's the most complicated pure reasoning task you can build. So working on theorem-proving AI may help in reasoning and reliability.
This can be applied on something like: Is your extension on distributed system protocol (like Paxos) correct? Does my novel security system hold certain properties? etc etc...
... 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.