 New Foundations with urelements

NFU has a universal domain, a predicate $S$ distinguishing sets from atoms, extensionality restricted to sets, and comprehension for stratified formulas. Atoms have no members. Every stratified predicate has a set extension, including the always-false predicate, so there is a distinguished empty set even when atoms exist. Permitting atoms removes the full-extensionality obstacle in New Foundations.