Strategic Reasoning of BitML Smart Contracts using the MCMAS Model Checker

This work proposes a novel formal verification technique to analyze Bitcoin smart contracts (when specified in BITML) through ATL model checking, using the MCMAS model checker. In particular, we developed a translation procedure from a BITML contract to a MCMAS model that simulates the BITML semantics, hence allowing for strategic reasoning on BITML smart contracts. We implemented the technique in a prototype tool, which we tested over several case studies, showing that we can verify smart contract specifications that capture interesting multi-agent interactions and strategic specifications.