drat
Check DRAT/DRUP proofs of unsatisfiability inside your Python process. Zero dependencies, optional Rust accelerator.
A readable, self-checking CDCL SAT solver, preprocessor and encoding library. Every answer comes with a certificate.