> In CompCert's case though, the register allocation verifier itself is verified.
I don't think so, I think moonchild's account of it is accurate. At least, it was accurate in 2012. From a 2012 blog post: [0]
> In CompCert, this algorithm is not proven correct. Instead, after generating the graph, the compiler calls an OCaml implementation of IRC and then checks that the coloring is valid. If the checker confirms that the coloring is valid, the compiler uses it and proceeds along. If it does not confirm that it's valid, compilation is aborted. This checker is proven correct, and because it is simpler, its proof of correctness is easier.