I think your question is not as precise as you portray it.
First, let me point out that you have not actually defined
a function $z$, in the sense of giving a first order
definition of it in set theory, and you provably cannot do
so, because of Tarski's theorem on the non-definability of
truth. We simply have no way to express the relation x is
definable in the usual first-order language of set theory.
More specifically:
Theorem. If ZFC is consistent, then there are models
of ZFC in which the collection of definable natural numbers
is not a set or even a class.
Proof. If V is a model of ZFC, then let $M$ be an internal
ultrapower of $V$ by a nonprincipal ultrafilter on
$\omega$. Thus, the natural numbers of $M$ are nonstandard
relative to $V$. The definable elements of $M$ are all
contained within the range of the ultrapower map, which in
the natural numbers is a bounded part of the natural
numbers of $M$. Thus, $M$ cannot have this collection of
objects as a set or class, since it would reveal to $M$
that its natural numbers are ill-founded, contradicting
that $M$ satisfies ZFC. QED
In such a model, your definition of $z$ is not first order.
It could make sense to treat your function $z$, however, in
a model as an externally defined function, defined outside
the model (as via second-order logic). In this case, $z(n)$
only involves standard or meta-theoretic definitions, and
other problems arise.
Theorem. If ZFC is consistent, then there is a model
of ZFC in which $z(n)$ is bounded by a constant function.
Proof. If ZFC is consistent, then so is $ZFC+\neg
Con(ZFC)$. Let $V$ be any model of this theory, so that
there are no models of ZFC there, and the second part of
the definition of $z$ becomes vacuous, so it reduces to its
definable-in-$V$ first part. Let $M$ be an internal
ultrapower of $V$ by an ultrafilter on $\omega$. Thus, $M$
is nonstandard relative to $V$. But the function $z$,
defined externally, uses only standard definitions, and the
definable elements of $M$ all lie in the range of the
ultrapower map. If $N$ is any $V$-nonstandard element of
$M$, then every definable element of $M$ is below $N$, and
so $z(n)\lt N$ for every $n$ in $M$. QED
Theorem. If ZFC is consistent, then there is a model
of ZFC in which $f(n)\lt z(10000)$ for every natural number
n in the meta-theory.
Proof. If ZFC is consistent, then so is $ZFC+\neg
Con(ZFC)+GCH$. Let $V$ be a countable model of $ZFC+\neg
Con(ZFC)+GCH$. Since $V$ has no models of ZFC, again the
second part of your definition is vacuous, and it reduces
just to the definability-in-$V$ part. Let $M$ again be an
internal ultrapower of $V$ by an ultrafilter on $\omega$,
and let $N$ be a $V$-nonstandard natural number of $M$.
Every definable element of $M$ is in the range of the
ultrapower map, and therefore below $N$. In particular, for
every meta-theoretic natural number $n$, we have $f(n)\lt
N$ in $M$, since $f(n)$ is definable. Now, let $M[G]$ be a
forcing extension in which the continuum has size
$\aleph_N^M$. Thus, $N$ is definable in $M[G]$ by a
relatively short formula; let's say 10000 symbols (but I
didn't count). Since the forcing does not affect the
existence of ZFC models or Turing computations between $M$
and $M[G]$, it follows that $f(n)\lt z(10000)$ in $M[G]$
for any natural number of $V$. QED
Theorem. If ZFC is consistent, then there is a model
of ZFC with a natural number constant $c$ in which $z(n)\lt
f(c)$ for all meta-theoretic natural numbers $n$.
Proof. Use the model $M$ (or $M[G]$) as above. This time,
let $c$ be any $V$-nonstandard natural number of $M$. Since
the definable elements of $M$ all lie in the range of the
ultrapower map, it follows that every z(n), for
meta-theoretic $n$, is included in the $V$-standard
elements of $M$, which are all less than $c$. But $M$
easily has $c\leq f(c)$, and so $z(n)\lt f(c)$ for all
these $n$. QED
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.
Best Answer
I will not answer the question since I think it is not completely defined without completely specifying the machine model. In the following I explain why.
Note that the exact running time of a machine is not natural mathematically, it heavily depends on the particular model of the machine we use (that is why in complexity theory we get rid of such constants using asymptotic notations like $O$). Therefore, the question of computing the running time modulo some value is not natural either.
We can easily consider a machine model where all halting machines halt in even number of steps and another model where all halting machines halt in odd number of steps, and in both cases your question is trivially computable. Even more artificially, we can define a machine model where a halting machine with size $k$ halts in even number of steps iff a particular machine halts in $k$ steps (which would make the problem uncomputable). These are all valid models of computation though artificial ones.
The function is trivially computable in one model of computation, and uncomputable in another model of computation. That tells us that the question is not a natural one. Note that this is not the case regarding $BB$, it is uncomputable in all acceptable models of computation (having same computational power as Turing machines). The answer doesn't depend on the particular model of computation we use, the numbers will be different, but the question about computability has the same answer in all of them.
Your question about $BB(k) \mod 2$ for a particular fixed completely specified model of computation is well defined, but IMHO it is not a very interesting one: it is too much dependent on the particularities of the machine model. Unless you have some reasonable restrictions on the models such that the answer will be the same on all such models the question would not be very interesting IMHO.
In a sense, this is similar to asking if a particular Diophantine equation has any integer answers without explaining why that particular equation is of any interest. Here is the same, from mathematical perspective, the answer to the question is not a natural one and too much dependent on the particular encoding of the machines and I don't see any way of getting around this dependence. (Also from practical perspective, I also don't see any use for computability of this function.)