Are extendible cardinals $\Sigma_3$-reflective, choicelessly? 
Definition. A cardinal $\kappa$ is extendible if for each $\alpha$ there is $\zeta$ and $j:V_{\kappa+\alpha}\prec V_\zeta$ and $\operatorname{crit}j=\kappa$, $j(\kappa)>\alpha$.

(There was confusion about the definition of extendible cardinals. See @Farmer S's comment or my comment below on my question.)
It is well-known that extendible cardinals are $\Sigma_3$-reflective:

Proof. ($\mathsf{ZFC}$)
Let $\phi(x,y)$ be a $\Pi_2$ formula and $a\in V_\kappa$. In one direction, if $V_\kappa \models \exists x\phi(x,a)$, then $V_\kappa\models \phi(x,a)$ for some $x$, so $V\models \phi(x,a)$ since $\kappa$ is supercompact and every supercompact cardinals are $\Sigma_2$-reflecting.
For the other direction, assume that $V\models \phi(x,a)$ for some $x$. Take $\alpha>\operatorname{rank} x$ and $j:V_{\kappa+\alpha}\prec V_\zeta$, $\operatorname{crit}j=\kappa$ and $j(\kappa)>\alpha$. Then $V_\kappa\prec V_{j(\kappa)}$ and $j(\kappa)$ is inaccessible. Since $H_{j(\kappa)}=V_{j(\kappa)}$ and by the Levy absoluteness theorem, $V_{j(\kappa)}\models \phi(x,a)$. Hence $V_\kappa\models \exists x\phi(x,a)$.

The standard proof (given above) uses the Levy absoluteness theorem, whose proof uses the axiom of choice. I can see that $\mathsf{ZF}$ still proves extendible cardinals are $\Sigma_2$-reflecting, essentially by the above argument. (It requires $\Sigma_1$-reflection of supercompactness, which follows from Magidor-like characterization of supercompactness over $\mathsf{ZF}$.)

Question. Can we prove extendible cardinals are $\Sigma_3$-reflecting from $\mathsf{ZF}$?

I think the following question is relevant to the above one:

Question. ($\mathsf{ZF}$) If $\kappa$ is inaccessible, then $V_\kappa\prec_{\Sigma_1} V$?


$\Sigma_3$-reflection property of extendible are referred to papers about choiceless large cardinals (e.g., Bagaria-Koellner-Woodin, or Cutolo's doctoral thesis.) They use $\Sigma_3$-reflection of extendibles to establish the relation between extendible cardinals and Berkely cardinals, although I think we can avoid $\Sigma_3$-reflection for proving these results.

Note. I was missed that Bagaria-Koellner-Woodin uses a slightly different definition for extendible cardinals. (They called the usual extendibles as weakly extendibles. However, Cutolo used the same definition as that of mine.) Here is the definition given by Bagaria-Koellner-Woodin:

Definition. A cardinal $\kappa$ is extendible if for each $\alpha$ there is $\alpha'$ and $j:V_{\kappa+\alpha}\prec V_{j(\kappa)+\alpha'}$ such that $\operatorname{crit}j=\kappa$, $\alpha<j(\kappa)$ and for each $\beta<\alpha$, $j(A\cap V_{\kappa+\beta})=A\cap V_{j(\kappa)+j(\beta)}$, where
$$A = \{\gamma \mid V_{\gamma}\prec_{\Sigma_1^*} V\}.$$

Note that, $V_{\gamma}\prec_{\Sigma_1^*} V$ if and only if for every $\alpha<\gamma$, a $\Delta_0$-formula $\phi(x,y)$, and $a\in V_\gamma$, if $$\exists b \,[{^{V_\alpha}}\,b\subseteq b\mathrel{\land} \phi(a,b)]$$
then
$$\exists b \in V_\gamma \,[{^{V_\alpha}}\,b\subseteq b\mathrel{\land} \phi(a,b)]$$
 A: The definition of supercompactness given by Bagaria-Koellner-Woodin allows $\Sigma_2$- and $\Sigma_3$-reflection, respectively. It does not answer my original question but solves some non-trivial parts of their paper.
Let me sketch how to prove it. First, we can see that extendible cardinals are supercompact. Moreover,

Claim. If $\kappa$ is supercompact, then $V_\kappa\prec_{\Sigma_2}V$.
Proof. Let $a\in V_\kappa$ and $\phi(x,y)$ be a $\Pi_1$-formula.
For one direction, assume that $V\models \forall x\lnot\phi(x,a)$. Then $\forall x\in V_\kappa \lnot\phi(x,a)$. By supercompactness, we can find $\overline{\gamma}<\kappa$ such that $a\in V_{\overline{\gamma}}$ and $V_{\overline{\gamma}}\prec_{\Sigma_1^*} V$. Hence $\forall x\in  V_\kappa (V_{\overline{\gamma}}\models \lnot\phi(x,a))$. The rest is straightforward.
(Note that the existence of the above $\overline{\gamma}$ does not directly follow from the definition of supercompactness, since we need an additional condition that $\overline{\gamma}$ can be arbitrarily large below $\kappa$. I think modifying the proof of Lemma 222 of Woodin's Suitable Extender models I would work. In fact, I also think that the critical point of $j: V_{\overline{\gamma}}\to V_\gamma$ can be arbitrarily large below $\kappa$.)
For the other direction, assume that $V\models\exists x\phi(x,a)$ holds. Take $\gamma$ such that $b\in V_\gamma\prec_{\Sigma_1^*} V$ for $b$ such that $\phi(b,a)$. By supercompactness, we can find $j:V_{\overline{\gamma}}\to V_\gamma$ such that $\operatorname{crit}j > \operatorname{rank} a$ and $V_\overline{\gamma}\prec_{\Sigma_1^*} V$.
The rest is direct from $V_\gamma\models \exists x \phi(x,a)$.

Now we have

Theorem. If $\kappa$ is extendible, then $V_\kappa\prec_{\Sigma_3}V$.
Proof. Let $a\in V_\kappa$ and $\phi(x,y)$ be a $\Pi_2$-formula. We only prove the non-trivial direction.
Assume that $V\models \phi(b,a)$ for some $b$. Observe that if $\kappa$ is supercompact, then $A = \{\xi \mid V_{\xi}\prec_{\Sigma_1^*} V\}$ is cofinal below $\kappa$, so $V_\kappa\prec_{\Sigma_1^*} V$. (We are using that $A$ is closed under arbitrary unions.)
Take large $\alpha\in A$ such that $V_\alpha \prec_{\Sigma_1^*} V $, $\kappa+\alpha=\alpha$ and $b\in V_\alpha$.
By extendibility, there is $j:V_\alpha\to V_{\alpha'}$ such that $\operatorname{crit}j=\kappa$, $\alpha<j(\kappa)$ and for each $\beta<\alpha$, $j(A\cap V_{\kappa+\beta})=A\cap V_{j(\kappa)+j(\beta)}$. Since $V_\alpha\models (A\cap \kappa\text{ is cofinal below }\kappa)$, we have
$$V_{\alpha'}\models A\cap j(\kappa) \text{ is cofinal below } j(\kappa),$$
which implies $V_{j(\kappa)}\prec_{\Sigma_1^*}V$. Then we are done by mimicking the $\mathsf{ZFC}$-proof of $\Sigma_3$-reflection of extendibles.

