There is often a lot of confusion surrounding the differences between relativizing individual formulas to models and the expression of "is a model of" through coding the satisfaction relation with Gödel operations. I think part of this can be attributed to the common preference for using formulas over codings. For example, a standard proof showing that $V_{\kappa} \models ZFC$ for $\kappa$ inaccessible will appeal to the fact that all of the ZFC axioms relativized to $V_{\kappa}$ are true. But then one learns about the Lévy Reflection Theorem scheme which allows every (finite) conjunction of formulas to be reflected to some $V_{\alpha}$. Perhaps this knowledge is followed by a question of whether the Compactness theorem can be used to contradict Gödel's Second Incompleteness Theorem.
Specifically, consider the following erroneous proof that ZFC + CON(ZFC) proves its own consistency:
Introduce a new constant $M$ into the language of set theory and add to the axioms of ZFC all of its axioms $\varphi_n$ relativized to $M$, denoted $\varphi_n^M$. Provided that ZFC is consistent, every finite collection of this theory is consistent by the Lévy Reflection Theorem whereby the Compactness Theorem tells us that the entire theory ZFC + "$M \models ZFC$" will be consistent. Consequently, this theory has a (ZFC) model $N$ so in this model, there exists a model $M$ of ZFC. To summarize then, arguing in ZFC + CON(ZFC), we've seemingly proven that we have a ZFC model $N$ modeling the consistency of ZFC by virtue of it having the model $M$ (i.e., seemingly $N \models ZFC + CON(ZFC)$ so we would have a proof of CON(ZFC + CON(ZFC)).
The misstep in this proof is of course a misuse of the conclusion of the Compactness theorem, mainly the assumption that such an $N$ will think that $M$ is a ZFC model. With some enumeration of the formulas of the axioms $\{\varphi_n| n \in \mathbb{N}\}$ of ZFC, it is clear that $N$ will certainly think that $M \models \varphi_n$ for any particular $n \in \mathbb{N}$ analogous to how a nonstandard model of Peano arithmetic has an element $c$ satisfying $c > n$ for any particular $n \in \mathbb{N}$. The problem of course in the case of $N$ is that there may be formulas with nonstandard indices not accounted for just as there will definitely be nonstandard numbers greater than $c$ in the PA example.
If one were to carry out the same proof with the more tedious arithmetization of syntax, then this link may be more apparent.
To a lesser extent, there may also be confusion with the fact that $0^{\sharp}$ provides us with a proper class of $L(\alpha) \preceq L$. This may lead to the question of whether $L$ has its own truth predicate, contradicting Tarski's Theorem. But of course $L$ will only realize that each of these $\varphi^{L(\alpha)}$ is true for any ZFC axiom $\varphi$, and if one attempts to appeal to the arithmetization of syntax, one can begin to see the problem that these $\alpha$ may not (and of course will not) be definable (without parameters) in the constructible universe L.
Since these types of misconceptions can be common among logicians and non-logicians alike, I thought I would ask the highly intelligent mathematicians who have worked through such problems or helped illuminate them to others if they would do so here as well. I think compiling a collection of tidbits of wisdom in this area from the collective perspectives of the MO Community can be illuminating to all. As such, my question is as follows:
What insights can you share regarding the questions of formalizing "is a model of ZFC" in ZFC and the various "paradoxes" that arise?
For example, maybe you can show a related seemingly paradoxical problem and resolve it, or simply share your thoughts on how to avoid such traps of logic.