Is there a TM that halts on all inputs but that property is not provable?
Yes. The Turing machine that computes the Goodstein sequence beginning from its input and terminates when the sequence hits zero.  It always terminates but this can't be proven in Peano arithmetic.  I'm sure there are equivalent things for ZFC or any other system you might choose.



Edit For ZF, Hartmanis and Hopcroft show that there's a Turing machine $M$ that rejects every input but that this can't be proven in ZF.  I'm not sure if ZF can prove that $M$ always halts but it certainly can't prove that the machine $M'(x)$ $=$ "If $M$ accepts $x$ then loop forever, else halt" always halts, even though it does.  That still leaves ZFC open but ZF is more powerful than PA.

See Sec.&nbsp;3 of Scott Aaronson's survey on independence of P=NP for an exposition of the Hartmanis&ndash;Hopcroft result and citations to their original papers.