I have created the SAM Pattern [1] (State/Action/Model) based on my interpretation of TLA+. The goal is to make the semantics available to developers. Why not writing code as close as possible to the way it would be specified?
SAM can also be used for stateful API/Microservice orchestrations [2]
If you want a slightly more formal introduction to SAM and its relationship to TLA+ (again, based on my own interpretation) I gave this lecture last month [3].
[2] http://www.ebpml.org/blog15/2015/06/designing-a-reliable-api...
[3] http://cloudsentinel.com/sam-state-machines-and-computation....