The starting point is a paper on "Non-blocking atomic commitment" by Babaoglu and Toueg, from Mulender's book on Distributed Systems. They present an algorithm for distributed atomic commitment that enjoys different sets of properties depending on what type of broadcast is used. They give an informal correctness proof which they claim is compositional, although I'd rather call it incremental (when the algorithm is modified, the proof is modified accordingly, some parts being reused).