In this arxiv post (to appear in Journal of Symbolic Logic) we prove the existence of an explicitly definable set-theoretic construction in ZF (without if/else clauses) of a hyperreal extension ${}^\ast\mathbb R$. If in addition countable choice is assumed then we prove that the transfer principle holds for this $^{\ast}\mathbb R$. Assumping the existence of a free ultrafilter on $\mathbb N$ with well-orderable base (an assumption weaker than the well-ordering of $\mathbb R$) we show that the extension $\mathbb {R}\hookrightarrow{}^\ast\mathbb R$ is proper.
As mentioned for this definable model ACC proves transfer so transfer can't fail in ZF+ACC.