SMTCoq is a Coq plugin that checks proof witnesses coming from external SAT and SMT solvers. It provides:

• a certified checker for proof witnesses coming from the SAT solver ZChaff and the SMT solvers veriT and CVC4. This checker increases the confidence in these tools by checking their answers a posteriori and allows to import new theroems proved by these solvers in Coq;
• decision procedures through new tactics that discharge some Coq goals to ZChaff, veriT, CVC4, and their combination.
• abducts for goals that external solvers fail to prove, which represent possibly missing hypotheses that would allow them to prove the goal, using the cvc5 SMT solver.

SMTCoq is freely available as an opam package and on GitHub. See the INSTALL.md file for instructions on how to install SMTCoq and the supported provers.

See the examples to see how to use SMTCoq. More details are given in the USE.md file.

SMTCoq is distributed under the CeCILL-C license.

Here is a very small example of the possibilities of SMTCoq: automatic proofs in group theory.

Require Import SMTCoq.SMTCoq ZArith.

Local Open Scope Z_scope.

Section group.
  Variable e : Z.
  Variable inv : Z -> Z.
  Variable op : Z -> Z -> Z.

  Hypothesis associative :
    forall a b c, op a (op b c) =? op (op a b) c.
  Hypothesis identity : forall a, (op e a =? a).
  Hypothesis inverse : forall a, (op (inv a) a =? e).

  Add_lemmas associative identity inverse.

  Lemma inverse' :
    forall a : Z, (op a (inv a) =? e).
  Proof. smt. Qed.

  Lemma identity' :
    forall a : Z, (op a e =? a).
  Proof. smt inverse'. Qed.

  Lemma unique_identity e':
    (forall z, op e' z =? z) -> e' =? e.
  Proof. intros pe'; smt pe'. Qed.

  Clear_lemmas.
End group.

SMTCoq is an ambitious, collaborative project: everyone is welcome! There are many and varied enhancement to do: join the SMTCoq forum to discuss!

• Clark Barrett (Stanford University)
• Valentin Blot (Inria)
• Amina Bousalem (Université Paris-Sud)
• Louise Dubois de Prisque (Inria)
• Burak Ekici (The University of Iowa)
• Quentin Garchery (Université Paris-Sud, Inria)
• Benjamin Grégoire (Inria Sophia Antipolis)
• Guy Katz (Stanford University)
• Chantal Keller (Université Paris-Sud)
• Alain Mebsout (OcamlPro)
• Andrew Reynolds (The University of Iowa)
• Laurent Théry (Inria Sophia Antipolis)
• Cesare Tinelli (The University of Iowa)
• Pierre Vial (Formal Land)

• Mikaël Armand (Inria Sophia Antipolis)
• Germain Faure (Inria Saclay)
• Tianyi Liang (The University of Iowa)
• Benjamin Werner (École polytechnique)

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Armand, Michaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Thery, Laurent; Werner, Benjamin, CPP - Certified Programs and Proofs - First International Conference - 2011.

1. SMTCoq: A plug-in for integrating SMT solvers into Coq (Tool Paper), Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark, CAV - International Conference on Computer Aided Verification - 2017.
2. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), Ekici, Burak; Katz, Guy; Keller, Chantal; Mebsout, Alain; Reynolds, Andrew; Tinelli, Cesare, HaTT - on Hammers for Type Theories - First International Workshop - 2016.
3. Verifying SAT and SMT in Coq for a fully automated decision procedure, Armand, Mickaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Wener, Benjamin, PSATTT - International Workshop on Proof-Search in Axiomatic Theories and Type Theories - 2011.
4. SMTCoq : automatisation expressive et extensible dans Coq, Blot, Valentin; Bousalem, Amina; Garchery, Quentin; Keller, Chantal, JFLA - Journées Francophones des Langages Applicatifs - 2019.

Overview of SMTCoq (February, 2019)