Verify a manufacturing certificate bundle. Re-derives the admission verdict from the certificate's own numbers rather than reading it, and checks integrity. Returns a verdict: VERIFIED, REFUTED, VACUOUS, or UNVERIFIED. IMPORTANT: without an expected_sha256 (a fingerprint obtained OUT OF BAND, not from the bundle itself) the verdict is UNVERIFIED — the tool abstains, because internal consistency alone cannot rule out a forgery whose inputs and verdict were edited together. UNVERIFIED means 'cannot tell', NOT 'the certificate is bad'. Do not report it as either pass or fail.

Explain WHY a certificate reached its verdict, locus by locus: which loci are safe, unsafe or straddling, the margin each had, the margin it needed, and how far short it fell. Use this after verify_certificate returns REFUTED or a certificate records a REJECT — it turns an opaque refusal into a specific, actionable list. Computes nothing new; it re-presents the arithmetic the verdict already rests on.

Verify a logic-equivalence receipt. Re-runs the DRAT proof check (or re-simulates the counterexample) over the committed formula, and recomputes the hash chain. The verdict is re-derived, never read from the receipt.

Prove two small combinational circuits equivalent, or return a counterexample input. Circuits are given as gate lists over named signals. Returns a receipt any third party can re-check. Small instances only — this is a demonstration prover, not a production one.

Check a DRAT refutation against a CNF in DIMACS form. Accepts proofs from any solver. Returns whether every lemma is RUP and, on failure, the index and content of the first lemma that does not follow.

Seal an acceptance specification BEFORE measuring, so it cannot be adjusted afterward. Returns a digest that commits to the criteria without revealing them. Call this before running an experiment, not after.

Check that an acceptance specification still matches its seal. Detects criteria that were changed after sealing. Returns matched=false with the two digests if they diverge.

Score a verifier command against the certificate failure atlas. Returns detection (forgeries rejected), precision (valid artifacts accepted), and atlas_score = the minimum of the two, plus exactly which forgeries got through.

Explain a certificate defect class from the atlas taxonomy: why the forgery looks valid, and which check catches it. Call with no key to list every defect.