
veriT
VeriT is an open, trustable and efficient SMT (Satisfiability Modulo Theories) solver, featuring efficient decision procedure for uninterpreted symbols and linear arithmetic, and quantifier reasoning.
veriT comprises a SAT solver, a decision procedure for uninterpreted symbols based on congruence closure, a simplexbased decision procedure for linear arithmetic, and instantiationbased quantifier handling.
Pascal Fontaine (Pascal.Fontaine@inria.fr)
Haniel Barbosa (haniel.barbosa@inria.fr), Daniel El Ouraoui (daniel.elouraoui@inria.fr), Pascal Fontaine (Pascal.Fontaine@loria.fr), HansJörg Schurr (hansjorg.schurr@inria.fr)
MODEL, VERIDIS
http://www.veriTsolver.org

TLAPS
TLAPS is a platform for developing and mechanically verifying proofs about TLA+
specifications. The TLA+ proof language is hierarchical and explicit, allowing a
user to decompose the overall proof into proof steps that can be checked
independently. TLAPS consists of a proof manager that interprets the proof
language and generates a collection of proof obligations that are sent to
backend verifiers. The current backends include the tableaubased prover Zenon
for firstorder logic, Isabelle/TLA+, an encoding of TLA+ set theory as an
object logic in the logical framework Isabelle, an SMT backend designed for use
with any SMTlib compatible solver, and an interface to a decision procedure for
propositional temporal logic.

Stephan Merz (Stephan.Merz@loria.fr)
Damien Doligez (damien.doligez@inria.fr), Stephan Merz (stephan.merz@loria.fr), Martin Riener (martin.riener@inria.fr)
GALLIUM, VERIDIS
https://tla.msrinria.inria.fr/tlaps/content/Home.html

SPASS
SPASS is an automated theorem prover based on superposition that handles firstorder logic with equality and several extensions for particular classes of theories.
The classic SPASS is an automated theorem prover based on superposition that
handles firstorder logic with equality and several extensions for particular
classes of theories. With version SPASS 3.9 we have stopped the development of
the classic prover and have started the bottomup development of SPASS 4.0 that
will actually be a workbench of automated reasoning tools. Furthermore, we use
SPASS 3.9 as a test bed for the development of new calculi.Meanwhile we have released the second version of SPASSIQ, our solver for
linear integer arithmetic that we are currently extending to real and mixed realinteger
arithmetic. We didn't release SPASSSATT yet, instead we further investigated
the use of redundency elimination in SAT solving and underlying implementation techniques.
Our aim is a new approach to SAT solving that needs fewer conflicts (on average) \emph{and} is faster than the current stateofthe art solvers. Furthermore, we have developed a new calculus and first prototypical implementation of a SAT solver with mixed OR/XOR clauses.SPASS 3.9 has been used as the basis for SPASSAR, an new approximation refinement theorem
proving approach.
Christoph Weidenbach (weidenbach@mpiinf.mpg.de)

VERIDIS
http://www.spassprover.org/

Redlog
Redlog is an integral part of the interactive computer algebra system Reduce. It supplements Reduce's comprehensive collection of powerful methods from symbolic computation by supplying more than 100 functions on firstorder formulas.Redlog generally works with interpreted firstorder logic in contrast to free firstorder logic. Each firstorder formula in Redlog must exclusively contain atoms from one particular Redlogsupported theory, which corresponds to a choice of admissible functions and relations with fixed semantics. Redlogsupported theories include Nonlinear Real Arithmetic (Real Closed Fields), Presburger Arithmetic, Parametric QSAT, and many more.
Redlog is an integral part of the interactive computer algebra system Reduce. It supplements Reduce's comprehensive collection of powerful methods from symbolic computation by supplying more than 100 functions on firstorder formulas.Redlog generally works with interpreted firstorder logic in contrast to free firstorder logic. Each firstorder formula in Redlog must exclusively contain atoms from one particular Redlogsupported theory, which corresponds to a choice of admissible functions and relations with fixed semantics. Redlogsupported theories include Nonlinear Real Arithmetic (Real Closed Fields), Presburger Arithmetic, Parametric QSAT, and many more.
Thomas Sturm (sturm@redlog.eu)
Thomas Sturm (sturm@redlog.eu)
VERIDIS
http://www.redlog.eu/

Nunchaku
Nunchaku is a model finder (counterexample generator) for higherorder logic.
Nunchaku is a model finder for higherorder logic, with dedicated support for various definitional principles. It is designed to work as a backend for various proof assistants (notably Isabelle/HOL and Coq) and to use stateoftheart model finders and other solvers as backends.
Jasmin Christian Blanchette (jasminchristian.blanchette@inria.fr)
Jasmin Christian Blanchette (jasminchristian.blanchette@inria.fr), Simon Cruanes (simon.cruanes@inria.fr)
VERIDIS
https://github.com/nunchakuinria