It is said in TLA+ documentation that the theory underlying the system is ZF. But technically speakingit is not true because Hilbert's epsilon (the CHOOSE construct) is used and this implies an extra axiomover ZF or ZFC namely the transfinite axiom.