For what it's worth I'm now working on a proof assistant so yeah, that's the game plan. I think the straight line case for the solver is probably OK but there's a huge range of optimisations out there and it's far too easy to introduce errors there.

At present we are a long way from proving general constraint solvers are correct, as they are built from some many little algorithms that interact in weird ways.

It's an interesting area, and I hope we'll get there in the future.

Or just prove yourself with pen and paper if the algorithm works, using structural induction and other techniques. Then it's just a matter of whether the code follows the spec