[creata]

Don't SMT solvers output proof objects so that the results can be easily independently verified?

[syrak]

Even if you had a verified SMT checker, you also need to prove that the encoding of the problem in SMT is correct, i.e., that a proof does translate to a valid register allocation solution, to achieve comparable guarantees to CompCert.