Blockchain technology, a type of distributed ledger, continues to increase in popularity. As widely distributed systems, these designs describe protocols that are complex and difficult to reason about. The stake distribution in blockchain protocols is described by the resolution of all transactions included in the chain. Proof-of-stake blockchain designs depend on this distribution of stake to elect agents to mine new blocks, form an agreement on the state of the chain, and incentivise honest behaviour. Formal modelling techniques can be used to provide insight into distributed systems and are therefore appropriate for analysis of such blockchain protocols. However, careful considerations must be made to describe models mathematically in a way that the formal modelling techniques can be applied to provide useful insights.

This work considers how abstractions of proposed proof-of-stake designs can be captured in a way that is appropriate for the application of formal modelling techniques. Designs are described in terms of three core design elements: election mechanism, consensus rules, and incentive structure. They are modelled as fully connected, synchronised, and static multi-agent systems. This approach appropriately bounds the state space of the models, permitting the application of model checkers. A formal framework is presented that applies probabilistic model checking to these design abstractions, analysing models against several desirable proof-of-stake properties. These properties are resource proportional elections, block finalisations, and rewards. They describe an agent’s ability to perform in these protocols in relation to the stake they own. The consideration of these properties is examined in models that explore the protocols in the context where all parties behave correctly, and they are also considered in the context of adversarial agents performing stake-specific attack strategies; Sybil and pooling attacks, where agents split and pool their stake, respectively, in an attempt to gain an advantage. This framework is then applied to three proof-of-stake design proposals: Peercoin, Ouroboros, and Algorand. Application of our formal framework successfully demonstrates the value of formal modelling in this setting, providing insights that help form discussions on design choices and parameters.