"You wouldn't write an Ada contract describing the full system, you would write one describing the local behavior you just described in your TLA+ model. The model ensures that the emergent behavior of the system is correct, "

This is how I was seeing it happen, too.