  Choreographic programming is a paradigm where a concurrent or distributed
system is developed in a top-down fashion. Programs, called choreographies,
detail the desired interactions between processes, and can be compiled to
distributed implementations based on message passing. Choreographic languages
usually guarantee deadlock-freedom and provide an operational correspondence
between choreographies and their compiled implementations, but until now little
work has been done on verifying other properties.
  This paper presents a Hoare-style logic for reasoning about the behaviour of
choreographies, and illustrate its usage in representative examples. We show
that this logic is sound and complete, and discuss decidability of its
judgements. Using existing results from choreographic programming, we show that
any functional correctness property proven for a choreography also holds for
its compiled implementation.
