In our mind we have a naive idea of what a set is, and in nature we can only observe something that behave like a finite set, ZFC (or set theories in general) tries to catch these properties in axioms. Like Peano axioms describe the nature of natural numbers, and all the "things" that behave in that way are "isomorphic to the naturals, that property seems is called categoricity (in my naive understanding is that all models of the naturals are isomorphic).
Well, I think that all agree on how sets behave, in the sense that in our experience of the word, we can see only a kind of finite set, or like a bag full of something (or empty) or as a property (comprension axiom), and all sets are finite.
My question is there is a concept of set (axioms), that have a "unique interpretation" and are exactly the naive concept of set?
If we really want to consider finite sets, we want not only that they will be finite but also that their elements will be finite, and the elements of their elements will be finite, and so on. In short, we want that the transitive closure of the set will be finite. (Where the transitive closure of a set $x$ is the smallest set $y$ such that $x\subseteq y$ and $t\in s\in y\rightarrow t\in y$.)
In a model of $\sf ZFC$ we can define the set of all hereditarily finite sets. This is commonly denoted by $V_\omega$. It is a countable set, and in fact it is exactly the [increasing] union of $\mathcal P^n(\varnothing)$, the iterated power set operation of the empty set.
To add more on this, $V_\omega$ satisfies all the axioms of $\sf ZFC$ except the axiom of infinity, and it does satisfy its negation: there is no inductive sets, and therefore there are no infinite sets either. So does this theory, $\sf ZFC$ with the axiom of infinity replaced by its negation good enough to decide what are finite sets?
Generally, it seems that yes. But as any first-order theory with infinite models, we can produce models of the same theory which are as large as we want, and that's not very good. But much like with the real numbers, or with $\sf PA$, we can move to second-order logic (with full semantics) and have a categorical theory!
We slightly modify our theory, and instead of the schema of replacement for definable sets, we add a full-blown second-order axiom of $\in$-induction:
This should be, if I am not mistaken, to a second-order formulation of the replacement schema, although I don't recall the proof at this moment.
Why does this guarantees that there is only one model? Suppose that $M$ was a model of our modified theory, then it has a naturally defined power set operation and an empty set. Construction by recursion $V_\omega$ as the union of the finite iterations of $\mathcal P^n(\varnothing)$, and we have a class satisfying the assumption of this induction axiom. Therefore it must be equal to the whole universe!
Note that the above proof happens outside the model $M$. Very much like how the proof that there is only one model of $\sf PA_2$ occurs outside $\Bbb N$.
It seems to me that this theory is reasonable to capture what is truly finite in the universe of sets.