Stationary correctness of ultrapowers by low order measures
It is consistent that $\kappa$ has a unique normal measure (so, in particular, Mitchell minimal) and that measure's ultrapower $M$ satisfies $\mathcal{P}(\kappa^+)\subseteq M$, so, by your note, the ultrapower is stationary-correct.
The model is just the Friedman--Magidor model for a $\kappa$ with a unique normal measure with large $2^\kappa$. I don't know that this had been observed before, but it appears as Theorem 32 in my paper with Radek Honzík, Capturing sets of ordinals by normal ultrapowers.
I once tried and failed to answer this question in the canonical (forgive me) inner models, and your really nice observation about strong cardinals and Mitchell rank helped me finally make some progress. So thanks. Out of gratefulness, I have written the following essay of an answer. I actually only did the version for $L[U]$.
Proposition. Suppose $\kappa$ is a cardinal and $U$ is a normal ultrafilter on $\kappa$. Let $W = U\cap L[U]$. Then in $L[U]$, $\text{Ult}(L[U],W)$ is not stationary correct at $\kappa^+$.
For the proof, we might as well assume $V = L[U]$. Call an ordinal $\alpha < \kappa^+$ relevant if there is a relevance witness for $\alpha$. Relevance witness is a term I made up for a mouse $\mathcal M$ with the following properties:
- The sequence of $\mathcal M$ has a final measure $U^\mathcal M$ which is total on $\kappa$.
- $\mathcal M$ projects to $\kappa$ and is sound.
- $\mathcal M|\kappa = V_\kappa$.
- $\alpha = \kappa^{+\mathcal M}$.
To the fine-structure averse, I promise that I won't talk much more about the above conditions. They have the key consequence that there is at most one relevance witness for any ordinal $\alpha < \kappa^+$. This is a standard comparison argument which we omit. It barely uses the assumption that $V = L[U]$. It goes through below a strong cardinal (or more generally if $\kappa$ is a cutpoint of the relevant models). It follows, for example, from Lemma 1.11 in Steel's paper "Projectively well-ordered inner models."
Let $S$ be the set of relevant ordinals. Notice that relevance is absolute between $V$ and $\text{Ult}(V,U)$ since $\text{Ult}(V,U)$ is closed under $\kappa$-sequences. Therefore $S\in \text{Ult}(V,U)$. I'm going to show that $\kappa^+\setminus S$, the set of irrelevant ordinals, is stationary in $\text{Ult}(V,U)$ but nonstationary in $V$. Actually, I found it easier to prove the following equivalent statement: $S$ contains a club in $V$, but no club in $\text{Ult}(V,U)$.
Let's start by showing that in $V$, the set of relevant ordinals contains a club. (This is where we really use that $V= L[U]$.) To see this, let $\mathcal P$ be the mouse in our fine-structural hierarchy whose underlying set is $H_{\kappa^{++}}$. Since $V = L[U]$, $\mathcal P$ has a top measure which is total on $\kappa$. For any elementary substructure $H\prec \mathcal P$ containing $\kappa$ and of cardinality $\kappa$, the ordinal $\alpha = H\cap \kappa^+$ is relevant. To see this, let $\mathcal N$ be the mouse given by transtive collapse of $H$. Build the constructible hierarchy over $\mathcal N$ until you reach a mouse $\mathcal M$ that projects to $\kappa$. Then $\mathcal M$ is a relevance witness for $\alpha$.
Finally, let's see that in $\text{Ult}(V,U)$, the set of relevant ordinals does not contain a club. Assume towards a contradiction that it does. In $\text{Ult}(V,U)$, we define $D$ to be the collection of sets $A$ such that there is a club of relevant ordinals $\alpha$ with a relevance witness $\mathcal M$ such that $A\in U^\mathcal M$.
We claim that $D = U$, which contradicts that $D\in \text{Ult}(V,U)$. Clearly $D$ contains $U$, so since $U$ is an ultrafilter, we are finally done if $D$ is a proper filter. This follows immediately from the uniqueness of relevance witnesses, since for any sets $A_0,A_1\in D$, we can intersect clubs to find a single relevant ordinal $\alpha$ and witnesses $\mathcal M_1,\mathcal M_0$ for $\alpha$ such that $A_0\in U^{\mathcal M_0}$ and $A_1\in U^{\mathcal M_1}$. But the uniqueness of relevance witnesses tells us that $\mathcal M_0 = \mathcal M_1$, and so $A_0\cap A_1\neq \emptyset$ since they belong to the proper filter $U^{\mathcal M_0} = U^{\mathcal M_1}$. This concludes the proof.
OK, now that that's over, there are a number of interesting questions. What's consistency strength of stationary correct normal ultrafilters? And at what level of the canonical inner models do they occur? By your observation, it is somewhere below a $2$-strong cardinal. Actually the proof of your observation shows that if $M$ is the first mouse with an extender on its sequence that is not equivalent to a normal ultrafilter, then an initial segment of $M$ thinks there is a proper class of stationary correct normal ultrafilters. So the answer to both the consistency strength question and the inner model theory question lies way below a 2-strong cardinal, somewhere in the hierarchy of Mitchell models with higher order measurables.
I think the above proof generalizes to show that stationary correct ultrafilters do not exist in the minimal inner model for $o(\kappa) = \kappa^++1$ (or in any smaller mouse). You just have to modify Condition 1 in the definition of a relevance witness. Maybe you can make it to $o(\kappa) = \kappa^{++}$. You can also ask whether there's a model of ZFC+ GCH with a stationary correct normal ultrafilter on the least measurable cardinal.