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.







Speakers


Grigore Roșu Grigore Roșu

Founder & CEO

Runtime Verification

Martin Lundfall Martin Lundfall

Formal Verification Researcher

Ethereum Foundation

Philip Daian Philip Daian

Cornell University and Flashbots

Mariano Conti Mariano Conti

Friend of Ethereum

Mooly Sagiv Mooly Sagiv

CEO

Certora

Vlad Zamfir Vlad Zamfir

Advisor

Runtime Verification

Kurt Barry Kurt Barry

Protocol Engineer

MakerDAO

Everett Hildenbrandt Everett Hildenbrandt

CTO

Runtime Verification

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

Director of Formal Verification

Runtime Verification

Stephen Skeirik Stephen Skeirik

Formal Verification Engineer

Runtime Verification

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
company mission and vision news team careers publications presentations videos faq Embedded Systems Blockhain Advisory Services Smart Contract Verification Protocol Verification Formal Design and Modeling The IELE Virtual Machine Partnerships contact media kit blog