I don't have time to explain in detail at the moment, but I recommend reading about the history of set theory and the problems that the introduction of ZFC was meant to solve. I think you'll agree that they were both important and have nothing to do with proof verification.
More generally, it's not clear to me why you necessarily want the language you use to rigorously investigate the foundations of mathematics to be the same one you use to do proof verification. ZFC – and set-theoretic approaches more broadly – facilitate proving things about mathematics (meta-mathematical theorems), and for that they are very useful. E.g., the strength of a theory is equivalent to the size of the cardinals it assumes, loosely speaking [1].
[1] https://en.wikipedia.org/wiki/Large_cardinal