Is there any short document that describes the differences of TLA+ and LTL?
Linear Temporal Logic types Functional Reactive Programs. ( http://www.asaj.org/papers/plpv12.pdf )
One could then use the type system to provide a correct implementation of the specification.