Event-B and \(\text{ TLA}^+\)  are two formal languages based in set theory. It is thus natural to exchange models between them. The work presented in this paper has been partly supported by the French ANR ICSPA project, which focuses on studying formal methods based on set theory (B, Event-B, TLA+ ) and by the ANR EBRP project which focus on enhancements of the Event-B method. It aims at translating Event-B models, proof obligations, and their corresponding proofs to the \(\text{ TLA}^+\)  environment. While the translation of models has been previously studied in [9], we extend this work by generating various proof obligations in TLA \(^{+}\) . Finally, we address the translation of proofs interactively constructed in the Rodin platform into the \(\text{ TLA}^+\)  proof script language.