This repository holds the work performed under Grant ID FY24-1544 of the Ethereum Foundation (EF). The purpose of this grant is to explore the viability of using the Cryptol language and the Software Analysis Workbench (SAW) to formally verify the EF's c-kzg library against the consensus-specs Deneb specification.