Yes. That's the reason the formal methodists started building verified or checkable tools with the checkers being tiny. Doing an solver might involve making it

Yes. That's the reason the formal methodists started building verified or checkable tools with the checkers being tiny. Doing an solver might involve making it produce a log of each step it made with a simpler system checking them. The checking is also easy to parallelize with linear scaling. My current recommendation is checkable solvers done in a parallel language like Chapel with tiny, verified checkers. Run it logless first to see if it even passes at all. Once passes, run it in logging mode to get evidence to feed to checker. Use multiple, sequential processes to check that as concurrency in checker reduces confidence.