We propose a novel modal logic and semantics for specifying and proving properties of distributed full-information-transfer protocols (protocols that broadcast state to all participants in a distributed system). We use this to design and prove correctness of novel generalisations of Bracha’s ‘reliable broadcast’ algorithm to a heterogeneous trust setting (where distinct participants may have distinct trust assumptions); these proofs have been mechanically formalised and checked.