Lets see how the world of sets could look like from the perspective of $\sf NFU$. So, here we work within the first order language of set theory, with the following extra-logical axioms:
1. Quine atom: There exists a unique Quine atom, i.e. a singleton that is an element of itself.
An "urelement" is defined as a singleton of the Quine atom. That is, it has one element and that element is the Quine atom.
2. Extensionality: if $x$ is not an urelement, then every set co-extensional with $x$ is equal to $x$.
3. Stratified Comprehension: as stated in $\sf NFU$.
4. Urelements: The set of all urelements is bijective with the set of all objects, i.e. the set of all urelements is as big as the universe.
5. Choice: as stated in $\sf NFU$.
Define: a set is said to be well founded if it is an element of every set that is a superset of its own powerset. Formally:
$$\operatorname {well-founded}(s) \iff \forall X: \mathcal P(X) \subseteq X \to s \in X$$
6. Replacement: if $A$ is a well founded set, and $\phi(x,y)$ is a formula standing for a many-to-one relation from well founded sets to well founded sets, then there is a set $\{y \mid \exists x \in A : \phi(x,y)\}$.
7. Infinity: There is a well-founded set having the empty set among its elements, that is closed under singletons.
So, this theory has a universe obeying the rules of $\sf NFU$ (but with urelements being the singletons of the Quine atom, instead of the usual formulation as element-less objects), and that has its well founded realm obeying the rules of $\sf ZFC$.
The definition of well-foundedness is due to Thomas Forster, while the theory is speaking about Holmes's $\sf BEST$ model of $\sf NFU$ with little modification.
This theory is way stronger than $\sf ZFC$ and of course $\sf NFU$, it goes high up to measurable cardinals.
Now, my question is about that definition of well foundedness which is just a recapture of stratified $\in$-induction in $\sf NFU$ terms. How this compares to the traditional definition of well foudedness:
\begin{align} \operatorname {well-founded}(s) \iff \exists t : \ & \operatorname {trs}(t) \land s \subseteq t \ \land \\&\forall v: \operatorname {trs}(v) \land s \subseteq v \to t \subseteq v \ \land \\ & \forall c \subseteq t \exists b \in c: b \cap c = \varnothing \end{align}
This definition also obeys stratified $\in$-induction.
Actually even the following simpler definition obeys stratified $\in$-induction:
$ \operatorname {well-founded}(s) \iff \\ \forall x \, (s \in x \to \exists y \in x: y \cap x =\varnothing)$