Finite axiomatizability of $\mathrm{WA}_0$ $\mathrm{WA}_0$ (which belongs to a hierarchy of theories called the wholeness axioms) is a theory extending ZFC where there is an elementary embedding $j:V \to V$ which is non-trivial and amenable, and where the replacement and separation schemas are only applied to formulas not mentioning $j$ (except $\Sigma_0$-separation, which is equivalent to amenability).
The paper The Wholeness Axioms and V=HOD by Joel David Hamkins claims that $\mathrm{WA}_0$ is finitely axiomatizable but the proof uses the fact that $V$ is the union of a chain of elementary extensions $V_{\kappa_m} \prec V_{\kappa_n}$ and I don't know how to prove this without using replacement, which is not finitely axiomatizable.
Edited to add another question: Can the equivalence of amenability and $\Sigma_0$-separation be proven without using replacement?
Part of my reason for asking this is that I'm annoyed that the axiom of replacement (and power set and union too) seem to be almost redundant in the sense they are not needed to prove the existence of any set but only to prove that the critical sequence is cofinal (using Kunen's inconsistency theorem) and that the $\in$-induction schema follows from the axiom of foundation, so I would like to prove them from the other axioms of $\mathrm{WA}_0$ if possible, but I may post a separate question about that.
 A: (This should fix an earlier attempt...) I don't see how one can prove that $V$ is the union of that particular chain, but here is a  variant, from which we still get finite axiomatizability.
Suppose for a warm-up that the model $(M,j)$ of wholeness has wellfounded $\omega$. Define the critical sequence $\left<\kappa_n\bigm|n<\omega\right>$ externally (not in $M$). Claim: this sequence is cofinal in $\mathrm{OR}^M$. Otherwise let $\delta$ be an ordinal such that $\kappa_n<\delta$ for all $n<\omega$; then $k=j\upharpoonright V^M_{\delta+2}:V^M_{\delta+2}\to j(V^M_{\delta+2})$ is elementary and $k\in M$.
Since $M$ has wellfounded $\omega$, it follows
that $\sup_{n<\omega}\kappa_n\in M$,
and so we can take $\delta=\sup_{n<\omega}\kappa_n$, and then $j(\delta)=\delta$ and $k$ contradicts Kunen in $M$. So, since the sequence is cofinal in $\mathrm{OR}^M$, $M$ is the (external) union of the elementary chain $\left<V^M_{\kappa_n}\right>_{n<\omega}$, hence models ZF.
If $M$ has illfounded $\omega$, I don't see that we can make the same conclusion about the elementary chain (and see the comment above for a counterexample).
But I claim that there is an "internal critical sequence"
$\left<\kappa_n\bigm|n\in X\right>$ for some initial segment $X$ of $\omega^M$ (possibly a proper cut) such that each proper segment of the sequence is in $M$, and then this sequence is cofinal in $\mathrm{OR}^M$
and $M$ is the union of the corresponding elementary chain of $V^M_{\kappa_n}$, so we still get a version of the desired thing.
For given $\delta\in\mathrm{OR}^M$, we have $j\upharpoonright V^M_\delta\in M$, and can use this, working in $M$, to define some critical sequence $\left<\kappa^\delta_n\bigm|n\in X^\delta\right>$, with $X^\delta$ the largest possible initial segment of $\omega^M$. If $\delta<\beta$
then the sequence defined using $\delta$ is an initial segment of that defined with $\beta$. So let $X=\bigcup_{\delta\in\mathrm{OR}^M}X^\delta$, and $\kappa_n=\kappa^\beta_n$ for $n\in X$. Note that $X$ has no largest element. Now suppose that there is $\delta\in\mathrm{OR}^M$ such that $\kappa_n<\delta$ for all $n\in X$. Using $j\upharpoonright V^M_\delta$ we get that $X=\omega^M$ (using an overspill argument). But then we have $\delta'=\sup_{n\in\omega^M}\kappa_n\in M$ (computed from $j\upharpoonright V^M_\delta$), and can contradict Kunen in $M$.
Now observe that $M\models$"$V^M_{\kappa_m}\preccurlyeq V^M_{\kappa_n}$"
whenever $m<n$ with $m,n\in X$: This is just because $M\models$"$V^M_{\kappa_0}\preccurlyeq V^M_{\kappa_1}$", and so working in $M$, where we have $j\upharpoonright V_\delta$ for arbitratily large $\delta$s, by induction, we get $M\models$"$V^M_{\kappa_i}\preccurlyeq V^M_{\kappa_{i+1}}$" for each $i\in X$, which also by induction in $M$ is enough. It follows that (outside $M$) $V^M_{\kappa_m}\preccurlyeq V^M_{\kappa_n}$ for $m,n$ as above. Therefore $M$ is the union of this elementary chain.
Therefore (in either case) we get $M\models\mathrm{ZF}$, and hence finite axiomatizability of WA0.
Note this seems to leave the possibility that $X\subsetneq\omega^M$.
And in fact this can happen. Just start with a  model $(M,j)$ of WA0
with $\omega^M$ illfounded and $\omega\subsetneq X$ where $X$ is as above (we get this by taking an ultraproduct of a countable model as in the comment above). We may assume $X=\omega^V$. Let $X'$ be any proper cut of $\omega^V$ and $V'=\bigcup_{n\in X'}V^V_{\kappa_n}$ where $\left<\kappa_n\bigm|n\in X\right>$ is as above. Let $j'=j\upharpoonright M'$. Then note that $j':M'\to M'$ is cofinal and $\Sigma_0$-elementary, since $M'$ is the union of the elementary chain $\left<V^M_{\kappa_n}\right>_{n\in X'}$. But then $M'\models\mathrm{ZF}$, so it follows that $j'$ is in fact fully elementary. And the other axioms of WA0 easily hold for $(M',j')$. Now if we start with $(M',j')$, we would get $X'$ via the process above, but $X'\subsetneq\omega^M=\omega^{M'}$.
Remark: It looks to me like essentially the same thing works for WA$n$.
E.g. for $n=1$, use WA$0$ + the axiom "For every set $x$ and $\Sigma_1$ formula $\varphi$ and parameter $p$, there is a set $y$ such that for all $z\in x$, we have $z\in y$ iff there is $\alpha\in\mathrm{OR}$ and a satisfaction relation for  $(V_\alpha,j\upharpoonright V_\alpha)$ witnessing that $(V_\alpha,j\upharpoonright V_\alpha))\models\varphi(p,z)$". This incorporates possibly nonstandard formulas $\varphi$ in the usual way.
