About well-definedness of $X_1$, "being a model of ZFC" is definable since ZFC is a recursive theory, so we could construct some $\Sigma_1^0$ predicate $\textrm{isZFCAxiom}(e)$ for $e$ a Godel-coding of a formula in the language of ZFC. Then I believe we can formalize "$M$ is a model of ZFC" by $\forall(e\in\mathbb N)(\textrm{isZFCAxiom}(e)\rightarrow M\vDash e)$ using some formalization of $\vDash$ for Godel-codes (for an explicit example, this set of notes "Models of Set Theory I" by Koepke).
Bounding $\alpha_1$: The following paragraph is an argument I heard from another MathOverflow user by personal communication.
To avoid considering arbitrary transitive models, for any transitive $M$ where $(M,\in)\vDash\textrm{ZF}$ we have $L^M\subseteq M$ and $(L^M,\in)\vDash\textrm{ZF}$. These models $L^M$ must be of the form $L_\xi$ (or $(L_\xi)^V$) for some ordinal $\xi$, and we have $\aleph_1^{(L^M)}\leq\aleph_1^M$, so without loss of minimality we can just consider the ordinals $\aleph_1^{L_\xi}$ where $(L_\xi,\in)\vDash\textrm{ZF}$. Also, to ensure we're bounding $\alpha_1$ and not just the $\aleph_1$ of the minimal model, we can show that $\gamma<\delta$ implies $\aleph_1^{L_\gamma}\leq\aleph_1^{L_\delta}$, since any bijection $\omega\rightarrow \aleph_1^{L_\delta}$ that's a member of $L_\gamma$ must also be a member of $L_\delta$. So the $\aleph_1$ of the minimal model of ZF is indeed $\alpha_1$.
From here on let $\xi$ be least such that $L_\xi\vDash\textrm{ZF}$. Each $L_\xi$ modeling ZF is admissible, so we can apply Theorem 10.2 of Arai's "A sneak preview of proof theory of ordinals", stating admissible $L_\xi$ satisfying "$\alpha$ is a cardinal $>\rho$" for some $\rho<\xi$ must have $L_\xi\cap\mathcal P(\omega)=L_\alpha\cap\mathcal P(\rho)$. Using some results from §4 of Marek and Srebrny's thesis "Gaps in the constructible universe" we obtain some weak lower bounds on $\alpha$: it's larger than the ordinal of ramified analysis $\beta_0$, and larger than the ordinal $\xi$ starting a gap of length $\beta^\beta$ of corollary 4.12. For the bonus question on $\aleph_n^M$, similar results apply when $\rho>\omega$, using the analogous notions of $\rho$-gaps (i.e. gaps in $L_\bullet\cap\mathcal P(\rho)$) introduced in §7.
Strengthening the bounds: Since we know the gap starts at $\alpha_1$ and ends at $\xi$, we can strengthen this bound by showing that the gap is long, e.g. contains many admissibles: let $\sigma_0$ be the $\Pi_3$ formula expressing "the universe is an admissible set" from Richter and Aczel's "Inductive Definitions and Reflecting Properties of Admissible Ordinals". Working in $L_\xi$, ZF proves $\forall\rho((\rho\textrm{ is a cardinal }>\omega)\rightarrow(\sigma_0)^{L_\rho})$, we assumed ZF is sound by assuming ZF has a transitive model, so $L_\rho$ satisfies this sentence. Since each relativization $(\sigma_1)^{L_\rho}$ is $\Delta_0$, each one is absolute and therefore true in $V$, so each $L_\rho$-cardinal, while not really a cardinal, is really admissible. So we get many admissibles (e.g. $\aleph_2^{L_\xi}$, $\aleph_\omega^{L_\xi}$, $\aleph_{\omega_1^{L_\xi}+\varepsilon_0^{234}}^{L_\xi}$) between the start and end points of the gap.
We can repeat this section but based on stronger properties of $L_\rho$-cardinals to improve this further. For instance Barwise's Admissible Sets and Structures has an exercise to show each $L_\rho$-cardinal $>\omega$ must be $\rho$-stable for admissible $\rho$, from which we can show each aforementioned $L_\rho$-cardinal in our gap is inaccessibly-stable. (However we need to be careful about showing these properties are absolute w.r.t. $V$)
