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.

devcon8 / a yellow paper you can run an independent executable evm spec in lean 4

  • YouTube
A Yellow Paper you can run: an independent executable EVM spec in Lean 4 preview
  • Details

A Yellow Paper you can run: an independent executable EVM spec in Lean 4

Duration: NaN:NaN:NaN

Speaker: Seulkee Baek

Type: Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

Ethereum's execution layer has a canonical executable specification — EELS. Jaune is an independent executable counterpart in Lean 4: one set of definitions that supports machine-checked proofs and runs the complete supported current-mainnet test corpus (5,100/5,100 fixture files, 34,005 cases, Prague through BPO2, gas and all 18 active precompiles, no FFI). This talk is what that independence turned up, told as stories. A merged correction to EELS's withdrawal decoding, found by Jaune's fixture gate demanding exact exception identities. Divergences between the transaction roots emitted by Geth and by the reference transition tool, reported upstream with proposed fixes. Then, what an independent spec is for beyond bug-hunting: a second opinion that reads like a spec, through the same t8n interface clients already speak; and a semantics you can prove against: verified compilation to bytecode, contract invariants carried to chain level, scope and trust boundaries stated exactly.

Categories

EVMFormal Verification