The discussion in the comments has helped clarify your question for me. I believe that it is closely related to the following remark by Harvey Friedman:
I am convinced that trying to take consistency statements like Con(ZFC +
measurable cardinals) or Con(ZFC + rank into itself), Con(ZF + inaccessible
rank into itself), etc., and force them into smaller and smaller Turing
machines not halting, with demonstrable equivalence in an extremely weak
system, is an open ended project, in the practical sense, that will create a
virtually unlimited opportunity, in the practical sense, for a stream of
ever and ever deeper mathematical ideas. Ideas that could come from
unexpected sources, ideas that could have independent deep ramifications,
ideas that -- well who knows what to expect. The benchmark is completely
clear - how many quadruples? At the very least, deep ideas about set theory
and large cardinals, but probably much more diverse deep ideas about, well,
the unexpected. Any branch of mathematics whatsoever might prove useful, or
even crucial, here. Whereas, we don't think that "any branch of mathematics"
might be useful in logic problems, normally. This is different.
Other relevant postings from the FOM archives may be found here and here.
So Friedman's work, that Andres Caicedo alluded to in the comments, is probably the closest thing to what you want. I don't know of any other people who are working actively on this kind of project.
As a side remark, I believe that your intuition is correct that there is some kind of intrinsic "complexity" to the statement "ZFC is consistent," and roughly speaking it is because the totality of mathematical knowledge is a "complex" entity.
The first thing to notice is that if ZF is consistent, then it is
consistent with ZFC that what you call ProveLoop is actually decidable. The
reason is that if ZF is consistent, then by the incompleteness
theorem, it is consistent with ZFC that $\neg$Con(ZF), in which case everything is provable in
ZF, in which case every program is in ProveLoop.
So in the proof that ProveLoop is undecidable, one needs to make
an additional assumption about the reliability of the proofs in ZF to
avoid this issue with the incompleteness theorem.
Meanwhile, under such a consistency assumption, ProveLoop is indeed
equivalent to the halting problem.
Theorem. Assume Con(ZF). Then ProveLoop is Turing
equivalent to the Halting problem.
Proof. Under the Con(ZF) assumption, it follows that whenever ZF proves that a program doesn't halt, then it really doesn't halt, since if it did halt, then this fact would also be provable, contrary to consistency.
Clearly ProveLoop is c.e. and hence reducible to the
halting problem, as you pointed out. Conversely, let's reduce the
halting problem to ProveLoop. Given any program $p$, we want to
decide whether $p$ halts on a blank tape, using an oracle for
ProveLoop.
Define a computable function $f$, so that $f(q)$ is the program
such that, on trivial input, if $p$ halts on the blank tape, then
$f(q)$ jumps into an immediate infinite loop, and otherwise, while waiting for $p$ to halt, the program $f(q)$ halts just in case it finds a proof that $q$ does not halt.
By the recursion theorem, there is a program $r$ such that $r$ and
$f(r)$ compute the same function, and we can find this $r$
effectively. Furthermore, by using the $r$ from the proof of the recursion theorem, we may also assume that ZF proves that $r$ and $f(r)$ compute the same function. Notice that it can't ever be that $r$ halts on account of finding a proof that $r$ does not halt, by our assumption which ensures the accuracy of proofs of non-halting, and so definitely $r$ does not halt in any case. Meanwhile, if $p$ halts, then $r$ does not halt, but for a trivial reason that will be provable in ZF, namely, the fact that $p$ halted; and otherwise, when $p$ does not halt, then $r$ will run forever, but this fact will not be provable (for if it were provable, then $r$ would halt, contrary to consequence of our assumption that such proofs are reliable). So what we have is exactly a reduction of the halting problem to ProveLoop, as desired. QED
Best Answer
Let $b_k$ be the assertion that the busy beaver function at $k$ has the value that it actually has, that is, the value it has in the standard natural numbers of the meta-theory. We know that not all of these statements are provable in ZF, if ZF is consistent, since if they were then we would be able to compute the values of the busy beaver function by searching for such proofs.
Theorem. The following are equivalent.
The theory $\text{ZF}+b_k$ is consistent, for any particular $k$.
The theory $\text{ZF}+b_{k_0}+\cdots+b_{k_n}$ is consistent, for any finite list of numbers $k_0,\ldots,k_n$.
ZF is $\Sigma^0_1$-sound.
A theory is $\Sigma^0_1$-sound, if any $\Sigma^0_1$ statement that the theory proves is actually true. If ZF is $\Sigma^0_1$-sound, then any true $\Pi^0_1$ sentences must be consistent with ZF, for otherwise we would be able to prove the negation, which would be a false $\Sigma^0_1$-statement, contrary to soundness.
Proof. ($3\to 2$) Assume ZF is $\Sigma^0_1$-sound. It already proves all the true $\Sigma^0_1$ assertions about particular machines halting. The extra assertions of the various $b_k$ are $\Pi^0_1$ assertions that no additional Turing machines of the given size halt at some later point. By soundness, these are consistent with ZF, as desired.
($2\to 1$) Immediate.
($1\to 3$) Suppose that we can consistently add any statements $b_k$ to ZF. Suppose that ZF proves some assertion $\exists n\, \varphi(n)$, where $\varphi(n)$ is $\Delta^0_0$. Consider the program $e$ that embarks on a search to find such an $n$. This program uses $k$ states for some $k$, and so if there is such an $n$, then ZF would prove that it would have to stop before the busy beaver value $BB(k)$, since otherwise we would violate the definition of $BB(k)$. Thus, if $ZF+b_k$ is consistent, ZF would prove that there is such an $n$ below the actual value of $BB(k)$. So the $\Sigma^0_1$ statement was true, and therefore ZF was $\Sigma^0_1$-sound, as desired. $\Box$
Meanwhile, let me point out that it is relatively consistent with ZF that ZF is not $\Sigma^0_1$-sound. For example, in any model of ZF in which $\neg\text{Con}(ZF)$, then obviously ZF will be proving false $\Sigma^0_1$ statements in the model. So if ZF is consistent, then so is ZF plus the assertion that ZF is not $\Sigma^0_1$-sound.