SAT solvers are the underlying tool for all kinds of automated analysis. One notable for those thst follow my submissions is SPARK language that uses them to prove no vulnerabilities in your code. They can also automate select parts of manual proof to save time. Trouble is, they’re known to make mistakes.
This work verifies one quite a lot using a language (Guru) I rarely see. The extracted implementation in C is faster than a non-verified solver in some benchmarks. The related work section is excellent where they cover a lot of works with in-depth commentary.
And for kicks, here’s another one I found done differently: