Formal Verification of Blockchain Consensus Mechanisms Using Event-B

Abstract

This study develops a formally grounded verification framework for blockchain consensus mechanisms and smart contract behavior using Event-B and the Rodin platform. Unlike prior approaches that rely primarily on simulation or case-based validation of isolated contracts, this work integrates Finite State Machine (FSM) abstraction, invariant-driven proof, refinement modeling, and temporal logic verification to analyze Proof of Work (PoW), Proof of Stake (PoS), and mechanisms for double-spending prevention. Solidity smart contracts are abstracted into FSMs and encoded as Event-B machines, enabling the formal specification of state transitions and safety constraints. Safety properties-including transaction uniqueness, state consistency, access control enforcement, and ledger invariant preservation-are verified through automatically generated proof obligations in Rodin. A total of 312 proof obligations were generated, of which 287 (92%) were automatically discharged, and 25 were proven interactively, resulting in complete invariant coverage. Liveness properties were specified in Computation Tree Logic (CTL) and validated via model checking, confirming deadlock freedom and eventual validator selection under PoS conditions. Double-spending prevention was formally enforced using state-consistent ledger modeling, where uniqueness constraints were proven across all reachable states. Protocol-level consensus logic for PoW and PoS was refined across three abstraction levels, ensuring block integrity and validator correctness through stepwise refinement. The results demonstrate that machine-checked proofs provide verifiable correctness guarantees beyond simulation-based evaluation, establishing a rigorous and reproducible verification pipeline that enhances correctness assurance and protocol-level robustness in blockchain systems.