By Standard Finite Set Theory, I mean the theory coined in a langauge that extends first order logic with the below mentioned omega-inference rule, that has the following extra-logical axioms, on top of the first order identity axioms:
Extensionality: $\forall XY [\forall Z(Z \in X \leftrightarrow Z \in Y) \to X=Y]$
Empty: $\exists X \forall Y (Y \not \in X)$
Finite construction: for $n=1,2,3,...$
$\forall X_1,..,X_n \exists X \forall Y (Y \in X \leftrightarrow Y=X_1 \lor ..\lor Y=X_n)$
Define: $ \mathcal P(A)=X \equiv_{df} \forall Y (Y \in X \leftrightarrow Y \subseteq A) $
Define: for $i=0,1,2,... \\ \mathcal P_0(\emptyset)=\emptyset \\ \mathcal P_{i+1}(\emptyset)=\mathcal P(\mathcal P_i(\emptyset))$
Omega-inference-rule for finite sets: if $\psi(X)$ is a formula in which only symbol $X$ occur free, and in which symbol $X$ never occurs bound; then:
FROM SCHEMA: $for \ i=1,2,3,... \\ \forall X (X \in P_i(\emptyset) \to \psi(X))$
INFER: $\forall X (\psi(X))$
Now I think this theory is complete. The model of this theory would be the set $\sf HF$ of all well founded hereditarily standard finite sets.
Now a theory $T$ is to be labeled as $\sf HF$-Sane, if and only if every sentence $s^T$ of $T$ having all of its quantifiers completely bounded by the set $V^T_\omega$ of all well founded hereditarily finite sets of $T$, that is convertible to a sentence $s*^T$ in the language of this theory by mere removal of all bounding symbols $V^T_\omega$ from $s^T$; would have the sentence $s*^T$ being a theorem of this theory. In nutshell $T$ is $\sf HF$-Sane if and only if it doesn't prove of its well founded hereditarily finite sets some statement that is not true of sets in $\sf HF$!
Now it is very demanding that a set theory, especially one that is thought of serving as a foundation of mathematics, be assumed to be $\sf HF$-Sane. And I think that $\sf HF$-Sanity of a theory is the same as arithmetical-Soundness of it. But since we are speaking about sets, then its more prudent to speak in terms of $\sf HF$-Sanity of a set theory.
Now why we don't see "$\sf ZFC \text { is HF}$-$\sf \text{Sane}$" as an axiom extending ZFC?