# Efficient Certified RAT Verification

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

## Key facts

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

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

- [Leveraging the Context through Multi-Round Interactions for Jailbreaking Attacks](https://mlsanity.com/paper/2402.09177/) (2024)
- [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)
- [PICID: Proof-Driven Clause Learning in Neural Network Verification](https://mlsanity.com/paper/2503.12083/) (2025)
- [Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability](https://mlsanity.com/paper/2501.17493/) (2025)
- [Proof Generation in CDSAT](https://mlsanity.com/paper/2107.02351/) (2021)
- [How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization](https://mlsanity.com/paper/2411.07955/) (2024)
- [Pseudo-Boolean Proof Logging for Optimal Classical Planning](https://mlsanity.com/paper/2504.18443/) (2025)
- [Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables](https://mlsanity.com/paper/2511.16637/) (2025)
- [Streaming LRAT Certificates into Lean Theorems](https://mlsanity.com/paper/2607.00815/) (2026)
- [Formally Verified Synthesizable Floating-Point Data Types in ARCH HDL](https://mlsanity.com/paper/2607.23715/) (2026)
- [LeanCSP: A Framework for Certifying Constraint Reformulation and Solving in Lean](https://mlsanity.com/paper/2607.28459/) (2026)
- [Dependable AI-Assisted Engineering: A Formal Framework for AI Participation and Assurance in Safety-Critical Workflows](https://mlsanity.com/paper/2610.04084/) (2026)

## Abstract (arXiv)

Clausal proofs have become a popular approach to validate the results of SAT solvers. However, validating clausal proofs in the most widely supported format (DRAT) is expensive even in highly optimized implementations. We present a new format, called LRAT, which extends the DRAT format with hints that facilitate a simple and fast validation algorithm. Checking validity of LRAT proofs can be implemented using trusted systems such as the languages supported by theorem provers. We demonstrate this by implementing two certified LRAT checkers, one in Coq and one in ACL2.