Devcon Archive logo
Devcon Devconnect Forum Blog
  • Watch
  • Event
    Event: background logo
    • Devcon 7
    • Devcon 6
    • Devcon 5
    • Devcon 4
    • Devcon 3
    • Devcon 2
    • Devcon 1
    • Devcon 0
    • Devconnect ARG
  • Categories
    Categories: background logo
    • Cryptoeconomics
    • Devcon
    • Developer Experience
    • Coordination
    • Core Protocol
    • Layer 2s
    • Real World Ethereum
    • Cypherpunk & Privacy
    • Security
    • Applied Cryptography
    • Usability
  • Playlists

Suggested

Loading results..

View all

About Devcon —

Devcon is the Ethereum conference for developers, researchers, thinkers, and makers.

An intensive introduction for new Ethereum explorers, a global family reunion for those already a part of our ecosystem, and a source of energy and creativity for all.

  • Watch
  • Devcon
  • Devconnect
  • Forum
  • Blog

Get in touch

devcon@ethereum.org

Subscribe to our newsletter

Crafted with passion ❤️ at the Ethereum Foundation

© 2026 — Ethereum Foundation. All Rights Reserved.

devcon 5 / formal verification of smart contracts made easy

  • YouTube
  • IPFS
  • Details

Formal verification of smart contracts made easy

Duration: 01:11:01

Speaker: Dimitar Dimitrov, Anton Permenev, Hubert Ritzdorf, Petar Tsankov

Type: Breakout

Expertise: intermediate

Event: Devcon

Date: Jul 2026

In this hands-on workshop, we will go through the process of formally verifying smart contracts. The attendees will learn (1) how to formally specify relevant functional requirements of Ethereum contracts, such as "the sum of deposits never exceeds the contract’s balance", and (2) how to verify these using existing analysis tools for Ethereum. First, we will show how to formally specify the intended behavior of smart contracts. We will look closer at safety temporal properties, an expressive class of properties for capturing which sequences of contract states are considered correct. We will present common requirement idioms, including access control, state-based properties, multi-contract invariants, and others. Next, we will provide an overview of existing testing tools, such as tools based on symbolic execution and fuzzers. The goal is to understand how they can be used to identify violations of the formalized properties as well as their limitations in providing unbounded formal guarantees. Finally, we will learn how formal verifiers go beyond testing and can provide unbounded formal guarantees (for any sequence of transactions). We will take a closer look at the specification language used by VerX and its automated verification method, which is easy to use and does not require in-depth knowledge in formal verification.

Categories

Securitytechnical