BitML2MCMAS: Strategic Reasoning for Bitcoin Smart Contracts

Abstract

We present BitML2MCMAS, a formal verification tool for analyzing Bitcoin smart contracts, when specified in BitML, through ATL model checking using the MCMAS model checker. We developed a translation procedure from a BitML contract to an MCMAS model that simulates the BitML semantics, allowing for strategic reasoning on BitML smart contracts. We tested our tool over several case studies, showing that we can verify smart contract specifications that capture interesting multi-agent strategic interactions.