cat _posts/2026-08-30-dratify-check-drat-drup-proofs-of-unsatisfiability-in-process.md
dratify: check DRAT/DRUP proofs of unsatisfiability in-process
dratify is a new public DRAT/DRUP proof
checker that runs inside your Python process: zero dependencies, no subprocess,
no compiler. It replays a solver’s derived-clause log to confirm the empty
clause really follows, sharing no code with the solver that wrote the proof,
and the same checker is published as a Rust crate. A register_native() seam
lets the Rust engine (~18x faster) be supplied without shipping a toolchain,
publishing is tokenless via Trusted Publishing, and the checker’s own tests
went from 12 to 71 with a coverage gate.