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 / etheorem lean 4 consensus spec proofs

  • YouTube
Etheorem: Lean 4 consensus-spec proofs preview
  • Details

Etheorem: Lean 4 consensus-spec proofs

Duration: NaN:NaN:NaN

Speaker: Raj gill

Type: CLS - EPF Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

Etheorem is an executable formalization of Ethereum's consensus layer in Lean 4. The same definitions run, pass the official conformance vectors at the current fork frontier, and carry machine-checked proofs. Normally the running code, the tests, and the proofs live in separate artifacts that drift apart. Here they're one set of definitions, so a proof and a passing vector describe the same spec.

Categories

Core ProtocolConsensusZKCryptography