Verified SAT Redundancy Checking in SPARK

Boolean satisfiability (SAT) asks to decide whether a formula can be evaluated to true. In certified SAT solving, one additionally asks to provide a certificate or verifiable proof to ensure correctness of the solver's output. A crucial component in this process are fast verified, proof checkers. However, constructing efficient, formally verified checkers remains challenging. In this paper, we study whether the Ada/SPARK programming language can enable reliable, efficient, verifiable proof checkers. SPARK 2014, with its design-by-contract capabilities, allows to express core concepts of propositional logic and modern redundancy criteria with functional correctness. We introduce a methodology for implementing SAT specifications in SPARK, accompanied by formal proofs with a focus on Resolution Asymmetric Tautologies (RAT). While a complete verified proof checker is not yet realized, our work establishes the foundational framework necessary for its future development, and demonstrates that strong correctness guarantees can be realized in SPARK.