"There is something interesting you could try, though: You could express global correctness properties in TLA+, and show (in TLA+) that they are preserved if some simple low-level properties are preserved, and then express and verify those in JML/SPARK. This is very interesting, and I'd love to hear about such an experience (or even try it myself), but my gut feeling is that that it would still be too costly. If someone does do that, however, that's something certainly publication-worthy."

That might have been how E-SPARK connected Event-B and SPARK. TLA+ is easier to use than Evdnt-B and often in similar domains. Ill try to remember this option.