Survey

• Proofs for Satisfiability Problems
• Generating and Exploiting Automated Reasoning Proof Certificates
• PROOFS FOR SMT

Projects

• SMTCoq

Verifiers

• SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
• CARCARA: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format
• A Resolution-Based Interactive Proof System for UNSAT

Proof Formats

• RESOLUTE
• LFSC CVC5
• DRAT-based Bit-Vector Proofs in CVC4
• The Alethe Proof Format

Work Based on Proof Checking

• ZKSMT: A VM for Proving SMT Theorems in Zero Knowledge