We propose a formal approach for specifying and implementing coordination logic in distributed systems, with a focus on smart contracts. Our model captures dynamic roles, data-driven transitions, and external coordination interfaces, enabling high-level reasoning about decentralized workflows. We implement a toolchain that supports formal model validation, code generation for Solidity (our framework is extendable to other smart contracts languages), and automated test synthesis. Although our implementation targets blockchain platforms, the methodology is platform-agnostic and may generalize to other service-oriented and distributed architectures.
We demonstrate the expressiveness and practicality of the approach by modeling and realising some coordination patterns in smart contracts.