I'm mechanizing set theory (I've been working off IZF.) NBG (Von Neumann–Bernays–Gödel set theory) caught my attention because (in theory) it is finitely axiomizable.
But the class comprehension principle seems a bit awkward. I was playing with a different approach of bounding formula over sets with something like modal logic or free logic?
Your class comprehension principle becomes something like
$$ \vdash \forall x. x \in \{ y \mid P(y)\} \rightarrow \mathop{\text{M}} x $$ $$ \vdash \forall x. x \in \{ y \mid P(y)\} \rightarrow \Diamond P(x)$$
$$ \vdash \forall x. \mathop{\text{M}} x \rightarrow \Box P(x) \rightarrow x \in \{ y \mid P(y)\} $$
You add two "comprehension modalities" with rules for quantifiers like
$$ \Diamond (\forall x. P(x)) \vdash \forall x. \mathop{\text{M}} x \rightarrow \Diamond P(x) $$ $$ \Diamond (\exists x. P(x)) \vdash \exists x. \mathop{\text{M}} x \wedge \Diamond P(x) $$
$$ (\forall x. \mathop{\text{M}} x \rightarrow \Box P(x) ) \vdash \Box (\forall x. P(x)) $$ $$(\exists x. \mathop{\text{M}} x \wedge \Box P(x) ) \vdash \Box (\exists x. P(x) ) $$
And I think you want axioms
$$ \vdash \forall x y. \Diamond (x \in y) \rightarrow x \in y$$ $$ \vdash \forall x y. x \in y \rightarrow \Box (x \in y) $$
I'm most familiar with monadic modalities. I'm not really sure what works the best here.
$$ P\vdash \Diamond P$$
$$\frac{P \vdash \Diamond Q}{\Diamond P\vdash \Diamond Q}$$
$$ \frac{\top \vdash P}{\top \vdash \Box P}$$
$$ \Box P \vdash P$$
$$\Box (P \rightarrow Q) \vdash \Box P\rightarrow \Box Q$$
You would stick most axioms in the comprehension modality.
$$ \vdash \Diamond (\forall x. x \notin \emptyset)$$ $$ \vdash \Diamond (\forall x y z. z \in \{x, y\} \iff z = x \vee z = y) $$
And so on.
Something like this seems like it should work for me. But I'm not familiar with formal set theory foundations.