It can't in the general case. When you're writing formally verified code (or hardware design) it is very common for the formal engine to just say "nope! couldn't prove it!".

But that doesn't mean it is useless. The halting problem has almost no practical relevance because we don't really care about the general case.