Dear Colleagues,

The development of blockchain applications and systems usually involves interactions between different systems and components. Hence, modelling and simulation are important aspects of blockchain software development. Modelling may involve the elicitation of system requirements and description of architecture and components that are part of blockchain systems. Simulation helps in understanding the dynamic behaviour of a software application. Due to the complexity of blockchain applications and systems, it has become increasingly important to apply formal methods in their development. This will help in achieving consistency and correctness of the static and dynamic properties that define the developed software artefact.

Formal methods for modelling and simulating blockchain systems may include Set theories, Game theories, Algebraic equations, Differential equations, Formalized pseudocode algorithms, Petri nets, etc. Applying any of these methods in software development demonstrates rigour and improves the verifiability of a software artefact.

This Special Issue seeks to collect articles that apply any of the listed (not limited to) above formal approaches in the development of blockchain applications. In addition, there is a special consideration for authors that applied formal methods in requirement analyses of blockchain systems and applications.