Is the following theory equivalent to Tarski-Grothendieck set theory?
The language is first order logic with equality, and membership, with axiom schemata:
Specification: $\forall A \exists! x \, \forall y \, (y \in x \iff y \in A \land \phi )$
Reflection: $(\varphi \implies \exists \alpha: \operatorname {superinclusive}(V_\alpha) \land \varphi^{V_\alpha} )$
$\operatorname {superinclusive}(X) \equiv_{df} \forall Y \subseteq X \, (|Y|<|X| \implies Y \in X)$
$\varphi$ is a first order formula in the language of set theory + defined predicates and functions, that doesn't use the symbol $\alpha$. And $\varphi^X$ is the formula obtained by merely bounding all quantifiers in $\varphi$ by $\in X$. The formula $\phi$ (of specification) is any formula that doesn't have the symbol $x$ occurring free.
This is only a partial answer to this question. It only establishes proving that $\sf TG$ set theory is a fragment of this theory!
All axioms of $\sf ZF$ would follow from Specification + Reflection on stages $V_\alpha$ of the cumulative hierarchy. This is well known (D. Scott, M. Potter 13.3).
Superinclusiveness would prove both Choice, and Tarski's axiom.
Choice is proved because each superinclusive $V_\alpha$ would be in bijection with the set $ON^{V_\alpha}$ of all von Neumann ordinals in it, since clearly $ON^{V_\alpha}$ is a cofinal subset of $V_\alpha$ (with respect to relation "strictly smaller rank"), and so it cannot be an element of $V_\alpha$, and so it must not be strictly smaller than $V_\alpha$ (superinclusiveness). Since every set is an element of some superinclusive stage, then it must be well-orderable after that bijection.
Tarski's axiom follows because every superinclusive $V_\alpha$ higher than $V_\omega$ would have $\alpha$ being strongly inaccessible, accordingly $V_\alpha$ would be a Grothendieck universe! To prove that, we see that $\alpha$ must be regular, since otherwise any strictly smaller cofinal subset of it would be an element of that stage (superinclusiveness) and thus rank-bounded within that stage, which cannot be! Also one can easily see that $V_\alpha$ must be closed on power set operator, since otherwise $\alpha$ would be a successor ordinal, and so the set $\{V_{\alpha-1}\}$ would be an element of $V_\alpha$ (superinclusiveness), which cannot be since all elements of $V_\alpha$ are subsets of $V_{\alpha-1}$. So every $\alpha$ for a superinclusive $V_\alpha$ is a regular strong limit cardinal, and when uncountable then it is inaccessible by definition.
Now, the other direction, that $\sf TG$ set theory can prove all axioms of this theory, is one I didn't reach to. And I suspect that it might not be the case. For I suspect that $\sf Ack + limitation \ of \ size$ is a conservative extension of this theory, and so this would mean that this theory is equivalent with ORD is mahlo, and accordingly stronger than $\sf TG$ set theory.