cat _posts/2026-09-03-dratify-v0-1-3-tests-behind-the-differential-claim-and-untrusted-input-that-can-no-longer-ask-for-gigabytes.md
dratify v0.1.3: tests behind the differential claim, and untrusted input that can no longer ask for gigabytes
dratify is tagged
v0.1.3: the docs said the
Python checker and the Rust checker were compared against DRATChecker on
acceptances and rejections, but the only two tests that did so had silently
skipped on every run — an import-time guard — so that claim had never once been
exercised. The new differential suite
(2889df3) sweeps 150 random
instances plus hand-written accept/reject cases, and CI installs the native
checker and fails if the tests skip. The same release hardens the
untrusted-input paths: header counts like p cnf 99999999999 0 that would have
asked for hundreds of gigabytes are rejected outright, register_native
validates the checker it is handed instead of unpacking a fixed tuple, and
proof parsing reports the offending line and token. Tests go from 87 to 96 and
coverage 84% to 87%, with each new guard confirmed to fail when its fix is
reverted.