Currently going through Simpson's "Subsystems of second order arithmetic", which I believe is the ultimate reference in reverse mathematics, after having completed (more like peeked) Stillwell's "Reverse Mathematics". However, I'm having some troubles following his foundations and his approach to set theory.
After some (slightly odd) remarks about the distinction between what he calls set-theoretic and non-set-theoretic (or ordinary) mathematics, he states
In this book we want to restrict our attention to ordinary, non-set-theoretic mathematics. The reason for this restriction is that the set existence axioms which are needed for set-theoretic mathematics are likely to be much stronger than those which are needed for ordinary mathematics.
which is true in light of the approach he's going to take to distinguish the different axiomatic systems. But, right after that, he starts talking about sets, set variables, set memberships, the natural numbers set, etc. without giving a construction or explaining how these are supposed to work, since obviously this cannot be ZF.
The question is how can we formalize this idea of sets and their properties without giving them too much power to actually be unable to create different axiomatic systems that are not equivalent. My bet is ZF without the axiom of specification (and possibly replacement, but I might be totally wrong about this) should suffice, since then we can add the suitable comprehension axioms without them being already "true" by the set theory axiomatic, but I haven't found any discussion about this topic.