Trust What You Prove: Proof Verification in the mrs Ecosystem

Abstract

Automated theorem provers competing in CASC produce proof objects, but those objects are often checkedonly for syntax and graph structure. The standard approach, delegating proof checking to external toolslike GDV or per-step ATP calls, requires external ATP binaries, leaves some inference rules unchecked, andin practice is not always run. This paper describes two components of the mrs ecosystem that address theremaining trust gap. mrs is a Rust CASC entrant using a worker-bounded portfolio of 15 active searchconfigurations, with category-tuned schedules derived from greedy set-cover experiments. mrs-proover is astandalone TSTP refutation verifier that competed in ProoVer 2026. In the official CASC-J13 competitionrun, the submitted mrs-proover v0.2.0 build scored 47/138 in the PRV division. A separate post-competitionlocal reproduction recorded at commit bcc9918 (v0.2.3, 30 seconds per proof, 8 workers) scored 148/150 onthe committed 100-proof corpus. At the core of mrs-proover’s strict path is mrs-proof-kernel, a small cratethat recomputes resolution, factoring, superposition, demodulation, and Skolemization from their definitions,with no external ATP calls. Competition mode combines dedicated structural checks and propositional fastpaths with an ATP ladder; strict mode uses only the independent kernel. The kernel checks explicit AVATARcertificates and can replay bounded FRAT/LRAT traces. Resource exhaustion is inconclusive and is nevertreated as positive proof evidence. We describe the architecture, adversarial testing methodology, and theoptional, fail-closed integration of strict checking into mrs’s own proof-output path.