Whether the halting of a particular Turing machine is provable (or disprovable) depends on which axioms you would accept a proof starting from, of course.
However, Gödel's Incompleteness Theorem shows how to construct, for every "reasonable" theory (that is, set of axioms) $T$, a particular logical formula $G$ where it is not provable from $T$ whether $G$ itself has a proof from $T$.
Thus, once you've chosen your theory $T$ (which could be for example Peano Arithmetic or ZFC set theory) construct a Turing machine $M$ which iterates through all possible strings of symbols and checks whether each of them is a valid proof of $G$. If it finds a valid proof it halts; otherwise it keeps searching.
Since $T$ cannot tell us whether $G$ has a proof, it cannot tell us whether $M$ will halt either.
The Gödel sentence itself is rather long and complicated if we want to write it out completely -- but fortunately we don't need to do that here: We can just program $M$ such that it starts by computing $G$ according to Gödel's instructions, and then begins looking for proofs. Writing an algorithm that will output $G$ is much more tractable than writing down $G$ itself. So if you want to see $M$ explicitly, a competent CS graduate student would probably be able to write it down in at most a few thousand lines of Scheme or Haskell.
Shorter solution: If we strip away the parts of Gödel's construction that are not immediately relevant here, we get this machine:
1. Let M be my own source code (using any standard quine technique)
2. Search for a proof in ZFC of "M does not halt".
3. If one is found, stop.
If ZFC proves that the machine doesn't halt, then it will halt (so ZFC can't be true). On the other hand if ZFC proves that it does halt, then (assuming ZFC is true) it will halt, which must be because it eventually finds a proof that it doesn't halt, so ZFC is inconsistent.
