Very recently, Sergei Tupailo (2010) has proved the consistency of NFSI, the fragment of NF consisting of extensionality and those instances of Comprehension (\(\{x \in A \mid \phi \}\) exists) which are stratified and in which the variable \(x\) is assigned the lowest type. Tupailo’s proof is highly technical, but Marcel Crabbé pointed out that a structure for the language of set theory in which the sets are exactly the finite and cofinite collections satisfies this theory (so it is very weak).