SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal

We present progress towards the formal verification of Wigderson’s graph coloring algorithm in Coq. We have created a library of formalized graph theory that aims to bridge the literature gap between introductory material on Coq and large-scale formal developments, while providing a motivating case study. Our library contains over 180 proven theorems. The development is at https://github.com/siraben/coq-wigderson.