Let $BB$ denote the Busy Beaver function. Constructively there is no obvious way to prove that the Busy Beaver function is total (e.g. a Turing machine may neither halt nor not halt), and I have heard (e.g. in Bauer's "Five stages of accepting constructive mathematics" that some intuitionistic theories have models in which every $\mathbb N\to\mathbb N$ function is computable*. Is there a known bound on the least $n\in\mathbb N$ such that intuitionistic ZF fails to prove "$BB(n)$ is defined"?
If it is relevant, there are known natural numbers $n$ such that ZF fails to prove "$BB(n)=S(\ldots S(0)\ldots)$" for any number of applications of the successor function. For example it was determined in Johannes Riebel's thesis "The Undecidability of BB(748)" that this happens when $n=745$.
*I can't name any examples of intuitionistic theories with models in which every $\mathbb N\to\mathbb N$ function is computable. Perhaps the paper "Algebraic Set Theory and the Effective Topos" by Kouwenhoven-Gentil and Oosten gives such a model of intuitionistic ZF in section 2.1.1, as the definition of satisfiaction for the model is realizer-based, but I don't know enough to be sure.
It is impossible to prove in any constructive system that the busy beaver function is defined. All constructive systems $T$ satisfy the “disjunction property”; for all sentences $\phi, \psi$, if $T \vdash \phi \lor \psi$, then $T \vdash \phi$ or $T \vdash \psi$. A recursive extension of Heyting arithmetic which satisfies the disjunction property also satisfies the numerical existence property: if $T \vdash \exists n \in \mathbb{N} (P(n))$, then there is some numeral $n$ such that $T \vdash P(n)$.
Therefore, if IZF (or any other constructive system) could prove the busy beaver function is total, we could compute the busy beaver function by, given an $n$, looking for the $m$ such that IZF $\vdash m = BB(n)$. But the busy beaver function isn’t computable; contradiction.
Alternately, IZF is relatively consistent with the proposition “all functions $\mathbb{N} \to \mathbb{N}$ are computable” (Church’s Thesis). Most, but not all, constructive theories are known to be relatively consistent with this proposition. Clearly, if all total functions are computable, then the busy beaver function cannot be total. If you’re looking for a relevant topos-theoretic approach, the effective topos (which is the realizability topos for Kleene’s first PCA) is a topos in which Church’s Thesis holds (and gives rise to a model of IZF having the same property).