Proof assistant for writing mathematics
Both Coq and Isabelle can do this.

[Coq]
Here is a paper discussing how to encode ZFC in CIC, on which Coq is based.

Benjamin Werner: Sets in Types, Types in Sets (1997).
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Isabelle]
There is a library for ZF.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html