These theories axiomatize a universe of sets that can have nonstandard elements such as infinitesimals. The nonstandard set theory BST [respectively, the relative set theory GRIST] extends the language of ZFC by a unary predicate “x is standard” [respectively, by a binary predicate “x is standard relative to y”].
Theorem. Every model M of ZFC has an extension to a model of BST [respectively, GRIST] in which M is the universe of standard sets. If M is countable, then the extension is unique, modulo an isomorphism that fixes standard sets.
Corollary. BST [respectively, GRIST] is conservative and complete over ZFC.
I will describe some ideas used to prove these results, in particular, the technique of internally iterated ultrapowers.