Turing machines whose termination is unprovable?
Termination of a Turing machine (on a fixed input) is a $\Sigma^0_1$ sentence and all usual first-order arithmetic theories are complete for $\Sigma^0_1$ sentences, i.e. all true $\Sigma^0_1$ statements are provable in these theories.

If you look at totality in place of halting, i.e. a TM halts on all inputs, then that is a $\Pi^0_2$-complete sentence and for any computably axiomatizable consistent theory which is strong enough (e.g. extends say Robinson's $Q$ theory) there is a TM whose totality cannot be proven in that theory.