My rambling comments are starting to cohere into a quasi-answer, though not a definitive one:

 1. In addition to ETCS, Lawvere also formulated [ETCC](https://ncatlab.org/nlab/show/ETCC), the elementary theory of the category of categories.

One could very likely arrive at a similar axiomatization of groupiods, either by adapting Lawvere's ETCC axioms, or by directly using the fact that groupoids form a full subcategory of categories.

Of course, the way you formulate the axioms of ETCS reflects a great deal of conceptual development which has happened since Lawvere originally wrote down the theory. I don't know of a similar modernized, sleek way to package Lawvere's axioms for the category of categories, and I think that's partly because it would be harder to do / the necessary concepts may not have been studied (yet?). So if one were to groupoid-ify ETCC, there would still be more work to make the theory more "palatable".

 2. You might also be interested in [groupoid models of type theory](https://homotopytypetheory.org/references/hofmann-streicher-the-groupoid-interpretation-of-type-theory/), where groupoids are thought of in a similar way to what you suggest, lying somewhere between sets and homotopy types and undelrying a theory which can be used foundationally.

 3. I'll also point out that your idea of thinking of the underlying groupoid of a category as a sort of "improved version" of the set of objects of the category does come up. For example, this way of thinking leads to the idea of a [complete Segal space](https://ncatlab.org/nlab/show/complete+Segal+space) as opposed to a [Segal category](https://ncatlab.org/nlab/show/Segal+category). 

Because of the difficulties I alluded to above in groupoid-ifying ETCC, it may be better to return to the comparison to ETCS. The formulation you give, though it doesn't directly invoke the notion of an elementary topos, is closely related to it. A groupoid version of this axiomatization, then, would be talking about something close in spirit to a higher theory of elementary topoi. There has been a great deal of interest in formulating such a theory for a long time.

Going beyond ordinary topoi, the most famous development is Lurie's theory of (Grothendieck) $\infty$-topoi. Nima Rasekh has given a theory of [elementary $\infty$-topoi](https://arxiv.org/abs/1805.03805), but the theory is very much in its infancy.

You want something in the middle -- a [(2,1)-topos](https://ncatlab.org/nlab/show/(n,1)-topos). (The "2" means that you want your topos to be a 2-category; the "1" means that only 1-morphisms and not 2-morphisms will be non-invertible in your category.) I believe that people like Mike Shulman have thought about notions in this area, but I don't know if anything is published.

I haven't thought carefully about this, but the main thing I'd think needs to be straightened out is the following. In ordinary topoi, the subobject classifier does a great deal of work, but in in $\infty$-topoi the concept needs to be strengthened to an [object classifier](https://ncatlab.org/nlab/show/%28sub%29object+classifier+in+an+%28infinity%2C1%29-topos), and size issues cause technical annoyances. The other way of thinking about what the object classifier encodes is in terms of _descent_ (a scary category-theoretic word which means different things to different people, but which in each individual case turns out to be not scary). Thinking in these terms, the theory of $\infty$-topoi actually turns out to be in some sense _cleaner_ than the theory of ordinary topoi. In fact the following is true in $\infty$-topoi but (its corresponding version) is false in ordinary topoi: if $\mathcal E$ is an $\infty$-topos, the "slice" functor $\mathcal E^{op} \to CAT_\infty$, $X \mapsto \mathcal E/X$ preserves limits. I'm not sure whether a (2,1)-topos is expected to be more like $\infty$-topoi or 1-topoi in this regard.