Using TLA+ to Model Cascading Failures

I have been modelling parts of our systems in TLA+ for years now and it really helps a lot working out complex scenarios.

Anyone here can shed some light on how to incorporate tla+ into an agile process?

Can anyone advise on whether it’s worth modelling general critical systems in TLA+ where they are not distributed?<p>In broad strokes, how does one make sure that your real system indeed behaves like your model?

It seems TLA+ would be a really great fit for modeling actor systems, has anyone found good examples of this, for instance for Akka or Erlang?