Suppose we are standing outside a realizable system which admits CZF or a similar constructive set theory. Then consider the following:
regexmid in Metamath ILE)So, working backwards from outside the system, is it the case that this system always has some non-well-founded sets? The internal logic might not be able to see them, of course.
You are using the wrong definition of well-foundedness.
Let $R \subseteq A \times A$ be a relation. Consider the following definitions:
$R$ is inductive when for all $B \subseteq A$, if $\forall x \in A . (\forall y \in A . y R x \Rightarrow y \in B) \Rightarrow x \in B$ then $B = A$.
$R$ has the minimal subset property when every inhabited set $B \subseteq A$ has an element $x \in B$ such that, for all $y \in A$, if $y R x$ then $y \not\in B$.
$R$ has no infinite decreasing chains when there is no $a : \mathbb{N} \to A$ such that $a_{n+1} R a_n$ for all $n \in \mathbb{N}$.
These conditions are classically equivalent, but not intuitionistically. The one that makes sense intuitionistically is the "$R$ is inductive".
CZF and most material set theories either assume as an axiom, or prove from other axioms, that $\in$ is inductive.
As far as realizability models of constructive set theories go, you can choose whether you want them to satisfy the $\in$-induction axiom. (People usually do.)
CZF includes the $\in$-induction axiom, which is the constructively sensible version of the foundation axiom. So everything in one of its models is well-founded in that sense.
However, while I'm no expert, I think this might not be a particularly definitive property. For instance, starting with a (pre)topos, you get a model of CZF/IZF/etc. by considering well-founded trees built using the (pre)topos. But you can also take non-well-founded trees to get models of non-well-founded set theories. I'm not sure there is anything more going on in realizability models of CZF than this—the model construction explicitly picking out objects so that $\in$ is well-founded.
