proof-checking
Check DRAT/DRUP proofs of unsatisfiability inside your Python process. Zero dependencies, optional Rust accelerator.
A readable, self-checking CDCL SAT solver, preprocessor and encoding library. Every answer comes with a certificate.
A reproducible audit harness for mathematical LaTeX papers: deterministic scanner, schema-validated issue ledgers with mechanical quote verification, and a stage-gated final gate — driven by any MCP agent or the CLI.
Replayable Python protocol engine for checking time-bound future claims from canonical artifacts, with typed outcomes and audit trails.
