Can we formally verify implementations of cryptographic libraries like the c-kzg library?
Duration: NaN:NaN:NaN
Speaker: Thanh-Hai Tran
Type: Lightning Talk
Expertise: Intermediate
Event: Devcon
Date: Nov 2024
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.