I would like to know some non-trivial examples of partial combinatory algebras whose realizability universe does not satisfy all of the axioms of Constructive Zermelo-Fraenkel (CZF) set theory.
Based on what I read in the notes Realizability by Streicher it seems that the realizability model of the Kleene's first combinatory algebra is as strong as Heyting Arithmetic with Extended Church Thesis, but not does not satisfy CZF. Is my understanding of the text correct? What are some other examples of non-trivial realizability models which do not satisfy CZF?
For each pca, there are multiple ways to make it into a realizability model depending on what exactly you want. In the note you linked to Streicher defines realizability for arithmetic and the categories of assemblies and modest sets. In each case $\mathbf{CZF}$ doesn't hold, but it's not so much a case of axioms being missing, but more that the construction of the model is for the language of first order arithmetic or the internal logic of a locally cartesian closed category, which is different to the language of set theory. For each pca $\mathcal{A}$, there is also a realizability model $V(\mathcal{A})$ of $\mathbf{IZF}$, explained in McCarty's PhD thesis, Realizability and Recursive Mathematics (and so $\mathbf{CZF}$ as a special case). Applying this to the first Kleene algebra gives a model of $\mathbf{IZF}$ satisfying Church's Thesis.