A proof system for graph (non)-isomorphism verification

In order to be able to apply graph canonical labelling and isomorphism checking within interactive theorem provers, either these checking algorithms must be mechanically verified, or their results must be verifiable by independent checkers. We analyze a state-of-the-art graph canonical labelling algorithm (described by McKay and Piperno) and formulate it in a form of a formal proof system. We provide an implementation that can export a proof that the obtained graph is the canonical form of a given graph. Such proofs are then verified by our independent checker, and can be used to certify that two given graphs are non-isomorphic.