What is the framework in which we can talk about the procedure of Richard's paradox rigorously?

Question

It seems there are two variants of Richard's paradox: one pertaining to natural language and one pertaining to first-order logic. I will focus on the latter.

Now as pointed out in this post, there are a few issues when it comes to talking about definable real numbers. First, you can't define the notion of a definable real number from within FOL. Second, it seems like whether something is definable or not is relative to the theory that you are starting with. These seem to be enough to circumvent Richard's paradox, but it still seems like I can still start with a theory and use Richard's paradox to construct a new real number.

Here I will informally outline my construction. I am wondering how I would be able to do this rigorously.

1. Lexicographically order all FOL formulas $\varphi$ that specify a unique real number $x$.
2. Number the items in the list so that these real numbers are placed into a sequence $x_{1}, x_{2}, \ldots$.
3. Apply Cantor diagonalization to the sequence to obtain a new real number $x$ distinct from $x_{1}, x_{2}, \ldots$.

Now I know this cannot be done in FOL and ZFC. My question is, in what extension to FOL and ZFC could I make this procedure to obtain this new real number $x$ (described by a system outside of initial system)? Can anyone give me any clues?