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

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 C S P # 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.