The complexity of $T$ is indeed the issue, but on a much grander scale than you're considering. When you ask whether $T$ is "computationally simple" (e.g. effectively axiomatizable) you're automatically assuming that the language of $T$ is countable (and indeed that you've fixed a method of numbering the sentences in the language of $T$). But this isn't the case for an arbitrary first-order theory.
ZF proves the following version of the completeness theorem:
Suppose $T$ is a theory in a well-orderable language and every model of $T$ satisfies $\varphi$. Then $T\vdash\varphi$.
This is because, relative to a well-ordering of the set of all relevant sentences, we can run Henkin's completeness argument perfectly explicitly. Where choice - or rather, a fragment of choice - kicks in is when we try to handle non-well-orderable languages (or, if we have full choice, when we argue that all languages are well-orderable).
In particular, any countable set is well-orderable, so ZF alone proves completeness for all countable theories. So ZF proves the completeness theorem for basically every theory that actually is relevant to mathematical practice. (The one exception I can think of is the language of nonstandard analysis, where in order to get full transfer we want symbols for every function on the reals.)
You ask also about "missing proofs." Actually it's the other way around: you should be worried about missing models.
Specifically, suppose I have a consistent (= $\not\vdash\perp$) theory $T$. Henkin tells me that, from a well-ordering of the language of $T$, I can build a "really complete" theory containing $T$, whose term model('s reduct) is then a model of $T$. If I'm working in a model of ZF alone, however, I might not have such a well-ordering, and so I won't be able to build a model of $T$.
That is, when we see in ZF a failure of completeness, it's not because we don't have enough proofs, it's because we don't have enough models. One way to see this "concretely" is via forcing (which admittedly is far too complicated to describe here, but the point is it's a method for building models of ZF(C) "to order"): starting with a model $M$ of ZF and a theory $T$ in $M$, we can force over $M$ to make $T$ well-orderable (e.g. force with $Col(\omega,T)$). In the resulting forcing extension $N$, the theory $T$ is now well-orderable and so Henkin's argument shows that $N$ contains a model of $T$. But forcing doesn't add any new finite sequences of things we already have - such as sentences in the language of our theory - so we haven't "gained proofs" in any sense; rather, our space of models has increased.