Report
Towards a B-Method Framework for Smart Contract Verification: The Case of ACTUS Financial Contracts
Abstract
The increasing use of advanced smart contract structures in finance necessitates rigor and scalability in ensuring their correctness. Traditional auditing falls short of comprehensive security; formal verification offers a robust, scalable approach to secure-by-design models. We introduce a B-method framework for modeling and verifying smart contracts based on the ACTUS standard for financial instruments, converting ACTUS specifications into B-method constructs to systematically model, analyze, and verify financial contract implementations on-chain.
Executive summary
As financial logic moves on-chain, correctness stops being a code-quality nicety and becomes a systemic requirement. This paper — presented at CRiSIS 2023 — argues that auditing alone cannot deliver that assurance, and develops a B-method framework for the formal verification of smart contracts built on the ACTUS standard for financial instruments.
By translating ACTUS specifications into B-method constructs, the work brings a systematic, secure-by-design discipline to modeling, analyzing, and verifying financial contract implementations in the blockchain context. The full paper follows below.