Before asking my question, let me give some motivation which could help getting better answers. In this MO question, Scott Aaronson was trying to use the concept of "definable number" to create function that would grow faster than a family of functions defined in terms of busy beaver functions and oracles using these.
Of course, as was pointed out in the answers and comments, using the concept of "some formula $\phi$ defining an integer $m$" may not make sense unless we refer to a class of structures for which we have a truth predicate, due to Tarski's theorem on truth. So, he defines his function by making a modification in the definition of "a formula defining an integer" by saying that a formula defines an integer if that integer is the unique integer satisfying the formula in all models of ZFC, in which case the definition reduces to provability.
I might be interpreting his question in a completely different way than what he had in mind, but it seems to me that he was trying to use the complicated structure of "truth" about natural numbers to create a really fast growing function.
If we were defining his $z(n)$ in the language of PA and $\omega$, I believe it would be the case that $0^{(\omega)}$ computes $z(n)$: Given n, we list all formulas with length at most n and for each formula if it defines a unique integer, we can find the unique number it defines using an oracle for $Th(\omega,+,*,0,1)$. Though, he seems to want to work with ZFC hoping maybe we can get more. However, there is no "standard model" of ZFC and quantifying over all models reducing the definition to provability creates a problem.
So, what if we fix a model $M$ of ZFC and define the function $z^M(n)$ using only that model? If I am not missing any minor points, the following should be true: If $(\omega,E)$ is some countable model of ZFC with E having Turing degree $a$, then the theory of $(\omega,E)$ has Turing degree less than or equal to $a^{(\omega)}$ (a side question: do we necessarily have equality here?), for we can decide the truth of a sentence with $k$ quantifiers by making $k$ jumps. Then, provided that one of his BB functions compute $a^{(\omega)}$, we can compute $z^M(n)$ and dominate it.
Following what he is trying to do in the original question, we want to have $M=(\omega,E)$ as complicated as possible. My question is how complicated can we make $M$? Can we have a class of models with the same theory whose membership relations have unbounded degrees? Instead of fully defining the details of how these models should look like, I want to leave the question open-ended (and add a soft-question tag!).
It probably is the case that whether these models are models of ZFC or some other theory is irrelevant. I would really like to hard-code arbitrary Turing degrees into a model using some kind of compactness argument but I do not yet see how it should go.
Not being a recursion theorist, I welcome any corrections or suggestions on my comments and observations.
Edit: Carl Mummert's answer shows that with a nice little flipping trick we can encode arbitrarily high degrees, which answers my question (and the side question!). In this case, I should rather be interested in the degrees of the theories of such models from which we can compute the functions $z$. But I guess some variant of the below trick can be used to encode any subset of naturals into the monotonicity of the continuum function on $\omega_n$'s which means that theories of these models also have unbounded degrees. If there were any bounds for this, I would try to use it to save Scott's question by fixing a model that has the same theory as $V$ (which we were not able to define in the first place) and putting a bound on growth of z, but I guess this kind of attempts is a lost cause.
Let $E$ be a countable model of a complete extension of ZFC such that each ordinal $$\omega\times n = \underbrace{(\omega + \omega + \cdots + \omega)}_{n \text{ times}}$$ is coded in $E$ by $2n$ and other sets are coded by odd numbers. Let $A$ be any subset of $\omega$. We may a new model $E'$ by "flipping" $4n$ and $4n+2$ whenever $n \in A$, which means letting $\omega \times 4n$ be coded by $4n+2$ and $\omega \times (4n+2)$ be coded by $4n$ instead. Then we can decode $A$ from $E'$ by asking whether $(4n) \in (4n+2)$ or $(4n+2) \in (4n)$. So we can make $E'$ have arbitrarily large Turing degree.