That's a pretty vague question, since it's not clear what you mean by 'construct and assess' and 'majority of mathematics'.

I'm simplyfing a good amount here, but some basic set theory is the most usual axiomatization for the basic mathematics of real analysis, topology, abstract algebra, graph theory, number theory, et al. (Z set theory plus the axiom of dependent choice is more than enough (more than enough since we don't need the axiom of regularity).)

But by Godel's second incompleteness theorem, (assuming that Z set theory is consistent, which assumption I'll take as tacit generally) there is no proof of the consistency of Z set theory in Z set theory, thus, perforce in no theory weaker than Z set theory. Especially, there is no finitistic proof of the consistency of even a basic number theory such as Peano arithmetic (not even of even weaker Robinson arithmetic).

There are lots of other approaches, but you're right that set theory is the most usual approach.

In the formal theory, we don't need to take 'set' as a primitive.

To your questions that follow: I basically agree with the outline you mentioned: informal logic->formal math->formal logic. (Or it could be informal math->formal logic->formal math if we like. Or an infinite escalation going up to formalizations of meta-theories (but then we observe that each escalation is just a clone of the previous escalation, etc.).) And I agree that at each informal stage above a formal stage, we take certain principles as given, such as modus ponens.

No matter what we do, unless we begin the whole process in an unexplained formal language, we will use certain principles informally to explain or stipulate our formalizations.

As to the extent of our informal assumptions, it seems to me that pretty much an informal version of first order logic is itself assumed. (For merely stating a formalization of the language and axioms of a formal theory like a formal set theory, I think informal versions of the principles of intuitionistic first order logic suffice?). That is reasoning that includes sentential (or at least intuitionistic sentential?) logic and the principles of universal generalization and universal instantiation. Also informal versions of the principles of identity: (1) Any object equals itself, and (2) If x equals y then whatever holds for x also holds for y.