$\forall x \neg \neg \phi(x) \to \neg \neg \forall x \phi(x)$ is not intuititionistically valid. I can come up with a complicated Kripke counter-model as follows:
Let there be a countably infinite number of related states $w_0 \le w_1 \le w_2…$ and objects $a_0, a_1, a_2, …$ such that $\phi(a_0), \phi (a_1),… \phi(a_n)$ hold at each state $w_n$, and $\phi(a_{n+1}), \phi(a_{n+2}),…$ do not hold at $w_n$. So, since for every object $a_i$ at every accessible state from $w_0$ there is an accessible state where $\phi(a_i)$ holds, we have $\forall x \neg \neg \phi(x)$. However, there is no accessible state from $w_0$ where $\phi(x)$ holds for all $a_i$. Thus, we do not have $\neg \neg \forall x \phi(x)$.
This seems to be a really inefficient counter-model, but I can’t seem to figure out a simpler one in Kripke semantics. Is there a simpler approach?
There isn’t really a nicer model. Any model with finitely many states will fail. To see this, note that maximal elements are “dense” in the finite state case (every element is less than a maximal element), and note that a maximal element necessarily models $\forall x \phi(x)$, since maximal states model classical logic.
A model which has infinitely many states but only finitely many objects will also fail, though the reasoning here is somewhat more complicated.