In [this arxiv post](https://arxiv.org/abs/1707.00202) (to appear in *Journal of Symbolic Logic*) we prove the existence of an explicitly definable set-theoretic construction in ZF (without if/else clauses) 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.