I don't know what SAL is, but translating TLA+ into any backend prover is a formidable task. You would probably wind up writing a possibly correct translation for a tiny subset of TLA+. Since there already exists a TLA+ to Z3 translation, it would probably be easier to produce a complete translation to Z3 that can reason about reals. I don't know if the Event-B prover handles reals. If it does, another possible alternative is to modify their TLA+ to Event-B translator to allow you to do that. However, that would probably be hard because I don't imagine that they translate proofs. Hand translating to another prover seems to be the only reasonable alternative to modifying TLAPS.
Leslie