Proof format: Alethe

Using the flag proof-format-mode=alethe, cvc5 outputs proofs in the Alethe proof format.

The Alethe proof format is a flexible proof format for SMT solvers based on SMT-LIB. It includes both coarse- and fine-grained steps and was first implemented in the veriT solver []. Alethe proofs can be checked via reconstruction within Isabelle/HOL [] as well as within Coq, the latter via the SMTCoq plugin []. There is also a high performance Rust proof checker and elaborator for Alethe: Carcara, available here. For a quick start, the cvc5 repository contains a script to download and install the Carcara checker’s version with full support for cvc5 Alethe proofs, and create scripts for generating proofs with cvc5 and checking them with Carcara.

Currently, the theories of equality with uninterpreted functions, linear arithmetic, bit-vectors and parts of the theory of strings (with or without quantifiers) are supported in cvc5’s Alethe proofs.

A simple example of cvc5 producing a proof in the Alethe proof format:

$ bin/cvc5 --dump-proofs --proof-format-mode=alethe ../test/regress/cli/regress0/proofs/qgu-fuzz-1-bool-sat.smt2
(error "Fatal error in option parsing: expert option proof-format-mode cannot be set in safe mode.")