I was looking through Giraud's book Cohomologie Non-abelienne, and there is a very nice theorem that Giraud proves in the Noetherian case (Cohomologie Non-Abelienne VII.2.2):

Let $f:X\to Y$ be a proper map of schemes with $Y$ locally Noetherian. Then for any map $i:A\to Y$, let $X_A$ denote the pullback equipped with projections $\pi_X:X_A\to X$ and $\pi_A:X_A\to A$. Then if $F$ is a constructible étale stack on $X$, the component of the base-change transformation $$\beta_F: i^\ast f_\ast F \to π_{A,\ast} \pi_X^\ast F$$ at $F$ is an equivalence.

By standard reductions, it suffices to prove this in the case where $Y$ is a strict Henselian ring and $A\to Y$ is the inclusion of the special point. In this case, it becomes equivalent to showing that the natural map $\Gamma_X(F)\to \Gamma_{X_A}(F\rvert_{X_A})$ is an equivalence of groupoids for all constructible étale stacks $F$ on $X$.

It also follows from proper base-change for constructible sheaves of sets and the obstruction theory of $1$-sheaves that we can reduce to the case where $F$ is a constructible gerbe.

Unfortunately, the proof seems to use Noetherianness in a tricky way, where the key step of the proof seems to be a Noetherian induction argument on closed subsets (see loc. cit. VII.2.2.14-15). My intuition is that there should be some way to apply absolute approximation to reduce to the Noetherian case, but I have no idea how to approximate Henselian pairs (or if they even have Noetherian approximations in general).

Can these Noetherian hypotheses be eliminated? If so, how? Is there anywhere in the literature to take a look?