Complementing @JasonChen's answer: Assume ZFC+$I_1$ and let $j:V_{\lambda+1}\to V_{\lambda+1}$ be elementary, so $\lambda$ is the sup of the critical sequence of $j$. Then $V_{\lambda}$ models $\mathfrak{ZFC}(\mathsf{SOL})$, but $\mathrm{cof}(\lambda)=\omega$. For suppose $f:V_\alpha\to\lambda$ is cofinal and definable over $V_{\lambda+1}$ from the parameter $p\in V_{\lambda}$. Let $n<\omega$ be such that $\alpha,p\in V_{\mathrm{crit}(j_n)}$ (where $j_n=$ the $n$th iterate of $j$). Note that $j_n\circ f\neq f$, because taking $x\in V_\alpha$ with $f(x)>\mathrm{crit}(j_n)$, we get $j_n(f(x))>f(x)$. But $j_n\circ f=f$ because $j_n:V_{\lambda+1}\to V_{\lambda+1}$ is elementary and $j_n(p,\alpha)=(p,\alpha)$.
Edit, considering @AsafKaragila's comment on consistency strength: Consistency-wise, the assumption above was overkill; a measurable suffices. Assume ZFC + $\kappa$ is measurable. Let $G$ be Prikry generic at $\kappa$. So $\kappa$ has cofinality $\omega$ in $V[G]$. Claim: In $V[G]$, $V_\kappa$ models $\mathfrak{ZFC}(\mathsf{SOL})$. In fact, if $f:\omega\to\kappa$ is cofinal and $f$ is definable over $V_{\kappa+1}^{V[G]}$ from parameters in $V_\kappa$, then $f\in V$, so $f$ is bounded. Since $V_\kappa^{V[G]}=V_\kappa^V$, this is a consequence of the fact that $\mathrm{HOD}^{V[G]}_V=V$, i.e. if $X\in V[G]$ and $X\subseteq V$ and $X$ is definable over $V[G]$ from parameters in $V$, then $X\in V$. (This follows from the fact that if $p,q$ are Prikry conditions then there are generics $G_p,G_q$ with $p\in G_p$ and $q\in G_q$ and $V[G_p]=V[G_q]$.
Edit 2: On the other hand, the kind of argument used in the paper "Inner models from extended logics: Part 1" referred to in @JasonChen's answer to show that in $L$, $V_\alpha$ models $\mathscr{ZFC}(\mathfrak{SOL})$ iff $\alpha$ is inaccessible, also works for the standard fine structural $L[\mathbb{E}]$ models $M$ for short extenders, for instance if $M$ has no largest cardinal, and assuming $M$ has Mitchell-Steel indexing, though I expect it would also work with Jensen indexing. So if those models are indeed consistent through ZFC + superstrongs, then one would need more than ZFC + ``There is a superstrong extender'' to prove there is a non-inaccessible $\alpha$ with $V_\alpha$ modelling $\mathfrak{ZFC}(\mathsf{SOL})$.
(The paper "The definability of the extender sequence $\mathbb{E}$ from $\mathbb{E}\upharpoonright\aleph_1$ in $L[\mathbb{E}]$" contains enough to generalize the argument of Kennedy, Magidor, Väänänen for $L$. The definability there is all done over $\mathcal{H}_\kappa$s, as it's more convenient, but that can be translated into the cumulative hierarchy with the usual coding; in the present case that's only actually needed at the very top, since we can assume $V_\alpha\models\mathrm{ZFC}$ to start with.)