I asked (and also answered) [a more general version of this question](https://mathoverflow.net/questions/304290/for-which-theories-does-zfc-without-global-choice-prove-the-existence-of-a-prope) a while ago. To summarize the answer, some [results of Kanovei and Shelah](https://arxiv.org/abs/math/0311165) have the following corollary: 

**Fact.** In $\mathsf{ZFC}$ there is a uniform procedure for building 'set-saturated,' class-sized elementary extensions of arbitrary structures. That is to say there are formulas $S(M,L,x)$ and $F(M,L,f,x)$ in the language of set theory such that in any model $V \models \mathsf{ZFC}$ if $L \in V$ is a language and $M \in V$ is an $L$-structure, then the following hold (where $M^\ast = \{x \in V : V \models S(M,L,x)\}$):

- $M \subseteq M^\ast$,
- if $\varphi \in V$ is an $L$-formula with free variables $x_0,\dots,x_n$ and $\bar{a} \in M^\ast$ is an $n$-tuple, then $V \models F(M,L,\exists x_n\varphi,\bar{a})$ if and only if $V \models (\exists x \in M^\ast) F(M,L,\varphi,\bar{a}x)$ (where we are using some fixed coding of tuples in $\mathsf{ZFC}$),
- furthermore, if $\bar{c} \in M$ is an $(n+1)$-tuple, then $V \models F(M,L,\varphi,\bar{c})$ if and only if $V \models “M \models \varphi(\bar{c})”$ (in particular, if $\varphi$ is a sentence, then $V \models F(M,L,\varphi,\varnothing)$ if and only if $V \models “M \models \varphi”$), and
- if $A \subseteq M^\ast$ is a set and $p(x)$ is a consistent set of $L_A$-formulas with free variable $x$, then there is $b \in M^\ast$ such that for any $\varphi(x,\bar{a}) \in p(x)$, $V \models F(M,L,\varphi,b\bar{a})$.

So to state it informally, $S(M,L,x)$ defines the universe of a class-sized elementary extension of $M$ and $F(M,L,f,x)$ is its truth predicate.

So applying this to the naturals tells us that there is a formula that defines a proper class monster model of $\mathrm{Th}(\mathbb{N})$ in any model of $\mathsf{ZFC}$.

One thing to note, though, is that without global choice (which makes my original question trivial), it's unclear whether there's always a definable isomorphism between different set-saturated class-sized models of a given theory. I believe this is related to [an unanswered MathOverflow question of Hamkin's](https://mathoverflow.net/questions/227849/is-the-universality-of-the-surreal-number-line-a-weak-global-choice-principle).

Another thing to note is that certain constructions that model theorists commonly use with the monster model are unclear in the context of these class monster models. There isn't necessarily a good way to talk about global types, for instance. You do, however, get a good homogeneity property: There is a subgroup $G$ of $\mathrm{Aut}(M^\ast)$ that can be represented as a class in a definable way which has the property that if $\bar{a}$ and $\bar{b}$ are set-sized tuples that realize the same type, then there is a $\sigma \in G$ such that $\sigma \bar{a} = \bar{b}$.