Tarksi's theorem states that for any sufficiently strong formal language L, the truth predicate for L cannot be defined in L. For instance the truth predicate for the language of first-order arithmetic cannot be defined in the language of first-order arithmetic. It can be defined in the language of second-order arithmetic though.
My question is, what is the truth predicate for the language of ZFC, i.e. the language of first-order set theory? And what is the language needed to define this truth predicate. Is it second-order set theory, i.e. the language of NBG and MK involving sets and classes?
This is all very standard - here is an attempt to write something about it.
If we are talking about truth, we really want to talk about models, rather than about languages, because until we specify a model we don't have a notion of "true" at hand. We should avoid talking about the "truth predicate for a language".
For any model $M$ in a first-order language, the definition of the truth predicate of $M$ is the same - we define the elementary diagram of $M$ as the set of all sentences with parameters from $M$ that are true in $M$, using Tarski's recursive definition of truth, using the T schema. This is the same for a model of ZFC as for any other model in first-order logic.
A key aspect of the T schema is that it is recursive - it gives an inductive definition of the set of true sentences, but not an explicit definition.
Tarski's theorem on the undefinability of truth shows that, for many theories, there is no formula $\text{True}(x)$ in the language of the theory so that, for every model $M$ of the theory and every formula $\phi$, $\text{True}(\phi)$ holds in $M$ if and only if $\phi$ holds in $M$. In particular, we could let the theory by PA or ZFC.
But there is a standard way to make an explicit definition of the truth, which works over every model of a given theory like ZFC of PA, by using a higher kind of quantifier. To do so, we first notice that the overall truth predicate of a model is stratified into a hierarchy by the number of alternations of quantifiers that the formula has in prenex normal form. This is analogous to the arithmetical hierarchy, but the formulas may now have parameters. In the case of ZFC these will be set parameters.
The base layer of this hierarchy consists of quantifier-free formulas with parameters. The next level consists of formulas that have one block of a single kind of leading quantifier, the third consists of formulas with two blocks of quantifiers at the front, etc. Call these levels $H_0$, $H_1$, etc.
For example, a formula $(\exists x)\phi(x)$ is true in a model $M$ if and only if $\phi(a)$ is true for some $a \in M$, in other words if and only if $\phi(a) \in H_0$ for some $a \in M$. Similarly $(\forall x)(\exists y)\psi(x,y)$ is true in $M$ if and only if $(\exists y)\psi(a,y)$ is in $H_1$ for every $a \in M$.
There is a single second-order formula $\tau$ that defines the sequence $(H_0, H_1, \ldots)$ over a model $M$. This formula first defines $H_0$ explicitly, then says that for all $n$, an existential formula $(\exists x)\phi(x)$ is in $H_{n+1}$ if and only if there is some $a \in M$ so that $\phi(a)$ is in $H_n$. There are additional clauses for all the logical connectives, etc.
Using the formula $\tau$, we can write an explicit second-order definition of the truth predicate: a formula with $n$ alternations of quantifiers is true if and only if, for every sequence $(A_0, A_1, \ldots)$ that satisfies $\tau$, $\phi$ is in $A_n$.
The reason that this does not give an explicit definition of the truth predicate in the original language is the parameters in the formulas. For example, if we work over any model $M$ of ZFC, $H_0$ is already a proper class of $M$ (among other things, it includes the formula $a = a$ for every $a \in M$).
Thus, for ZFC, saying "for every sequence $(A_0, A_1, \ldots)$ that satisfies $\tau$" requires quantifying over proper classes. This is exactly what the new quantifiers in second-order ZFC can do, so we can write an explicit definition of the truth predicate in second-order ZFC. If we call this definition $\text{True}'(\phi)$ we have this result: for every model $M$ of ZFC, if $M'$ is the expansion of $M$ to a full second-order model, and $\phi$ is any sentence of ZFC, then $M$ satisfies $\phi$ if and only if $M'$ satisfies $\text{True}'(\phi)$. Here the full expansion of $M$ is the second-order model whose classes are all the possible subsets of the domain of $M$.