carlok — zsh — 88×30

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.