If we specifically do not assume the Axiom of Choice, are all the sets that we can prove to exist specified by some finite formula? (All the other Zermelo-Frankel set theory axioms seem constructive to me, so I want to say yes, but I'm not sure.) If not, what's an example of such a set?
A slightly related questions: in a previous question I had about the Axiom of Choice, some of the answerers mentioned the distinction between a function and "a function you can name". Assuming the Axiom of Choice is basically assuming the existence of a function you can't name; are there examples of unnameable functions if we don't assume the Axiom of Choice? (Again, I want to say no, but I want to make sure.)
I believe that your first mistake is that the ZF theory is a lot less constructive then it seems. The axiom of choice in particular.
The answer to your first question is no. If something can be proved to exist, then you can write a formula defining the class of all sets which has this property. From this, however, you cannot say that every such set is definable. You cannot even have a canonical represntative which you can always use explicitly.
Here are some examples of sets that we cannot prove from ZF, or even ZF+Not AC:
Andreas Blass proved in [1] that in ZF assuming that every vector space has a basis implies the axiom of choice, as a result if we assume that the axiom of choice does not hold then we can only tell that in our universe there is a vector space without a basis. We cannot actually define it, or even know over which field it is.
When asserted, the axiom of choice tells us that every cardinal is an $\aleph$-number, and we have definable representative sets for each $\aleph$. That is there is a class function $C$ such that $C(X)=|X|$ and $C(X)=C(Y)\iff |X|=|Y|$. Such function may not be definable with the absence of choice. However, it may be definable depending on the universe. [2, Theorem 11.3]
Assuming the axiom of choice itself does not hold, there are restricted versions of it (and there are many different ones) which are independent from one another, each asserting the existence of some sets that you cannot really define otherwise. Unless you specify exactly how much of the axiom of choice is violated there may be some choice hidden in your universe and you cannot prove that. [2, Chapter 8]
In continuation from the last example, a universe of ZFC is in particular a universe of ZF without choice. If only specifying ZF, without an additional assumption that AC does not hold, it is possible that your universe is actually L, for example.
As for the second question, following from the first, we have that it is yes.
For example, take amorphous sets. These are infinite sets which cannot be written as a disjoint union of two infinite sets. Their existences violates the axiom of choice in a very strong way, as the axiom of choice implies that every infinite set can be written as a disjoint union of two parts equinumerous to the original set.
Suppose $A$ is an amorphous set. Then $A\in V$, and for some $\alpha$ we have that $A\in V_\alpha$ ($V_\alpha$ and $V$ are the von Neumann hierarchy).
It can be shown that the minimal $\alpha$ is a successor ordinal. Therefore for some $\beta$ we have $A\in V_{\beta+1}=\mathcal P(V_\beta)$. This means that there exists a partial function from $V_\beta$ bijective with this crazy set. Where does that happen in the hierarchy? How does the function look like? No one knows. It cannot be in the first $\beta=\omega$ levels, since in there everything is definably well ordered, but we cannot tell much more than that.
Of course that the axiom of choice, by definition, asserts that there are functions which exist and we cannot prove their existence otherwise. However as above shows, in its absence there are also functions which we cannot describe.
Bibliography:
Blass A. Existence of bases implies the axiom of choice, (Axiomatic Set Theory (ed. J. E. Baumgartner, D. A. Martin, and S. Shelah) Contemp. Math. 31 (1984) 31-34).
Jech T. The Axiom of Choice, North-Holland (1973).