We argue that high-level Petri nets are well suited for the representation of distributed algorithms as well as for correctness proofs. To this end, we provide a simple definition of high-level Petri nets, a way to formulate message-passing algorithms in this notion, a temporal-logic style language for the formulation of properties, and a proof technique which combines techniques from Petri net theory and from temporal logics. As a nontrivial case study, we present a variant of Raymond's message-passing mutual exclusion algorithm that works on arbitrary connected networks.