What is veriT?

veriT is a SMT (Satisfiability Modulo Theories) solver. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.

The input format is the SMT-LIB language (both versions 1.2 and 2.0) and DIMACS, but veriT can also be used as a standalone library and incorporated in third-party software. The tool is open-source and distributed under the BSD license.

veriT is complete for the logic of unquantified formulas over uninterpreted symbols, difference logic over integers and real numbers, and the combination thereof. This corresponds to the logics identified as QF_IDL, QF_RDL, QF_UF and QF_UFIDL in the SMT-LIB benchmarks. veriT includes quantifier reasoning capabilities through quantifier instantiation heuristics and the integration of a first-order prover and linear arithmetics for integers and real numbers.

veriT has proof-production capabilities that may be used or checked by external tools. Although not (yet) as fast as the solvers performing best in the SMT competition, veriT has a decent efficiency.

The ancestor of veriT is haRVey. Its web page can still be reached here.

How to contribute?

veriT is under heavy development, and newcomers to the project are most welcome! Check the Job section of this site, and contact us.