Which kind of foundation are mathematicians using when proving metatheorems?

Your question is much more specific than your title suggests. As to the question itself, my answer is that it doesn't matter. The proof is given in mathematics, not in any formal system. A foundation for mathematics, in order to count as a foundation of mathematics, must be able to formalize most ordinary mathematical arguments. Thus, any foundation for mathematics could be used to formalize such a metatheorem.

With that said, some people care about whether metatheorems of this sort can be formalized in very weak theories. There's nothing wrong with that, but it's not something I spend my time thinking about, and in particular I didn't think about it when writing the proof you refer to. The closest I came was noting that instead of a "construction of a model" the proof can equivalently be regarded as giving a translation of first-order formulas. If you're interested in this sort of question, then Nik's answer seems reasonable to me, but I'm not familiar with the details of how this sort of thing goes.

One direction could go like this. Let ${\rm ZFC}^+$ be the theory in the language of set theory augmented by a constant symbol ${\bf M}$ with the axioms

$\bullet$ every axiom of ${\rm ZFC}$

$\bullet$ "${\bf M}$ is countable and transitive"

$\bullet$ the relativization of every axiom of ${\rm ZFC}$ to ${\bf M}$.

Then one can prove ${\rm Con}({\rm ZFC}) \Rightarrow {\rm Con}({\rm ZFC}^+)$ in Peano arithmetic, and based on the page you linked, it looks like one can straightforwardly prove the consistency of any finite fragment of ${\rm SEAR}$ in ${\rm ZFC}^+$. Thus one can prove ${\rm Con}({\rm ZFC}) \Rightarrow {\rm Con}({\rm SEAR})$ in Peano arithmetic. (If ${\rm SEAR}$ were not consistent then some finite fragment ${\rm SEAR}_0$ would be inconsistent, and this fact would be verifiable in ${\rm ZFC}^+$, so that ${\rm ZFC}^+$ would prove both ${\rm Con}({\rm SEAR}_0)$ and $\neg{\rm Con}({\rm SEAR}_0)$ and hence be inconsistent.) For details see Chapter 7 of my book.

I imagine a similar argument would work in the reverse direction to prove ${\rm Con}({\rm SEAR}) \Rightarrow {\rm Con}({\rm ZFC})$ in Peano arithmetic, but I'm not familiar with ${\rm SEAR}$ so I can't say that for sure.