one thing where proofs are invaluable is the security of distributed systems where you need to exhaustively consider many uncoordinated actors.