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.

Classroom A

Thanh-Hai Tran is an independent researcher. Before that, he was a senior researcher in the Dependable Distributed System team at Consensys. His interests are formal methods, distributed systems, cryptography, and blockchains. He has experience in designing blockchain protocols, applying formal verification techniques in multiple projects, e.g., the Distributed Validator Technology (DVT), the 3-Slot-Finality (3SF) protocol, and the C-KZG library, and developing analysis tools, e.g., APALACHE.