NFU is a set theory with decidable syntactic check that decides whether a formula is suitable or not to be used as a property defining a set. This feature makes NFU particularly interesting for formalization within assisted theorem provers. We discuss an implementation of a certified stratification algorithm as the first stepping stone in a larger project of implementing NFU in Coq.