Abstract. We look at some sources of insecurity and difficulty in reasoning about partially ordered runs of distributed ASMs, and propose some techniques to facilitate such reasoning. As a case study, we prove in detail correctness and deadlock–freedom for general partially ordered runs of distributed ASM models of Lamport’s Bakery Algorithm.