It depends on what you mean by "fully featured" but Isabelle supports ZF logic [1] and also you can do ZFC in Isabelle/HOL [2]. And, of course there is Mizar [3

It depends on what you mean by "fully featured" but Isabelle supports ZF logic [1] and also you can do ZFC in Isabelle/HOL [2]. And, of course there is Mizar [3]. [1] https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html https://isabelle.in.tum.de/dist/library/ZF/ZF/index.html [2] https://www.isa-afp.org/entries/ZFC_in_HOL.html https://www.isa-afp.org/entries/ZFC_in_HOL.html [3] http://mizar.org/ http://mizar.org/