Formal Verification of the Burn-to-Claim Blockchain Interoperable Protocol

Abstract

This paper introduces an abstract blockchain model that employs the Burn-to-Claim cross-blockchain protocol [1]. This multi-level simulator models a virtual environment of nodes running on the Ethereum Virtual Machine (EVM). Developed using the $$CSP\#$$ language [2], it has undergone formal verification with the model checker PAT. Focusing on inter-network operations, our model ( https://github.com/b-pillai/Burn-to-Claim-formal-verification ) examines the properties of correctness, security, and atomicity using PAT. Surprisingly, atomicity, assumed to be inherent in the time-lock mechanism of the Burn-to-Claim protocol, does not always hold. We establish its validity under specific assumptions while confirming the protocol’s correctness and security under the added assumptions.