Abstract

Applied combinatorial optimization has witnessed a revolution in performance since the turn of the millennium, but the complexity of modern solvers is making bugs into an ever more serious concern. The most promising remedy is to make solvers certifying, so that they use proof logging to generate machine-verifiable proofs of correctness. We present the first example of certified graph colouring in the state-of-the-art solver ZykovColor using VeriPB proofs. Combined with the formally verified CakePB backend, this provides end-to-end certified graph colouring. An experimental evaluation shows excellent results with only moderate overhead for proof logging and checking.