- a
**certified**checker for proof witnesses coming from the SAT solver zChaff and the SMT solver veriT. This checker increases the confidence in these tools by checking their answers*a posteriori*; **decision procedures**through new tactics named`verit`, that calls veriT on any Coq goal, and`zchaff`, that calls zChaff on any Coq goal.

Download: To install it, please report to the installation instructions available in the archive. We provide a snapshot of the version of Coq required to compile it, and a snapshot of the version of veriT used for it.

- Produce a zChaff proof witness:
`zchaff file.cnf`. This produces a proof witness file named`resolve_trace`. - In a Coq file
`file.v`, put:

`Require Import SMTCoq.`

`Zchaff_Checker "file.cnf" "resolve_trace".` - Compile
`file.v`:`coqc file.v`. If it returns`true`then zChaff indeed proved that the problem was unsatisfiable. - You can also produce Coq theorems from zChaff proof witnesses:
the commands

`Require Import SMTCoq.`

`Zchaff_Theorem theo "file.cnf" "resolve_trace".`

will produce a Coq term`theo`whose type is the theorem stated in`file.cnf`.

- Produce a veriT proof witness:
`veriT --proof-prune --proof-merge --proof-with-sharing --cnf-definitional --disable-e --disable-ackermann --input=smtlib2 --proof=file.log file.smt2`. This produces a proof witness file named`file.log`. - In a Coq file
`file.v`, put:

`Require Import SMTCoq.`

`Section File.`

`Verit_Checker "file.smt2" "file.log".`

`End File.` - Compile
`file.v`:`coqc file.v`. If it returns`true`then veriT indeed proved that the problem was unsatisfiable. - You can also produce Coq theorems from veriT proof witnesses:
the commands

`Require Import SMTCoq.`

`Section File.`

`Verit_Theorem theo "file.smt2" "file.log".`

`End File.`

will produce a Coq term`theo`whose type is the theorem stated in`file.smt2`.

where

where

- 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. PDF, BIBTEX
- 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. PDF, BIBTEX

- Version 1.0, (to be used with this version of Coq and this version of veriT)
- Version 0.1 (this version was used for the benchmarks of this paper)

Last update: July, 2nd 2014