Is there a conservative extension of IZF that extends IZF by a weak form of the axiom of choice? The full axiom of choice implies the LEM, and so is incompatible with constructive mathematics, although there are some weaker forms of the axiom of choice, such as the axiom of dependent choice, or the axiom of countable choice, that do not imply LEM, and thus some constructivists make use of. My motivation for this question is, even though some (all?) of the weaker forms of the axiom of choice do not imply LEM, are they valid constructively in the sense that even though the axiom might allow for non constructive proofs, we could still in principle take any proof, and derive an appropriate constructive proof (sort of a "meta-constructivism", if you will).

Yes, the _presentation axiom_ ($\mathbf{PAx}$), which implies dependent choice and so also countable choice holds in realizability models. Hence it is consistent with Church's Thesis (all functions are computable) and we have conservativity for some formulas (in particular all $\Pi^0_1$ sentences). Also there is a very weak axiom, $\mathbf{AC}_{\omega, \omega}$ for which we get conservativity for all arithmetical sentences (see Chen, _Independence and conservativity results for intuitionistic set theory_, chapter 8).