GHSA-xccm-c64j-hf7g: 
Python vulnerability analysis and mitigation

Impact

dratify.check_proof exists to answer one question: is this proof of unsatisfiability genuine? Before 0.1.11, both checkers could answer yes for a formula that is satisfiable. It takes default flags and an ordinary text proof, on both the pure-Python checker and the Rust crate.

from dratify import parse_dimacs, check_proof
f = parse_dimacs("p cnf 2 2\n1 0\n-1 2 0\n")
check_proof(f, "d -1 2 0\n-2 0\n0\n").ok   # True before 0.1.11

Making variables 1 and 2 true satisfies this formula, and no step of the proof is valid. A checker that keeps the deleted clause rejects -2 0; drat-trim and rate also refuse the proof. The cause: deleting a clause removed it from the clause store and left the root assignment alone. (-1 2) was the reason 2 was true. After the deletion, 2 stayed true while nothing supported it. (-2) then passed as vacuously RAT, because no live clause contained 2. It was false at the root, which registered a conflict, and everything after a conflict passes. You are affected if you rely on ok=True from a proof you did not produce yourself: one from an untrusted party, or from a solver whose correctness is what you are checking. Not affected:

• Calls with apply_deletions=False or with check_rat=False. With either, every root literal stays entailed by the input and earlier lemmas.
• The verdict on a formula that really is unsatisfiable.
• Valid proofs: this defect only ever accepted too much. Proofs from CaDiCaL and kissat verify under the fix in every case tried. Earlier results are not all suspect, but a certificate accepted from an untrusted source by an affected version should be checked again.

Patches

Fixed in dratify 0.1.11, on PyPI and crates.io, and in cdclkit-native 0.2.1, which embeds the crate. A plain cdclkit install takes the fix by upgrading dratify. A deletion is now ignored when the clause, as a set, has exactly one literal true and all the others false at the root. Every reason clause has that shape, so every root literal keeps a live clause behind it. Ignoring a deletion is always sound, because it only leaves more clauses to satisfy. This follows drat-trim's operational reading of deletion (Rebola-Pardo and Biere, 2018), approximated by the root-unit test. A proof that relies on a reason clause being gone is now rejected or checked against more clauses. drat-trim and specified-DRAT checkers can differ on such proofs; the README describes the reading used here.

Workarounds

Upgrade. Otherwise, pass apply_deletions=False. It may reject a valid proof whose RAT steps depend on a deletion, but it fails closed. check_rat=False also closes this and rejects every RAT step.

References

• Fix: https://github.com/carlok/dratify/commit/3a53eca
• Release notes: https://github.com/carlok/dratify/blob/main/CHANGELOG.md#0111--2026-11-09