[raphlinus]

Lean's foundations are similar to Coq. I think the ergonomics are a bit better.

Most activity in proof systems is based in type theory these days, but set theoretical systems do exist, of which Metamath is the most mature. That said, Metamath is seriously lacking in automation, so there is an element of tedium involved. That's not because of any fundamental limitations, but I think mostly because people working in the space are more motivated to do things aligned with programming language theory. There was also a talk by John Harrison a few years ago proposing a fusion of HOL and set theory, but I'm not sure there's been much motion since then.

I believe a fully featured proof assistant based in set theory would be a great contribution.

[1]: http://aitp-conference.org/2018/slides/JH.pdf

[robinzfc]

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

[2] https://www.isa-afp.org/entries/ZFC_in_HOL.html

[3] http://mizar.org/