Towards verifying ethereum smart contract bytecode in Isabelle/HOL

TLDR

Blockchain technology, particularly Ethereum’s smart contracts executed on the EVM, is increasingly used for financial and mission‑critical applications, yet errors can cause significant loss, making formal verification essential for ensuring correct behavior. The paper extends an existing Isabelle/HOL EVM formalisation by adding a sound bytecode‑level program logic. Bytecode sequences are partitioned into straight‑line code blocks, and a program logic is constructed to reason about these blocks. This abstraction advances control over the cost and complexity of formally verifying EVM smart contracts.

Abstract

Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety-, security-, or mission-critical purposes. Errors in smart contracts have led and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of straight-line code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts.