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 Proof of Work (PoW) and Proof of Stake (PoS) regulate validator selection, block validation, and ledger synchronization. In addition, smart contracts extend blockchain capabilities by embedding programmable logic that autonomously executes predefined rules, enabling decentralized applications across sectors such as finance, healthcare, and governance. As blockchain technologies are increasingly deployed in high-value, safety-critical environments, ensuring the correctness of consensus mechanisms and smart contract behavior has become essential to maintaining operational reliability².

Despite their decentralized nature, blockchain systems remain susceptible to logical and protocol-level vulnerabilities. Double-spending attacks may occur when ledger consistency constraints are not rigorously enforced. Weaknesses at the consensus level, such as incorrect validator selection logic or flawed block validation rules, as well as smart contract vulnerabilities, including re-entrancy and improper access control, have led to substantial financial losses in deployed platforms. Although empirical testing and simulation frameworks are widely used to evaluate the behavior of PoW and PoS protocols, these approaches provide only illustrative observations rather than comprehensive correctness guarantees. Simulation-based validation cannot prove invariant preservation across all reachable states or ensure safety and liveness properties under every execution path. This limitation highlights the need for mathematically grounded verification techniques that can rigorously reason about blockchain systems beyond observational analysis.

Formal methods offer such a foundation by enabling system specification and verification through mathematical logic^3,4. Event-B extends this paradigm through stepwise refinement, representing systems as abstract state machines in which system states are constrained by invariants and transitions are modeled as guarded events⁵. The Rodin platform automatically generates proof obligations and supports their discharge, enabling machine-checked verification of invariant preservation and state consistency⁶. Classical specification techniques such as the B-Method⁷ and Z⁸ demonstrate how invariant-based reasoning and formal refinement can ensure system correctness across different development stages. These methods have been widely applied in mission-critical and safety-critical systems to ensure correctness prior to deployment^{9,10,11,12,13}. Additional extensions such as UML-B and graphical refinement frameworks further demonstrate the scalability of refinement-based modeling for complex industrial systems^{14,15,16,17,18,19}. These developments illustrate that refinement-driven formal modeling can effectively manage system complexity while maintaining strong correctness guarantees.

Formal verification approaches have also been explored for blockchain systems. SMT-based contract verification techniques automatically check assertions within Solidity programs and can produce counterexamples when logical violations occur²⁰. Tools such as VERISOL employ finite-state abstractions for smart contract verification², while theorem-proving approaches translate contracts into formal reasoning frameworks such as F*²¹. In addition, semantic formalizations of the Ethereum Virtual Machine enable rigorous reasoning about execution semantics and vulnerability detection²². Similarly, theorem-proving environments such as Coq have been applied to analyze consensus-related security properties and transactional correctness²³. While these approaches provide valuable insights, they often focus on either contract-level correctness or consensus-level properties independently. System-level ledger invariants, consensus state transitions, and smart contract behavior are rarely integrated within a unified refinement-based framework that maintains traceability across specification layers and verification artifacts. Furthermore, many existing approaches emphasize vulnerability detection or logical assertion checking rather than systematic invariant preservation across multiple refinement levels.

The present study addresses this methodological gap by proposing a unified formal verification framework that integrates Finite State Machine (FSM) abstraction of Solidity smart contracts with Event-B refinement modeling and machine-checked proof obligation discharge within the Rodin platform. Instead of treating contract verification and consensus modeling as separate problems, the proposed framework formally specifies protocol-level state transitions for PoW and PoS, ledger integrity constraints, transaction uniqueness conditions, and smart contract state evolution within a single structured model. Safety properties—including invariant preservation, transaction uniqueness, controlled state transitions, and ledger consistency—are expressed as Event-B invariants and verified through automatically generated proof obligations. Temporal and execution-order dependent properties are specified using Computation Tree Logic and verified through model checking to ensure correctness beyond static invariants. A key methodological contribution lies in establishing explicit traceability across abstraction layers: Solidity functions are abstracted into FSM transitions, FSM transitions are encoded as Event-B events, and invariants together with temporal specifications are linked directly to discharged proof obligations and model-checking results. This structured mapping ensures that each correctness claim is supported by machine-verified evidence and clearly distinguishes proof-based guarantees from simulation-based observations.

The scope of this work is deliberately constrained to ensure precision and analytical clarity. Modeling focuses on protocol-level state transitions for consensus mechanisms, ledger integrity constraints, transaction uniqueness properties, and smart contract state behavior. Network-level aspects such as message propagation delays, Byzantine adversarial strategies, fork resolution mechanisms, and detailed Ethereum Virtual Machine gas semantics fall outside the defined abstraction boundary. By explicitly defining these modeling assumptions, the framework ensures that verification claims remain aligned with formally verified proof evidence. The remainder of this paper presents the abstraction methodology, the Event-B modeling and refinement process, the procedures for invariant and temporal verification, and the resulting verification outcomes. By grounding blockchain protocol and smart contract verification in refinement-based formal modeling and machine-checked proofs, this study strengthens methodological rigor and enhances pre-deployment correctness assurance for decentralized ledger systems.

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 during verification.

Modeling boundary
Formal modeling focuses on the control-flow logic of smart contracts, including function entry and exit behavior, internal execution, and contract-level state transitions. Function visibility (public, external, internal, and private) was represented together with the corresponding call-stack behavior relevant to re-entrancy analysis. The types of abstract transitions (call, send, transfer) were treated as operations for transferring ethers.

Contract-level invariants were defined to ensure transaction uniqueness and prevent double-spending within the abstraction boundary. To represent the validation selection and block integrity requirements, the protocol-logic abstraction layer was defined in terms of the protocol-level state transitions of both Proof of Work and Proof of Stake.

The abstraction boundary did not include network-layer elements, including scheduling of messages to be delivered and delays caused by any number of hops, fork resolution, network adversaries employing Byzantine strategies, Ethereum Virtual Machine semantics, and gas semantics controlled by network nodes, exceptions propagation, asynchronous executions, intricate fallback behavior, and network-level finality. Thus, the outcomes of double-spending determination apply only to contract-level invariants and do not constitute a network-level agreement on finality.

Tools and configuration
The Rodin platform was used to model, refine, generate proof obligations, and discharge the Event-B (version 3.7.0) model, which enabled the PP, ML, SMT, and Atelier-B provers to discharge proofs automatically and interactively. nuXmv version 2.0.0 was run on the generated SMV models in full CTL exploration mode to do CTL model checking.

All verification executions were performed in a controlled computational environment using Ubuntu 22.04 LTS, OpenJDK 11, and Python 3.10.12. Web3 (7.6.0), NetworkX (3.4.2), Matplotlib (3.8.0), Graphviz (0.20.3), NumPy (1.26.4), and Pandas (2.2.2) were used to implement simulation and visualization elements. This design guaranteed that formal verification and simulation results could be reproduced when executed under the same execution conditions.

Transformation workflow
This verification process had four phases. Solidity contracts were first translated into a Finite State Machine (FSM-SC) representation. The FSM-SC model was subsequently encoded in Event-B, with clearly specified invariants and refinement degrees. The FSM-SC abstraction was translated into an SMV model in nuXmv. The verification results were reported as statistics on proof obligation discharge and CTL model checking, and counterexamples were provided as cases.

FSM construction
Each contract was abstracted as a Finite State Machine defined as:

Where:
S = set of states
S₀ = initial state
T = transition relation
V = visibility mapping
G = guard predicates
A = actions/state updates.

Algorithm 1: FSM construction from Solidity
Input: Solidity source code
Output: FSM-SC

1) Parse the Solidity contract abstract syntax tree.
2) Create the initial state S₀ from the constructor definition.
3) For each Solidity function f, create a distinct control state S_f and record visibility V(f) ∈ {public, external, internal, private}.
4) For each statement within function f, derive a transition t by extracting guard predicates from require/assert conditions and actions from state-variable updates.
5) Add transition t to T.
6) Create explicit transition types for Ether transfer operations (call, send, transfer), internal and external calls, delegatecall, selfdestruct, tx.origin usage, conditional branches, and loop constructs.
7) Return FSM-SC = (S, S₀, T, V, G, A).

And each Solidity function is associated with a different FSM control state. For vulnerability understanding, vulnerability-relevant execution flows, e.g., such flows with external calls followed by balance updates, were explicitly abstracted into ordered transitions. Figure 2 describes an example FSM-SC diagram for the SimpleDAO-style contract, showing how entry states, external-call transitions, and state-update sequences were abstracted during this construction stage.

Encoding FSM into Event-B
FSM transition was represented as Event-B constructs. All the transitions correspond to Event-B events, including particular guards and actions.

Algorithm 2: FSM to Event-B encoding
Input: FSM-SC
Output: Event-B machine and context

1) Define STATE_SET and FUNCTION in the contract context.
2) Declare variables representing FSM control state and contract-level state.
3) Represent each FSM control state s ∈ S using current_state ∈ STATE_SET.
4) For each transition (s → s′, g, a), create an Event-B event E_t with:
5) WHERE current_state = s ∧ g
6) THEN current_state := s′ ∥ apply(a)
7) Encode visibility constraints using guards derived from V(f).
8) Define invariants inv1–inv9 to capture safety and consistency properties.
9) Define INITIALISATION by assigning S₀ and default values.

The set of states, the current state, function visibility, call stack, transaction timestamp, Ether transfer status, delegate call flag, self-destruct flag, and verification condition are some of the variables that are captured in the Event-B model. The invariants (inv1-inv9) and the actions of the initializations (act1-act6) match the ones of the formal specification. Figure 3 also provides a graphical representation of how the key events relevant to vulnerabilities, especially re-entrancy-related transitions, are maintained in the Event-B encoding. This figure explains how the structural patterns of the FSM-SC model shown in Figure 2 are mapped into verifiable Event-B events.

Refinement strategy
Two levels of refinement were implemented. High-level contract control flow and core invariants were represented at the abstract level. The refined level added contract-specific restrictions, including call-stack restrictions, visibility restrictions, and re-entrancy prevention conditions.

Algorithm 3: Refinement and proof-obligation discharge
Input: Abstract machine and refined machine
Output: Discharged proof obligations and statistics

1) Generate proof obligations for the abstract machine in Rodin.
2) Execute enabled automatic provers and record discharge results.
3) Generate refinement proof obligations for the refined machine.
4) Apply automatic provers to refinement obligations.
5) Discharge remaining obligations interactively when necessary.
6) Export proof statistics and status reports.

Proof reporting included the number of invariants, refinement levels, proof obligations generated, automatic discharge rate, interactive discharge rate, and final discharge rate.

CTL property specification and model checking
The FSM-SC abstraction was translated into an SMV model for branching-time temporal verification in nuXmv.

Algorithm 4: FSM to SMV and CTL Checking
Output: PASS/FAIL verification result and counterexample traces (if any)

1. Record FSM control states as an enumerated SMV variable state.
2. Convert FSM transitions into guarded next(state) assignments.
3. Maintain flags for vulnerability-relevant conditions, such as external calls and balance updates.
4. Encode CTL properties in nuXmv and perform model checking.
5. If a property fails, generate counterexample traces representing FSM transition sequences.

CTL checking included re-entrancy order requirements, finalizing state updates after transfer operations, limiting unconstrained recursive entry into critical sections, and avoiding deadlock.

Security properties verified
The Simple DAO-style contract that prevents re-entrancy was confirmed by ensuring safe ordering between external calls and state updates via invariants and CTL constraints. Where permitted, these guards checked access-control constraints, ensuring that unauthorized transitions were restricted by invariants. The reduced ledger model verified the invariants of transaction uniqueness and ledger consistency at the level of prevention within the contract.

Outputs reported
The Results section provides reports on FSM structural metrics, Event-B model metrics, and statistics for the proof of obligation and CTL verification. The results of formal proof, and those of CTL model-checking, are given separately to distinguish the evidence of correctness guarantees by invariants, and the evidence of a time verification using temporal verification.

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