Have we found a Turing Machine for which halting/non-halting is unprovable? The undecidability of the Halting Problem implies that there exist Turing Machines such that you can't prove whether they halt or not in whatever logical system you're using (let's say ZFC)$^1$.
Have we found any such machines, and proven their halting's independence of ZFC?
It's easy to come up with problem specifications for which no proof could be found either way, but I'm looking for concrete programs you could write in any programming language. Put another way, I'm looking for a constructive proof of the Halting Problem.
$^1$ Proof: Consider a program H which takes a number N, enumerates all statements in ZFC searching for a proof that the Nth Turing Machine halts or does not halt. If every TM has  such a proof, then H will eventually find an answer, and thus will solve the halting problem (unless there's a contradiction in ZFC, in which case the proof of halting for any machine can be found trivially).
 A: As announced in postings on Scott Aaronson's blog (The 8000th Busy Beaver number eludes ZF set theory and 
Three announcements), here are two explicit Turing machines whose halting/nonhalting behavior is claimed to be independent of ZFC: 
7918 states (by Adam Yedidia and Scott Aaronson)
1919 states (by Stefan O’Rear)
A: 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.
