The soundness of Satisfiability Modulo Theories (SMT) solvers is critical in many applications. One way to ensure soundness is to have solvers generate proofs that can be independently verified. Unfortunately, generating proofs can have a significant overhead. We propose a new proof format (eDRAT) that extends the well-known DRAT format from SAT to SMT. eDRAT proofs can be generated with little overhead and can be verified by combining existing tools for propositional reasoning with specialized theory checkers. We instrument the CVC5 solver to generate eDRAT proofs and we develop checkers for two SMT theories. Our checkers include an untrusted elaborator written in Rust and a formally verified component written in Lean that validates results from the elaborator. Empirical evaluation shows that eDRAT has a much lower proof generation overhead than other formats supported by CVC5, and it has comparable or better proof checking times.
Research areas
