It is my understanding it is provable in ZFC+zero sharp that intuitionistic ZF has a nonconstructive model.
(Here I am assuming the existence of zero sharp only to guarantee that ZFC has a nonconstructive model, which I guess most people probably believe)
I cannot find any proof online and am not in a place to attempt to prove this myself, and so I don't know if there is a constructive proof of this (constructive in a manner that would satisfy the intuitionist).
Assuming there is, would this be a problem for the intuitionist?
My thought is this: if it can be constructively proved that the intuitionists foundational theory is 'just as true' in a nonconstructive ontology, the intuitionist has in no way 'guaranteed' that their universe is constructive.
I’m not exactly sure what “nonconstructive model” means in this context. In fact, when one is discussing constructive theories, one must typically adopt a broader class of models than the class classical logicians consider.
That said, it is well-known that IZF and ZF are equiconsistent. This is not too surprising, as there are many other constructive theories that are equiconsistent with a classical counterpart, such as Heyting Arithmetic and Peano Arithmetic. I personally don’t think this says too much about which one is “true” or “correct”, but that’s more of a philosophical question. The obvious and relevant facts are (1) one can prove quite a few nice things using classical logic that can’t be proved constructively, and (2) there are a lot of interesting and useful models of constructive mathematics which aren’t models of classical mathematics.