Basic Concepts

• Wiki

Proof Checker

• drat-trim
• GRAT Certified

Solver

• Z3
• CVC4
• Vampire

Verified/Certified Solver

VeriT

• Can be used with external checkers, e.g. SMTCoq

versat: A Verified Modern SAT Solver

• No code, not usable
• Dependent Type; Guru-lang

Papers

SMT Solver Funzzing

• Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing

Formal(ly Verified) SAT/SMT Solver

• A Reflexive Formalization of a SAT Solver in Coq
• Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL

Proof Checking

• Rocket-Fast Proof Checking for SMT Solvers
• Fast and flexible proof checking for SMT

Also see the related articles.

Other Resources

• SMT-LIB
• Practical SAT Solving A course