This was asked in the Rust Zulip as well, and is actually the original idea which this thesis evolved from (Xavier said something along the lines of "My supervi

This was asked in the Rust Zulip as well, and is actually the original idea which this thesis evolved from (Xavier said something along the lines of "My supervisor and I have talked about how cool it would be to have a solver which verifies itself"). The short answer is that it should be possible to write a Why3 driver for CreuSAT which allows it to handle basic propositional reasoning, and that one would probably need to add some theories. The a bit longer answer: Getting it to work as a backend should probably not be all that hard, and it should probably be possible to make it able to prove some things as well. Getting it to verify itself would probably be very hard. As it stands, the proof needs Alt-Ergo, CVC4 and Z3 (all of which are really good) to pass, and some of the obligations take a long time. A solver capable of verifying itself would (I imagine) have to put much more emphasis on having only simple proofs which were solvable using a minimal amount of theories, and would probably have to run for a very long time. I dunno, would be a fun project, and I guess one could decide after having tried to prove for instance Friday (the super naive solver) if it is at all worth pursuing.