Kanovei & Shelah (2004) explicitly constructed a nonstandard extension of the reals. Now, I'm no expert on this but I gather that they first specified a set of free ultrafilters, and then used it to explicitly specify a particular free ultrafilter, which they used to construct a nonstandard extension of the reals. Here's the theorem they proved:
In ZFC, there exists a definable, countably saturated extension $^*\mathbb{R}$ of the reals $\mathbb{R}$, elementary in the sense of the language containing a symbol for every finitary relation on $\mathbb{R}$.
They said about their construction:
A somewhat different, but related problem of unique existence of a nonstandard real line $^*\mathbb{R}$ has been widely discussed by specialists in nonstandard analysis. Keisler notes...that for any cardinal $\kappa$, either inaccessible or satisfying $2^\kappa=\kappa^+$, there exists a unique, up to isomorphism, $\kappa$-saturated nonstandard real line $^*\mathbb{R}$ of cardinality $\kappa$, which means that a reasonable level of uniqueness modulo isomorphism can be achieved, say, under GCH. [Our theorem] provides a countably saturated nonstandard real line $^*\mathbb{R}$, unique in absolute sense by virtue of a concrete definable construction in ZFC.
The model they constructed is unique in the sense that given their definitions, one and only one model can be constructed. Here's my question: given a different set of definitions, can a totally different nonstandard extension of $\mathbb{R}$ be explicitly constructed via the same strategy they used? I'm just wondering whether more nonstandard models can be explicitly defined, other than the one defined by Kanovei & Shelah. Perhaps if a different set of free ultrafilters is specified from the start, then a different nonstandard extension can be constructed.