On the specification and verification of atomic swap smart contracts (extended abstract)

Abstract

This paper investigates the specification and verification of atomic swap multi-party transactions. It is argued that logics with the ability to express properties of strategies of players in a multi-agent setting are conceptually useful for this purpose, although ultimately, the less expressive setting of temporal logic suffices for verification of concrete implementations. This is illustrated through the use of a model checker to verify atomic swap smart contracts in on-chain and cross-chain settings.