I think the most important point in stratification is to have what may be called a fixed membership type distance per variable.
What I mean is that if a variable $x_i$ occurs in a stratified formula $\phi$ and the stratification function assings to it a natural $n$, then all variables $y_j$ where $y_j \in x_i$ is a subformula of $\phi$ must be at a fixed $-m$ type distance from $n$, i.e. the type of each $y_i$ variable symbol is $n-m$, so we say that the type of $x_i$ is $n$ and the membership type distance from $x_i$ is $-m$. We may allow distinct variables to have different membership type distances, for example: $x \in y \in z$, we can have type assignment: $x \to 1, y \to 10 , z \to 12$.
We also have an absolue fixed equality type distance which would be set to $0$ always, so if $x_i=y_j$ occurs in $\phi$ then the both $x_i,y_j$ must receive exactly the same type indices, and so the type distance over them is $0$.
So, if a function from the variable symbols of a formula to the naturals respects the above mentioned rules of type distances, then it's to be named a stratification function, and the formula a stratified formula.
Now a formula in the typed language of $\sf TST$, can be also said to be sort-stratified if the "sort" mapping over its variables respects the above stratification rules, in other words if we can define a stratification function over its variables such that for each variable symbol $x_i$ (where $i$ is the sort of the varaible in the typed language) receives stratification index $i$.
Now for a formula $\phi$ in the mono-sorted language of set theory, we say that formula $\phi^*$ is a stratified-sorted rendering of $\phi$ to mean that it's a formula in which each variable is attached to a sort (put as subscript) in a stratified manner.
Now we define NST* in $\infty$-$\small \sf FOL(=,\in)$, as the set of all stratified-sorted renderings of axioms of Naive Set Theory "NST".
Now, I think that $\sf NF$ is interpretable in $\sf NST^*$. Also, I'd conjecture that $\sf NST^*$ is exactly $\sf TTT$ of Ranadall Holmes. Hence the question:
Is $\sf NST^* = TTT$?
PS: $\sf NST$ is the theory of Extensionality and naive comprehension, that is: $\{x \mid \phi\}$ exists for each $\phi$.
