veriT's big logo
An open, trustable and efficient SMT-prover

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 linear arithmetic on real numbers and integers. It also offers good support for quantifiers. The input format is the SMT-LIB 2.0 language and DIMACS, but veriT is intend also to be used as a standalone library and incorporated in third-party software.

veriT is open-source and distributed under the BSD license.

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 project is under heavy development, and newcomers are most welcome! Just contact us.


Here you can find published papers about veriT.

Papers 2016

  • Haniel Barbosa. Efficient Instantiation Techniques in SMT (Work in Progress). 5th Workshop on Practical Aspects of Automated Reasoning co-located with IJCAR 2016, (PAAR), 2016.
    [ pdf | bibtex]

Papers 2015

  • Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine. Adapting Real Quantifier Elimination Methods for Conflict Set Computation. FroCoS 2015.
    [ pdf | bibtex]
  • Richard Bonichon, David Déharbe, Pablo Dobal, Cláudia Tavares. SMTpp : preprocessors and analyzers for SMT-LIB. 13th International Workshop on Satisfiability Modulo Theories, (SMT), 2015.
    [ pdf | bibtex]
  • Haniel Barbosa, Pascal Fontaine. Congruence Closure with Free Variables (Work in Progress). 2nd International Workshop on Quantification, (QUANTIFY), 2015.
    [ pdf | bibtex]

Papers 2014

  • Richard Bonichon, David Déharbe, Cláudia Tavares. Extending SMT-LIB v2 with λ-Terms and Polymorphism. Proceedings of the 12th International Workshop on Satisfiability Modulo Theories, (SMT). CEUR Workshop Proceedings, vol. 1163, p. 53-62, 2014.
    [ pdf | bibtex | online ]
  • David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. Integrating SMT solvers in Rodin. Science of Computer Programming, 2014. DOI: 10.1016/j.scico.2014.04.012.
    [ pdf | bibtex ]

Papers 2013

  • David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure. Computing prime implicants. 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), p.46-52. Portland, USA. October, 2013.
    [ pdf | bibtex ]
  • Carlos Areces, David Déharbe, Pascal Fontaine, Ezequiel Orbe. SyMT: finding symmetries in SMT formulas. (Extended Abstract: Work in progress). 11th International Workshop on Satisfiability Modulo Theories (SMT). Helsinki, Finland. July, 2013.
    [ pdf | bibtex ]
  • David Déharbe. Integration of SMT-solvers in B and Event-B development environments. Science of Computer Programming. Vol. 78, nº 3. p. 310-316. Abstract State Machines, Alloy, B and Z - Selected Papers from ABZ 2010. Edited by Marc Frappier, Uwe Glässer, Sarfraz Khurshid, Régine Laleau and Steve Reeves. DOI: 10.1016/j.scico.2011.03.007.
    [ pdf | bibtex ]
  • David Déharbe, Pablo Federico Dobal, Pascal Fontaine. Le solveur SMT veriT. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). Tool demonstration, 2013.
    [ pdf | bibtex ]

Papers 2012

  • Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. Combining decision procedures by (model-) equality propagation. Science of Computer Programming, Vol. 77, p. 518-532, 2012. DOI: 10.1016/j.scico.2010.04.003.
    [ pdf | bibtex ]
  • David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin. SMT solvers for Rodin. In John Derrick, John A. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves and Elvinia Riccobene, editors, In Proc. ABZ, volume 7316 of LNCS, pages 194-207, Springer, 2012.
    [ pdf | bibtex ]

Papers 2011

  • David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo. Quantifier Inference Rules for SMT proofs. Workshop on Proof eXchange for Theorem Proving (PxTP), 2011.
    [ pdf | bibtex ]
  • David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. Exploiting symmetry in SMT problems. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors. In Proc. Conference on Automated Deduction (CADE), volume 6803 of LNCS. pages 222--236, Springer-Verlag, 2011.
    [ pdf | bibtex ] [ pdf (long version) | bibtex ]

Papers 2010

  • Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo. Exploring and Exploiting Algebraic and Graphical Properties of Resolution. In Aarti Gupta and Daniel Kroening editors In Proc. Workshop on Satisfiability Modulo Theories (SMT), 2010.
    [ pdf | bibtex ]
  • Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. GridTPT: a distributed platform for Theorem Prover Testing. In Boris Konev, Renate Schmidt and Stephan Schulz, editors. In Proc. Workshop on Practical Aspects of Automated Reasoning 2010.
    [ pdf | bibtex ]
  • Alessandro Cavalcante Gurgel, Valério Gutemberg de Medeiros, Marcel Oliveira, David Déharbe. Integrating SMT-Solvers in Z and B Tools. Abstract State Machines, Alloy, B and Z (ABZ 2010). Lecture Notes in Computer Science, Vol 5977/2010, p. 412-413, 2010. DOI: 10.1007/978-3-642-11811-1_45.
    [ bibtex ]

Papers 2009

  • Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. veriT: an open, trustable and efficient SMT-solver. In Renate A. Schmidt, editor. In Proc. Conference on Automated Deduction (CADE), volume 5663 of LNCS, pages 151--156. Springer-Verlag, 2009.
    [ pdf | bibtex ]
  • Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine. Combining decision procedures by (model-)equality propagation. In P. Machado, A. Andrade and A. Duran, editors, In Proc. of the Brazilian Symposium on Formal Methods (SBMF), Salvador, Bahia, Brazil, 2008. volume 240 of Electr. Notes Theor. Comput. Sci., pages 113-128, 2009.
    [ pdf | bibtex ]

Our tools

Several tools are used to support the development of veriT. This section collects our tools that are sufficiently stable for distribution, as well as tools developed by the SMT community and updated for our needs.

Delta SMT

DeltaSMT is a debugging tool developed by Robert Brummayer and Armin Biere at the Institute for Formal Models and Verification at Linz University.

The tool was updated for SMT-LIB 2.0. Please note that this version of the tool does not support the full syntax but only the features supported by the original tool. E.g. there is no support for quantifiers, or push and pop.

Alternatively, the beta version of another (new) delta debugger developed by Aina Niemetz at the Institute for Formal Models and Verification at Linz University and supporting SMT-LIB syntax version 2.0 is available here.


The GridTPT platform has been used to support the development of the SMT solver veriT for several years. Since programming provers is a complex task, a good testing platform can contribute in detecting bugs early and helping development. GridTPT's features are fairly standard, but it allows to easily distribute the task in a cluster for extensive tests to be completed quickly.

GridTPT is neither stable nor easy to use, but if you are looking for a testing platform for your prover or solver, contact us and we will help you to install, configure and use the solver. This will also help us to improve the tool and hopefully eventually distribute a adaptable tool to the community. The code is BSD and written mostly in Python.


SMTpp is a tool operating both as a source-to-source transformer and analyzer for SMT-LIB. Our goal is to offer a platform to develop:

  • analyses of SMT-LIB problems (unused variables, typechecking, logic detection)
  • simplifications and transformations of SMT-LIB problems (term normalization, constant propagation) as pre- or post-processing steps.

SMTpp has grown out of veriT and is available under the ISC license. Check out our GitHub page for more detailed information.

SAT solver within Matlab and Octave

Interface between the veriT SAT solver and either Matlab or Octave. The SAT problem can be modeled using Matlab matrices. The current implementation allows to either use dense or sparse matrices. It has already been used successfully under Windows 7 64 bits and Ubuntu 13.10 64 bits. It is intended to be used by industrial as well as academic communities. The code is released under the BSD license.

Different packages for different operating systems and architectures are available:

  • package for Windows 7 64 bits with Matlab
  • package for Windows 7 32 bits with Matlab
  • package for Linux 64 bits with Matlab
  • package for Linux 64 bits with Octave

External software

veriT relies on third-party software using them either as libraries or as stand-alone applications. veriT is also used or integrated with other software.

GNU MP (is used by veriT)

The GNU Multiple Precision Arithmetic Library is used to represent and manipulate numerical value. It is distributed under the GNU LGPL.

Rodin (integrates veriT)

Rodin is an Eclipse-based development environment for Event-B. The SMT plug-in for Rodin allows to use SMT-solvers to discharge proof obligations. It is still under development.

REDUCE (can be used by veriT)

REDUCE is a computer algebra system often used as an algebraic calculator for problems that are possible to do by hand. Some versions of veriT use Reduce.

E (was used by veriT)

The E equational theorem prover is a first-order logic theorem prover based on the superposition calculus. It was used by veriT as a standalone application. It is released under the GNU GPL.

CRefine (was used by veriT)

CRefine is an editor that supports the formal development of concurrent object-oriented software in Circus by implementing a refinement calculus.

Bliss (was used by veriT)

Bliss is a backtracking algorithm for computing automorphism groups and canonical forms of graphs, based on individualization and refinement.

Saucy (was used by veriT)

Saucy is the implementation of a symmetry-discovery algorithm.

PermLib (was used by veriT)

PermLib is a C++ library for permutation computations.

MiniSat (was used by veriT)

In early releases, veriT used the SAT-solver MiniSat to represent and manipulate the boolean structure of the formulas.

Our Team

veriT is current under development by its creators David Déharbe and Pascal Fontaine and other researchers.

David Deharbe's photo

David Déharbe

Lead developer
Associate professor at UFRN/Brazil (team ForAll).

Pascal Fontaine's photo

Pascal Fontaine

Lead developer
Associate professor at University of Lorraine/France (team VeriDis).

Haniel Barbosa's photo

Haniel Barbosa

PhD student at University of Lorraine/France (team VeriDis).

Past developers have helped a lot:

  • Pablo Federico Dobal developed the SMTpp tool and contributed to the testing infrastructure and the arithmetic reasoning module.
  • Richard Bonichon and Cláudia Tavares developed the SMTpp tool.
  • Diego Caminha Barbosa de Oliveira developed the arithmetic reasoning module and contributed to the combination framework in the theory reasoning engine.
  • Thomas Bouton contributed to the QA infrastructure and the integration of the SAT solver with the theory reasoning engine.

In case you want to participate in the development of a SMT-solver, you may want to join the team of developers of veriT.

If you are interested in a post-doctoral position to work on the development and applications of veriT, either at LORIA (Nancy, France) or UFRN (Natal, Brazil), please contact us in advance so that we can obtain funding for your stay.

Contact Us

For questions, comments, feature requests and bug reports, please .

While reporting bugs, please make sure you give enough information in your report to enable us to reproduce and fix the problem:

  • Tell us the version of veriT you are using (including the operating system)
  • Try to send us a minimal example that causes the problem

Thanks for helping us improving veriT.