Formal verification proves code correctness. In other words, formal verification aims to check if the code behaves as expected.

This short definition can lead to questions such as: how a blockchain project can apply formal verification, what does it mean to prove the code, how bulletproof is it? Or, what are the tools and techniques available at the moment, and how can they be applied to ensure a safer environment?

Formal Verification in the Ethereum Ecosystem is the first event in the industry that aims to answer the most common questions developers and users have and, most importantly, educate and deconstruct some of the misinformation in the space.

Get ready for a full day of sessions covering the essential aspects of formal verification, different languages, tools, approaches, and methods applied by key players in the ecosystem.

ETH RTD badge



Speakers

Grigore Roșu

Grigore Roșu

Founder & CEO

Martin Lundfall

Martin Lundfall

Formal Verification Researcher

Ethereum Foundation

Philip Daian

Philip Daian

Security Advisor

Mariano Conti

Mariano Conti

Friend of Ethereum

Mooly Sagiv

Mooly Sagiv

CEO

Certora

Vlad Zamfir

Vlad Zamfir

Ethereal Advisor

Kurt Barry

Kurt Barry

Protocol Engineer

MakerDAO

Everett Hildenbrandt

Everett Hildenbrandt

CTO

Leo Alt

Leo Alt

Formal Verification Lead

Ethereum Foundation

Tannr Allard

Tannr Allard

Protocol Engineer

MakerDAO

Dan Guido

Dan Guido

CEO

Trail of Bits

Joran Honig

Joran Honig

Security Engineer

Consensys Diligence

Jan Gorzny

Jan Gorzny

Blockchain Researcher

Quantstamp

Yu Feng

Yu Feng

Assistant Professor

UC Santa Barbara

Daejun Park

Daejun Park

Research Collaborator

Stephen Skeirik

Stephen Skeirik

Formal Verification Engineer

Agenda


12:30PM - 12:40PM ET
Welcome!

Silvia Barredo - Runtime Verification


12:40PM - 1:00PM ET
So...What's Formal Verification

Grigore Roșu - Runtime Verification


1:00PM - 1:45PM ET
Formally Verifying Ethereum Smart Contracts by Overwhelming Horn Solvers

Leo Alt - Ethereum Foundation


1:45PM - 2:30PM ET
Automatic basic-block summarization of Ethereum bytecode using KEVM

Everett Hildenbrandt - Runtime Verification


2:30PM - 3:15PM ET
Formal Verification at MakerDAO: Past, Present, and Future

Kurt Barry & Tannr Allard - MakerDAO


3:15PM - 4:15PM ET
Panel discussion. Available tools and automatization when conducting formal verification

Martin Lundfall - Ethereum Foundation, Mooly Sagiv - Certora, Yu Feng - UC Santa Barbara & Joran Honig - Consensys Diligence. Moderator: Everett Hildenbdrant - Runtime Verification


4:15PM - 5:15PM ET
Panel discussion. The current state of Formal Verification: methods, resources, opportunities and limitations.

Philip Daian - Cornell University and Flashbots, Vlad Zamfir - Advisor RV, Dan Guido - Trail of Bits & Jan Gorzny - Quantstamp. Moderator: Mariano Conti


5:15PM - 6:00PM ET
Symbolic Execution for MEV

Philip Daian - Cornell University and Flashbots


6:00PM - 7:00PM ET
Formal models of constant product market makers

Stephen Skeirik - Runtime Verification