For Intuitionistic Zermelo Fraenkel (IZF) set theory, Moczydlowski ("Normalization of IZF with Replacements", 2008) proved that the Term Existence Property (TEP) holds, so if $\exists x. \phi(x)$ is provable $\phi(t)$ is provable for some term $t$.
Has a similar result been proven for Constructive Zermelo Fraenkel (CZF) set theory, or is it possible to do so?
$\mathbf{CZF}$ has many nice properties such as the numerical existence property and disjunction, but it does not have the term existence property. The immediate, but boring reason for this is that defined in the usual set theoretic language, which is relational and does not have terms witnessing e.g. union and separation. However, there is also something deeper going on. For relational theories, it's natural to ask instead for the existence property to hold, which states that whenever a sentence of the form $\exists x.\varphi(x)$ is provable, there is some formula $\psi(x)$ such that $\exists ! x.\varphi(x) \wedge \psi(x)$ is provable. This fails for $\mathbf{CZF}$, and also the more usual version of $\mathbf{IZF}$ that has collection rather than replacement. See Swan, CZF does not have the existence property for $\mathbf{CZF}$ and Friedman and Scedrov, The lack of definable witnesses and provably recursive functions in intuitionistic set theories for $\mathbf{IZF}$.