Well, TLA+ checks your 'contract' by traversing states of your model explicitly which takes a lot of time usually while in ADA we have to deduce feasibility of a contract at compile time. Checking a property of a distributed system at compile time is generally a hard problem, so I expect that ADA`s ability to do this should be rather limited.

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, and the local contract ensures that the local behavior of the various actors is correct -- and therefore results in that emergent behavior. Combined, that's a fairly solid argument that your system does what you intended.

If you had to implement the full proof in Ada, there would be no point to doing the TLA+ work.

Oh, now I see your point. Checking a TLA+ model of an algorithm and then implementing each actor in Ada reinforcing it with pre/post conditions perfectly makes sense.

Its just a little out of scope of the current thread, because the author of parent message was talking about using pure Ada/SPARK, without help of TLA+ (As I understand it in the first place), so my comment about using contracts was in that context.

No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.

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