I think the reality is that it has to be baked into the language. Here's my real attempt at that - if you model the system in the language, the compiler can reason about the distributed fleet: https://hale-lang.org/proof/