satkit.py is a stdlib-only CDCL SAT solver (watched literals, VSIDS, 1UIP learning, Luby restarts) with an RUP proof log and a separately written RUP checker. It was shipped with no test suite. This directory is that suite, plus the two real defects it found and the fix.

Files

file	role
`satkit.py`	the solver + checker (two checker bugs fixed here, see below)
`verify_satkit.py`	the suite: 11 legs, exit 0 iff all pass
`show_defects.py`	reproduces both pre-fix defects against the shipped code
`README.md`	this record

Run

python3 verify_satkit.py     # 11/11 legs, ~3.4 s, exit 0
python3 show_defects.py      # both defects reproduced pre-fix, absent post-fix, exit 0

The suite never grades satkit with satkit:

SAT/UNSAT is decided by exhaustive brute force on small instances (a model is the certificate either way), and by refutation on large ones;
every proof step is re-derived by oracle_rup() inside verify_satkit.py, a textbook unit-propagation implementation that shares no code with the checker it is auditing;
models are checked by satisfies(), not by satkit.model_satisfies;
the suite itself is attacked: four sabotaged copies of satkit must each fail the leg aimed at them, or the run is red.

Defects found (measured, not inferred)

Both were in RupChecker. Both were found by differential fuzzing against the textbook oracle — 4 disagreements in the first 18 random proof sequences.

D1 — unsound: a satisfied clause reported as a conflict. _propagate() treated "len(c)-1 literals false and no unassigned literal" as a conflict, but that state also occurs when the remaining literal is true. The checker therefore accepted proofs of formulas that have models:

F = [(-3,),(-2,),(2,1,3),(-1,5,4),(-2,5,3),(-3,-4),(1,),(-2,4,5),(5,),(2,4,-3)]
brute-force model: [1,-2,-3,-4,5]           (model_satisfies -> True)
pre-fix   check_proof(5, F, [()]) -> ok=True   "all 1 steps RUP-checked"   <- wrong
shipped   check_proof(5, F, [()]) -> ok=False  "step 0 rejected: not RUP"

D2 — incomplete: nfalse[] driven negative. _undo() decremented the false-literal counter for every trail literal, including literals never visited because propagation returned early on a conflict. The counters went negative and later clauses could never reach "all false", blinding the checker. Consequence: valid 1UIP refutations were rejected.

PHP(4,3) 4 pigeons / 3 holes, solver says UNSAT with a 7-step refutation
pre-fix   accepted=False at step 1     (5 clauses at nfalse=-1 after step 0)
shipped   accepted=True  after 7 steps

Fix (two hunks, both in satkit.py): the len(c)-1 branch now continues when the last non-false literal is true, and _undo() decrements only the clause indices recorded in self.touched during propagation.

Post-fix: 6000 random proof sequences, 0 false accepts, 0 false rejects against the textbook oracle.

Legs and what each one actually measured

edge_cases           PASS   0.00s  7 degenerate cases
exhaustive_n2        PASS   0.01s  n=2: 247 formulas (152 unsat), all agreed
exhaustive_n3        PASS   0.16s  n=3: 4048 formulas (813 unsat), all agreed
random_sweep         PASS   0.58s  1200 random CNFs: 458 sat / 742 unsat, models and refutations verified
php_proofs           PASS   1.63s  PHP(3,2) 2 steps; PHP(4,3) 7; PHP(5,4) 28; PHP(6,5) 145; PHP(7,6) 765
random3sat_proofs    PASS   0.83s  6 instances n=70 ratio 4.3: 2 sat (models ok) / 4 unsat (refutations ok)
oracle_selfcheck     PASS   0.05s  535 model-falsified candidates, oracle never claimed RUP
negative_controls    PASS   0.00s  5 forged proofs all rejected
cross_process        PASS   0.13s  child emitted a 7-step proof; parent oracle + checker both accept
determinism          PASS   0.00s  identical sat/model/proof across repeat runs
mutant_control       PASS   0.00s  4/4 mutants killed
11/11 legs passed in 3.40s

exhaustive_n2/n3 enumerate every formula over all non-tautological clauses of width ≤ 2 up to 6 (resp. 4) clauses — 4295 formulas, not a sample.
negative_controls is the leg that would have caught D1: forged empty clause on a satisfiable formula, a refutation built from the negation of a known model, a truncated refutation, a genuine refutation transplanted onto a weaker satisfiable formula, and a provably non-RUP step spliced into step 0.
mutant_control kills: flipped_sat (caught by exhaustive_n2), all_positive_model (random_sweep), short_proof (php_proofs), lax_checker (negative_controls). A green run means those legs have teeth.

Scope — what this does not establish

RUP only. The checker is sound and complete for RUP steps; a valid proof that needed RAT (clause addition by resolution on a pivot, used by some DRAT producers) would be rejected. satkit emits RUP steps only, so this does not affect it, but the checker is not a general DRAT checker.
Exhaustive agreement covers n ≤ 3; n ≤ 10 is sampled (1200 CNFs), and larger instances are covered only where a refutation or a model certifies the answer. There is no completeness test on satisfiable large instances beyond the models returned.
Refutation checking is a soundness certificate: a checked RUP proof ending in the empty clause proves UNSAT. A rejected proof proves nothing about the formula — only that this producer's proof was bad.
show_defects.py reconstructs the pre-fix methods by subclassing, so the "before" column is a faithful copy of the shipped pre-fix code, not a rerun of an old checkout.