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 / formally verified evm golf and reverse bug bounties

  • YouTube
  • IPFS
  • Details

Formally verified EVM golf and reverse bug bounties

Duration: 00:52:05

Speaker: Lev Livnev, Martin Lundfall

Type: Breakout

Expertise: Advanced

Event: Devcon

Date: Jul 2026

With the formalized semantics of the EVM in the K framework (the Jello paper), a new arsenal of analysis tools has become available for Ethereum smart contract development. This workshop will demonstrate how this tooling can be used to verify the complete behavior of smart contracts, sharing the techniques and tools used to verify the core contracts of multicollateral dai.We will demonstrate the power of formal verification by presenting the Ethereum community with two challenges:In the first one, we invite the workshop participants to a round of formally verified EVM golf. The most gas efficient implementation of an ERC20 contract which provably matches the specification wins!In the second challenge, the task is to challenge the specification itself, by writing a passing adversarial smart contract. In this "reverse bug bounty", participants are invited to poke holes in a specification by writing smart contracts which satisfy the postulated requirements but are otherwise faulty in some way.

Categories

Developer Infrastructuretechnical