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.