[ultrafilter]

Every formal axiom system, whether about sets or anything else, can only prove that N of Busy Beavers halt, for some (not-too-large in practice) finite number N. If you just want to maximize N, right now your best bet is set theory plus a very strong large cardinal axiom, like I0.

http://cantorsattic.info/L_of_V_lambda%2B1

Perhaps simply because it is older, set theory is way ahead of its competitors in developing a hierarchy of extremely strong (but apparently consistent) axioms to supplement its base theory ZFC.

[xamuel]

You're confused. Only very basic arithmetic is needed to prove that any particular TM halts (if it does halt). You might have meant to say something like, "can only prove that N of the Busy Beavers are really Busy Beavers".

[ultrafilter]

You're right. I should have written "halts last among its peers" or similar.