In studies of ZFC, it is conventional to take Peano arithmetic (hereafter PA) as the metatheory. However, I don't like this convention; I think a better approach would be a metatheory (like ZF-fin with $\in$-induction, or whatnot) that describes $V_\omega$, the universe of hereditarily finite sets. This creates a cleaner interface between the metatheory and the object theory, in my opinion.
Now suppose we instead wish to study ETCS. We could take Peano arithmetic as our metatheory; but, by the above argument, this probably isn't the right thing to do. We're better off having a metatheory that describes the category of finite sets. So I ask: Has anyone successfully axiomatized the category of finite sets in such a way that the resulting theory is bi-interpretable with PA?