To define nonstandard models of Peano arithmetic or set theory, many articles use enumerations like $x>0, x>1, \dots$ where $x$ is said to be a nonstandard natural number, ie a number that is finite from the PA model's point of view, but infinite from outside.
I find those enumerations confusing, especially when trying to construct a subtle notion such as a finite infinity. What kind of infinity is hidden in the dots "$\dots$" ? Some articles acknowledge the problem, and quickly offer to repair it by the compactness theorem. Then they consider a theory starting with the Peano axioms and adding a new constant symbol $c$, with axioms $c>0, c>1, \dots$ And that's even more confusing.
So far, the best definition I found of a nonstandard PA model is a structure $(M,0,S,+,\times,\leq)$ that satisfies the Peano axioms, and such as the order $\leq$ on $M$ is not a well-order. It may be more abstract than an enumeration "$\dots$", but I think it has the merit of being precise.
Is there a similar definition of a nonstandard model of ZF, not using enumerations or "intuitive" natural numbers ? It's more difficult because it concerns a model of PA inside a model of ZF. I don't manage to access the inner PA order $\leq$ from the ambiant logic.