"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 mod

"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.