Gotcha, thanks. So to clarify, the issue is that the relevant bit is a ZFC proof of “if N halts, then if M halts, then ZFC proves phi” rather than “if N halts, then if M halts, then phi,” so in the next paragraph where we talk about N finding the proof, it doesn’t necessarily find a proof of the statement it’s searching for? And that differs from the original (correct) proof because… help me finish that sentence?

Thanks for the answer. I think I’d get a better sense for why my argument doesn’t work if I could see the original (correct) argument about Löb’s theorem recast using your notation. Would it be possible to see why the original argument is correct but why my modified one fails?

An always-halting TM would not meet the requirements because were specifically interested in a TM that loops over all proofs and checks for a proof that it itself halts. You could imagine writing a TM $X$ that takes in a TM $Y$ as input, searches for a proof that $Y$ halts, then halts if and only if it finds one. Applying Kleene’s theorem to that TM then produces $M$. This could be done in any Turing-complete language. As for which inputs - let’s relax our model of TMs a bit and imagine that, like Turing’s original conception, a TM starts with a blank tape and runs from there.

The second recursion theorem I linked in my comment states, essentially, that TMs can compute arbitrary functions of their own encodings. See these lecture slides for more details and an concrete example of a program that computes a nontrivial property of itself.

This is possible due to Kleene’s second recursion theorem. It’s analogous to the idea of a program that prints its own source code (a Quine), which is possible despite the fact that it seems like the program wouldn’t be “complete” without containing a copy of its source code. (See Chapter 6 of Sipser’s Introduction to the Theory of Computation for a good explanation.)