Towards a B-Method Framework for Smart Contract Verification: The Case of ACTUS Financial Contracts

The increasing use of advanced smart contract structures in finance necessitates rigor and scalability in ensuring their correctness. Traditional auditing methods fall short in providing comprehensive security, but formal verification offers a robust and scalable approach to constructing secure-by-design models and implementing smart contracts. In this paper, we introduce a B-method framework for modeling and verifying smart contracts based on the ACTUS standard for financial instruments. We start by converting ACTUS specifications into B-method constructs to bring a systematic approach to model, analyze, and verify financial contracts’ implementations within the blockchain context.