Yes, the theory underlying TLA+ is a variant of ZFC. In most presentations that I am aware of, it is written "Zermelo-Fraenkel set theory" (sometimes "... with choice"), avoiding the more technical abbreviations ZF and ZFC.
I would say that a perfectly accurate description would be "Zermelo-Fraenkel set theory with the transfinite axiom"
(since the axiom of choice is implied.)
Zermelo's picture by the way.
http://fr.wikipedia.org/wiki/Ernst_Zermelo
--
FL