The Way of Harmonious Distributed System Proofs.
In this ESOP'22 paper jointly written with Cláudio Belo Lourenço, we study principles and models for reasoning inductively about properties of distributed systems, based on programmed atomic handlers equipped with contracts. We present the Why3-do library, leveraging a state of the art software verifier for reasoning about distributed systems based on our models, and illustrate its use with a number of examples involving invariants containing existential and nested quantifiers (including Dijsktra’s self-stabilizing systems). The library promotes contract-based modular development, abstraction barriers, and automated proofs.
You can try out the library by downloading the paper’s artifact (honored with an ETAPS distinguished artifact award).