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 consensus spec formalization and proving in lean4

  • YouTube
Etheorem: Consensus Spec Formalization and Proving in Lean4 preview
  • Details

Etheorem: Consensus Spec Formalization and Proving in Lean4

Duration: NaN:NaN:NaN

Speaker: Ivan Anishchuk

Type: CLS - EPF Talk

Expertise: Some familiarity with the topic

Event: Devcon

Date: Nov 2026

A novel approach to the spec, a single artifact that can we run, test, and prove. Contributions included completeness theorem for merkle branch check widely used in consensus (deposits, lightclient sync, and PeerDAS sampling), protocol arithmetic and invariants proofs, and various spec model improvements (including modeling Heze fork with FOCIL).

Categories

ConsensusFormal Verification