Formal Verification of Blockchain Consensus Mechanisms Using Event-B

Summary

This study presents a formal verification framework for blockchain consensus mechanisms and smart contracts, employing the Event-B method. This approach combines abstraction from representation, invariant-based proof, and temporal model checking with formal checks of safety, liveness, and resistance to double-spending before deployment.

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.

Introduction

Blockchain technology has evolved into a distributed ledger paradigm that enables decentralized record-keeping without reliance on centralized authorities. By replicating ledger states across participating nodes and achieving agreement through consensus mechanisms, blockchain systems provide integrity, transparency, and tamper-resistance in open and adversarial environments. As described by Yaga et al.¹, blockchain architecture combines cryptographic primitives, distributed consensus protocols, and peer-to-peer communication to ensure that validated transactions become computationally impractical to alter. Core consensus mechanisms such as Proo....

Protocol

Study inputs
In this study, two Solidity smart contracts were used as verification inputs. The former was a Simple DAO-style contract that was used as a re-entrancy case study. The second one was a thinned-out ledger/state-transition contract designed to test contract-level constraints against double-spending. The original Solidity source code served as input to the abstraction and verification processes defined in this protocol. The general transformation process used for such contracts is illustrated in Figure 1, which shows the gradual transformation of the Solidity source code into the FSM, Event-B, and SMV models....

Results

The findings of this work combine the formal verification products of Event-B and CTL model checking with executable information from blockchain simulation. The combination of these multi-layered outputs supports the validation of key behaviors in smart contracts, their consensus systems, and their ledger-soundness limitations within the limited exemplification of the design.

Environment setup and dependency verification
The execution environment used for model transformat.......

Discussion

Formal and simulation-based verification demonstrate that the multi-layered verification system used in the given research was capable of verifying smart contract behavior, consensus-mechanism correctness, and the ledger-integrity property under the well-defined abstraction boundary. Event-B provides a mathematically grounded representation of safety properties, a state-flow, and re-entrancy-prevention logic in terms of invariants and refinement-based logic^5,6. T.......

Materials

List of materials used in this article

Name	Company	Catalog Number	Comments
Rodin Platform (v3.7.0)	Rodin Team / Eclipse Foundation	https://www.event-b.org/install.html	Event-B modeling, refinement, and proof-obligation generation and discharge
Event-B Method	University of Southampton / Rodin Community	https://www.event-b.org/	Formal modeling framework for invariant specification and refinement
nuXmv Model Checker (v2.0.0)	FBK (Fondazione Bruno Kessler)	https://nuxmv.fbk.eu/	Symbolic model checking of CTL properties
Graphviz (v0.20.3)	Graphviz Team	https://graphviz.org/	FSM visualization and graph rendering
Python (v3.10.12)	Python Software Foundation	https://www.python.org/downloads	Simulation and execution environment
Web3.py (v7.6.0)	Ethereum Foundation / Contributors	https://web3py.readthedocs.io/	Blockchain interaction and transaction simulation
NetworkX (v3.4.2)	NetworkX Developers	https://networkx.org/	Graph modeling of blockchain and FSM structures
Matplotlib (v3.8.0)	Matplotlib Development Team	https://matplotlib.org/	Plotting mining time and validator distributions
NumPy (v1.26.4)	NumPy Developers	https://numpy.org/	Numerical computations
Pandas (v2.2.2)	Pandas Development Team	https://pandas.pydata.org/	Data analysis and processing
OpenJDK 11	Oracle / OpenJDK Community	https://openjdk.org/projects/jdk/11/	Required runtime for Rodin platform
Ubuntu 22.04 LTS	Canonical Ltd.	https://ubuntu.com/download	Operating system for all experiments
Solidity	Ethereum Foundation	https://soliditylang.org/	Smart contract source language used as input
nuXmv Input Language (SMV)	FBK	https://nuxmv.fbk.eu/documentation.html	Intermediate model representation for CTL verification