Claims of the chain – a formal analysis of the blockchain protocol in B

This paper presents the first ever formal analysis of the blockchain protocol using a B language tool, ProB.

We first discuss formal methods and conduct a critical analysis of their benefits before moving on to construct a comprehensive formal model of the blockchain, focusing in particular on its current security vulnerabilities and the scalability problem that still affects the growth of all blockchain-based networks.

View paper