PaperlayerView exact revision on arXiv

Source-linked AI summary

A Survey of Smart Contract Formal Specification and Verification

Palina Tolmach, Yi Li, Shang-Wei Lin, Yang Liu, Zengxiang Li

arXiv:2008.02712v3cs.SE

TL;DR

Smart contract research needs formal specifications and verification methods because many contracts lack specifications despite their importance and exposure to security pitfalls. This survey systematically classifies modeling, specification, and verification approaches, then identifies common patterns and gaps. It finds that contract-level models with model checking are widely used for functional correctness, while program-level techniques address low-level and security-oriented reasoning.

  • Problem

    The paper addresses the lack of formal specifications for smart contracts and the need to understand how desired correctness and security properties are represented.

  • Method

    The survey systematically reviews and classifies formal models, property specifications, and verification techniques for smart contracts.

  • Results

    Contract-level models with model checking are widely used to reason about functional correctness across the considered smart contract domains.

  • Takeaways & Limitations

    Verification technique choice depends on the formal model and specification, with different approaches supporting temporal, control-flow, data-flow, correctness, and security analyses.

  • Takeaways & Limitations

    The survey excludes privacy-preserving smart contracts, treating them as an independent topic of study.

Abstract

from arXiv · show

A smart contract is a computer program which allows users to automate their actions on the blockchain platform. Given the significance of smart contracts in supporting important activities across industry sectors including supply chain, finance, legal and medical services, there is a strong demand for verification and validation techniques. Yet, the vast majority of smart contracts lack any kind of formal specification, which is essential for establishing their correctness. In this survey, we investigate formal models and specifications of smart contracts presented in the literature and present a systematic overview in order to understand the common trends. We also discuss the current approaches used in verifying such property specifications and identify gaps with the hope to recognize promising directions for future work.

1 INTRODUCTION

The survey addresses the need for formal specification and verification of smart contracts amid growing adoption and documented security incidents. It systematically reviews models, property specifications, verification techniques, and research gaps.

  • Smart contracts automate blockchain actions and support applications across sectors including supply chain, finance, legal, and medical services.
  • Security incidents, including theft and frozen funds, have accompanied blockchain and smart contract adoption.
  • The survey reviews formal models, domain-specific properties, and formalisms for specifying and verifying smart contract correctness.
  • 1.1 Methodology: The authors collected 202 papers published from September 2014 to June 2020 using database searches, snowballing, inverse snowballing, and later updates.The initial search found 70 in-scope papers, snowballing added 85, and later searches added 47.
  • 1.1 Methodology: The authors do not claim to provide a complete set of properties that smart contracts should meet.
  • 1.2 Related Works: The survey classifies analysis approaches through a four-layer framework and develops a taxonomy of smart contract specifications across domains.

2 A TAXONOMY OF SMART CONTRACT MODELING FORMALISM

Smart contract modeling formalisms are classified into contract-level and program-level categories according to their abstraction level. Contract-level approaches represent high-level behavior without usually modeling implementation and execution details.

  • Smart contract formalisms divide into contract-level and program-level approaches based on the abstraction level used for modeling and analysis.
  • Contract-Level Models: Contract-level approaches describe a contract’s high-level behavior while usually omitting technical implementation and execution details.

2.1 Contract-Level Models

Contract-level models abstract away internal execution details to represent how smart contracts interact with users and external agents. The survey covers process algebras, state-transition and probabilistic models, visual and set-based formalisms, and frameworks that support analysis or contract synthesis.

  • Contract-level abstraction: Contract-level models treat smart contracts as black boxes that receive transactions, produce observable events, and may irreversibly alter blockchain state.Users, transactions, balances, parameters, and externally observable outcomes are modeled while internal execution details are abstracted.
  • Process algebras: Process algebras model smart contracts and users as interacting concurrent processes, supporting translations from Solidity or implementation in domain-specific languages.CSP and SAPIC translations represent public functions and can expose vulnerable transaction sequences or trace-level safety violations.
  • State-transition systems: State-transition formalisms represent contract behavior through explicit states and transitions, including FSMs, timed automata, and Petri nets.Applications include modeling auction states, reasoning about time constraints, checking reachability of vulnerable states, and generating Solidity from workflow models.
  • Visual modeling and synthesis: Visual modeling frameworks translate BPMN, UML, or FSM specifications into Solidity or verification models for deployment, analysis, or provably safe contract generation.Caterpillar and Lorikeet translate BPMN models, while VeriSolid translates FSM models through BIP into NuSMV input.
  • Probabilistic and multi-agent models: Probabilistic and multi-agent transition models capture nondeterministic user behavior, strategies, fairness, correctness, expected payoffs, and incentives for dishonest behavior.Examples use Markov decision processes, concurrent games, strategic games, and interface automata with model checking.
  • Set-based methods: Event-B and TLA+ use set theory and logic to specify smart contracts and support refinement, verification, design patterns, and correct-by-design implementation.Requirements can constrain variable values, participant states, authorized callers, and legally permitted events.

2.2 Program-Level Models

Program-level models represent smart contracts through lower-level artifacts such as source code, bytecode, ASTs, CFGs, and program logics. These representations support syntactic, control-flow, symbolic, information-flow, and deductive analyses, while introducing challenges in recovering execution semantics and environment details.

  • Program-Level Models: Program-level models provide a white-box view of contract execution using source code, compiled bytecode, and derived representations.They complement contract-level models, which capture high-level interactions but provide limited insight into internal execution details.
  • 2.2.1 AST-Level Analyses: AST analyses commonly check predefined code patterns and support lightweight pre-analyses before heavier verification techniques.Applications include detecting dangerous imports, checking ERC20 compliance, locating possible overflows, decoding memory layout, and systematic instrumentation.
  • 2.2.2 Control-Flow Automata: CFGs describe operational semantics as labeled directed graphs whose nodes are program locations and edges are possible transitions.Recovering Ethereum CFGs from bytecode is non-trivial because stack-sensitive jump resolution and inter-procedural or inter-contract analysis are required.
  • 2.2.2 Control-Flow Automata: CFG-based analyses include control-flow, data-flow, and symbolic execution techniques adapted from traditional software analysis.Ethainter, for example, uses information-flow analysis on Solidity traces to reveal composite vulnerabilities reached through transaction sequences.
  • 2.2.2 Control-Flow Automata: CFG extensions with annotations allow custom constraints, invariants, inter-contract flows, inter-transaction flows, and vulnerability patterns.Annotary, Solar, and SmartScopy illustrate annotation-based extensions for specifying or detecting contract properties.
  • 2.2.3 Program Logics: Program logics provide formal proof rules for statically reasoning about smart-contract behavior, including correctness, knowledge, trust, accountability, and legal obligations.The surveyed approaches use Hoare, rewriting, reachability, epistemic, authority-algebra, first-order, dynamic, deontic, and defeasible logics.
  • 2.2.3 Program Logics: Hoare-style and reachability approaches verify properties through theorem proving, model checking, or executable semantic frameworks such as K.These systems rely on formal semantics for languages or bytecode including EVM, Solidity, Michelson, and Java-based contract representations.
  • 2.2.3 Program Logics: Logic-based languages also support legal smart contracts by representing contractual obligations, permissions, prohibitions, and related legal semantics.Formal Contract Logic is used to encode legal smart contracts as logical rules.

2.3 Summary

The survey contrasts abstraction levels and shows that each supports different reasoning goals. Higher-level models clarify interactions, whereas lower-level and bytecode representations expose execution and resource details but complicate semantic specification.

  • 2.3 Summary: Contract-level models capture high-level interactions with users, other contracts, and the blockchain, but abstraction creates a gap from original execution logic.Program-level representations instead provide intuition about lower-level execution details.
  • 2.3 Summary: Bytecode-level modeling supports low-level reasoning about resource consumption but complicates specification of semantic properties concerning smart-contract behavior.The survey therefore presents abstraction choice as a trade-off between execution detail and behavioral expressiveness.

3 SURVEY ON SMART CONTRACT SPECIFICATIONS

The specification survey reviews formal languages for expressing smart-contract requirements and organizes them by abstraction level and property type. It distinguishes contract-level from program-level specifications and covers properties including security and functional correctness.

  • 3 SURVEY ON SMART CONTRACT SPECIFICATIONS: Smart-contract requirements are usually expressed as formal properties describing program behaviors.The survey reviews the formalisms used to specify these properties and the property types addressed in the literature.
  • 3 SURVEY ON SMART CONTRACT SPECIFICATIONS: Formal specifications are categorized into contract-level and program-level approaches, corresponding to high-level and lower-level views of smart contracts.The survey also reviews property classes such as security and functional correctness.

3.1 Formal Specifications for Smart Contracts

Formal smart-contract specifications span contract-level logics for high-level behavior and program-level assertions or execution patterns for implementation details. The survey covers temporal, legal, behavioral, and correctness properties alongside the formalisms used to express and verify them.

  • 3.1 Formal Specifications for Smart Contracts: Contract-level specifications describe high-level contract properties, while program-level specifications govern lower-level implementation behavior.This distinction corresponds to model-oriented and property-oriented specification traditions.
  • 3.1.1 Contract-Level Specification: Temporal logics express safety and liveness properties over smart-contract executions and are the most prevalent contract-level logic category.LTL describes properties along a single sequence of states, whereas CTL quantifies over branching future paths.
  • 3.1.1 Contract-Level Specification: Auction specifications use temporal formulas to constrain event order, including prohibiting bids after closing and restricting withdrawals until finishing.Figure 6 presents corresponding LTL and CTL formulations for auction-contract properties.
  • 3.1.1 Contract-Level Specification: Dynamic logic incorporates program termination into property specifications, while deontic and defeasible logics represent legal modalities and rule exceptions.Deontic logic addresses obligations, permissions, and prohibitions; defeasible logic additionally represents clause superiority for disputes and breaches.
  • 3.1.1 Contract-Level Specification: Other contract-level approaches use temporal first-order logic, Coq predicates with temporal connectives, role-based access control, predicate logic, and ambient constraints.These formalisms address process traces, Scilla behavior, and location- or time-based crypto-wallet access policies.
  • 3.1.2 Program-Level Specification: Program-level specifications include Hoare-style assertions and predefined patterns over instructions or execution events.Hoare triples relate preconditions and postconditions, while Solidity require and assert statements can encode preconditions, invariants, and postconditions.
  • 3.1.2 Program-Level Specification: Hoare-style and pattern-based specifications support verification of correctness and detection of vulnerabilities through symbolic execution and other analyses.Pattern-based methods can identify problematic traces, while VeriSol translates state-machine policies into source-code assertions to check state transitions and initial states.

3.2 Properties Classification by Domains

The survey classifies smart-contract properties across security, privacy, resource, business, and fairness concerns, connecting these domains to different specification formalisms. It reviews how such properties are expressed and verified, including vulnerabilities, access control, invariants, temporal behavior, and application-specific guarantees.

  • Property domains: Smart-contract properties cover vulnerability absence, privacy, resource consumption, business-rule conformance, and fairness.The survey organizes its proposed categorization around property domains observed in the literature.
  • Security: Security properties address liquidity, atomicity, single-entrancy, arithmetic correctness, access control, and resistance to gas-exhaustive patterns.Violations correspond to vulnerabilities such as greedy contracts, unchecked calls, reentrancy, integer overflow or underflow, and denial of service.
  • Security verification: Symbolic execution detects vulnerable traces and path patterns, including timestamp dependence, suicidal behavior, and unauthorized fund or control transfers.Tools inspect path conditions and traces derived from a contract control-flow graph.
  • Privacy: Privacy specifications use variable annotations to restrict readership, with zkay and Raziel supporting privacy guarantees that can be certified using zero-knowledge protocols.The survey distinguishes privacy annotations from broader privacy-preserving smart-contract research.
  • Asset Tracking: Asset-tracking properties can verify proportional energy-market allocation, eventual market closure, and optimization of the total number of exchanged tokens.These guarantees are reported for marketplace contracts matching buying and selling offers.

3.3 Summary

Smart-contract properties express security requirements and semantic conformance through multiple formalisms. The survey emphasizes path-level patterns, Hoare-style properties, and temporal logic, while identifying limited attention to low-level execution details in contract-level models.

  • 3.3 Summary: Vulnerabilities are often detected through path-level patterns in the control- and data-flow of smart-contract execution.Hoare-style properties can also capture vulnerable conditions and semantic correctness at the program level.
  • 3.3 Summary: Temporal logic is considered suitable for specifying blockchain’s multi-agent execution environment, including temporal and probabilistic constraints and user strategies.Contract-level behavioral specifications often use temporal logics because smart-contract execution relies on temporal conditions.
  • 3.3 Summary: Contract-level modeling and specification techniques seldom consider low-level execution details.The survey presents this as a limitation of existing approaches.

4 SMART CONTRACT FORMAL VERIFICATION TECHNIQUES

Formal verification techniques for smart contracts span model checking, theorem proving, symbolic execution, program verification, runtime verification, and testing. Their suitability depends on the formal model and specification, while practical trade-offs include abstraction limits, incomplete path exploration, unsoundness, and runtime overhead.

  • 4 SMART CONTRACT FORMAL VERIFICATION TECHNIQUES: The survey reviews techniques and tools for verifying smart contract models and properties, with Table 1 providing a partial tool summary.The techniques are assessed against the properties outlined for smart contracts.
  • 4.1 Model Checking: Model checking verifies finite-state contract models against temporal specifications and supports concurrency, nondeterminism, time constraints, liveness, liquidity, and deadlock- or livelock-freedom.The survey identified 18 model-checking techniques, including seven using NuSMV or nuXmv.
  • 4.1 Model Checking: Model checking is constrained by state explosion, abstraction requirements, execution simplifications, and limited feasibility of precisely modeling the blockchain environment.High-level representations also rarely capture blockchain execution details.
  • 4.2 Theorem Proving: Theorem proving encodes systems and properties in mathematical logic to derive proofs, supporting infinite systems and formal semantics across multiple smart-contract language levels.Coq, Isabelle/HOL, and Agda support reasoning about language properties and contract correctness conditions.
  • 4.2 Theorem Proving: Theorem proving expresses correctness, security, and gas-consumption conditions precisely, but usually gives limited attention to inter-contract communication and temporal properties.Trace-semantics formalization enables temporal-property verification for Scilla smart contracts.
  • 4.3 Symbolic Execution: Symbolic execution explores multiple concrete paths through reconstructed bytecode control-flow graphs and is widely used to detect predefined smart-contract vulnerabilities.The survey found 22 symbolic- and concolic-execution applications, with nine-tenths relying on Z3 for path constraints.
  • 4.3 Symbolic Execution: Inter-transactional symbolic verification targets composite vulnerabilities but faces path explosion and bounded invocation depth; VerX additionally models gas mechanics and interacting contracts.Gas-aware pruning removes paths unreachable because of out-of-gas exceptions.
  • 4.4 Program Verification: Program verification encompasses 42 publications and uses translated verification languages for automated analyses of correctness, security, data flow, control flow, and composite vulnerabilities.Static analyses may abstract execution and memory unsoundly, and gas mechanics are often omitted.

5 DISCUSSIONS

The survey finds distinct but complementary verification patterns: contract-level models commonly support functional reasoning, while program-level and runtime techniques target security properties. It also identifies execution-model, temporal-property, runtime, and ecosystem limitations, alongside directions including safer languages, repair, hybrid analyses, and standards.

  • Current approaches: State-transition models with temporal logic and model checking dominate contract-level verification, especially for functional correctness.
  • Current approaches: Program-level verification commonly uses Hoare-style specifications, theorem provers, symbolic execution, and verification toolchains to analyze behaviors and security patterns.Security analyses often identify issues along paths matching predefined vulnerable patterns.
  • Current approaches: Runtime verification monitors execution traces through contract instrumentation, instrumented clients, or off-chain event tracking for compliance applications.Instrumentation can use assertions, while off-chain monitoring supports escrow and supply-chain compliance checking.
  • Open challenges: Known-pattern analysis is limited to vulnerabilities represented by expert-defined patterns, although specification languages and invariants can broaden detectable cases.
  • Open challenges: Verification must model platform-specific execution details, including gas, memory, time, transaction ordering, fallback behavior, and inter-contract nondeterminism.These details can make high-level property specification less straightforward, particularly when gas-aware analysis operates at bytecode level.
  • Open challenges: Runtime verification is constrained by pre-deployment instrumentation, gas and bytecode limits, local client operation, private-state opacity, and non-revertible offline analysis.
  • Open challenges: The ecosystem lacks clear development standards and tool-chain guidance, while differing platforms require substantially different specification and vulnerability-detection approaches.
  • Future directions: Promising directions include safe languages, self-healing contracts, hybrid online/offline and contract/program-level analyses, collaborative standards, verified libraries, and curated benchmarks.Safe languages use design restrictions or formal guarantees, while hybrid analyses aim to connect behavioral specifications with execution precision.

6 CONCLUSION

The survey classifies formal modeling, specification, and verification approaches for smart contracts and relates domain properties to verification capabilities. It finds model checking common for functional correctness, while program-level and runtime techniques address security properties, and its holistic analysis exposes limitations.

  • The survey provides a comprehensive classification of smart contract modeling, specification, and verification approaches.
  • Contract-level models and specifications combined with model checking are widely used for functional correctness across considered domains.
  • Program-level representations are often analyzed for security properties using symbolic execution, program verification toolchains, or theorem proving.
  • Runtime verification can identify security issues in smart contract execution traces.
  • A holistic survey perspective correlates contract properties with verification capabilities and uncovers existing limitations.
Loading 2008.02712v3…