Devcon Archive logo
Devcon Forum Blog
  • Watch
  • Event
    Event: background logo
    • Devcon 7
    • Devcon 6
    • Devcon 5
    • Devcon 4
    • Devcon 3
    • Devcon 2
    • Devcon 1
    • Devcon 0
  • 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
  • Forum
  • Blog

Get in touch

devcon@ethereum.org

Subscribe to our newsletter

Crafted with passion ❤️ at the Ethereum Foundation

© 2025 — Ethereum Foundation. All Rights Reserved.

devcon 7 / how model checking can help build trust in the design of distributed protocols like single slot finality

  • YouTube
  • Details

How model checking can help build trust in the design of distributed protocols like Single Slot Finality

Duration: 00:06:19

Speaker: Igor Konnov, Thanh-Hai Tran

Type: Lightning Talk

Expertise: Intermediate

Event: Devcon

Date: Nov 2024

Ethereum is a lively place for developing distributed protocols. Getting a distributed protocol right is a notoriously difficult task. When it comes to developing the Ethereum CL, the community follows two pragmatic approaches: Writing pen & paper proofs and writing executable specs in Python. We show how model checking can confirm our intuition about the behavior of consensus protocols or disprove it. We do so by applying our method to one of the recently proposed Single Slot Finality protocols

Categories

ConsensusProtocol DesignFormal VerificationapalacheConsensusFormal VerificationProtocol Design
  • Related
Keynote: [title redacted] preview
Devcon
Talk
26:22

Keynote: [title redacted]

[description redacted]

VLSMs—analyzing faulty distributed systems preview
Devcon
Talk
29:47

VLSMs—analyzing faulty distributed systems

Validating Labeled State transition and Message production systems (VLSMs) provide a general approach to modeling and verifying faulty distributed systems. With formal definitions of validation and equivocation, we are able to prove that for systems of validators, the impact of Byzantine components is indistinguishable from the effect of the introduction of corresponding equivocating components. All of the results presented in this talk have been formalized and checked in the Coq proof assistant

Ethereum in 25 Minutes, Version MMXVII preview
Devcon
Talk
24:53

Ethereum in 25 Minutes, Version MMXVII

So what are all of the different moving parts of the Ethereum blockchain? What are uncles, how do contracts call other contracts, who runs them? What is the role of proof of work and proof of stake, and what exactly is gas? What will EIP86 do for you? Vitalik Buterin provides a 25-minute technical overview of the ethereum blockchain, start to finish, and explain many of these concepts in detail.

Exploring the Future of Account Abstraction preview
Devcon
Talk
26:47

Exploring the Future of Account Abstraction

Discover the journey of Ethereum's Account Abstraction (AA) from inception to its current state, challenges tackled by ERC-4337, and future roadmap: modular native AA approach for L2 and L1, and EOA improvement (EIP-7702).

Native Account Abstraction in Pectra, rollups and beyond: combining EOF, EIP-7702 and RIP-7560 preview
Devcon
Talk
25:21

Native Account Abstraction in Pectra, rollups and beyond: combining EOF, EIP-7702 and RIP-7560

Account Abstraction has rightfully become one of the most discussed topics in the Ethereum ecosystem. The upcoming Pectra upgrade is set to be the first one to improve EOAs by including EIP-7702. But can EIP-7702 alone achieve "Account Abstraction"? We will discuss the challenges and benefits of EIP-7702, and break down the team's vision for achieving "complete" Native Account Abstraction with RIP-7560/EIP-7701 and how it differs from ERC-4337 + EIP-7702.

BRAID: Implementing Multiple Concurrent Proposers preview
Devcon
Lightning Talk
08:59

BRAID: Implementing Multiple Concurrent Proposers

BRAID is a consensus specification for implementing concurrent leaders in ethereum from parallel chains. The talk will cover the design of braid. Technical challenges of alternative designs for multi proposer and, if time permits, other topics of interest in execution consensus seperation.

Fork-Choice enforced Inclusion Lists (FOCIL) preview
Devcon
Talk
25:35

Fork-Choice enforced Inclusion Lists (FOCIL)

A direct consequence of centralized block production is a deterioration of Ethereum's censorship resistance properties. In this talk, we introduce FOCIL, a simple committee-based design improving upon previous inclusion list and co-created block mechanisms. We present the benefits of (1) relying on a committee to address issues related to bribing/extortion attacks, and (2) having attesters enforce the IL as part of the block validity condition to prevent IL equivocation.

Ethereum for Dummies preview
Devcon
Talk
23:52

Ethereum for Dummies

Ethereum's CTO Dr. Gavin Wood presents "Ethereum for Dummies" or "So, now we've built it, WTF is it?"

Understanding the Ethereum Blockchain Protocol preview
Devcon
Talk
38:18

Understanding the Ethereum Blockchain Protocol

Ethereum's Vitalik Buterin presents on the intricacies of the Ethereum Blockchain Protocol.

Can we formally verify implementations of cryptographic libraries like the c-kzg library? preview
Devcon
Lightning Talk

Can we formally verify implementations of cryptographic libraries like the c-kzg library?

In this talk, we present our work on formally verifying the implementation of a cryptographic library key to the security of the Ethereum Data Availability layer: the c-kzg library. We will explore what we have been able to prove so far and what is ahead of us.