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

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

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

Also see the related articles.

- SMT-LIB
- Practical SAT Solving A course