# Efficient Certified Resolution Proof Checking

arXiv: https://arxiv.org/abs/1610.06984 · HTML: https://mlsanity.com/paper/1610.06984/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Oct 2016.

## Built on by (most cited first, 5 of 5)

- [Logic-Based Explainability in Machine Learning](https://mlsanity.com/paper/2211.00541/) (2022)
- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)
- [Certified MaxSAT Preprocessing](https://mlsanity.com/paper/2404.17316/) (2024)
- [Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability](https://mlsanity.com/paper/2501.17493/) (2025)
- [Streaming LRAT Certificates into Lean Theorems](https://mlsanity.com/paper/2607.00815/) (2026)

## Abstract (arXiv)

We present a novel propositional proof tracing format that eliminates complex processing, thus enabling efficient (formal) proof checking. The benefits of this format are demonstrated by implementing a proof checker in C, which outperforms a state-of-the-art checker by two orders of magnitude. We then formalize the theory underlying propositional proof checking in Coq, and extract a correct-by-construction proof checker for our format from the formalization. An empirical evaluation using 280 unsatisfiable instances from the 2015 and 2016 SAT competitions shows that this certified checker usually performs comparably to a state-of-the-art non-certified proof checker. Using this format, we formally verify the recent 200 TB proof of the Boolean Pythagorean Triples conjecture.