veriT
veriT is an SMT solver that has beem primarily developed in the VeriDis team at Inria centre of Lorraine university by Pascal Fontaine (now in Liège, Belgium). VeriT is open source and distributed under the BSD license.
Carcara
Carcara is a proof checker and elaborator for SMT proofs in the Alethe format. It is developed at the Fed. University of Minas Gerais by Haniel Barbosa and his students. It is distributed under the Apache license.
TLAPS
TLAPS is a proof-assistant for verifying concurrent and distributed systems. TLAPS is developed as part of the Tools for Proofs project at the Microsoft Research–Inria joint center in Paris, France. It is developed under the MIT
license.
Dedukti
Dedukti is a logical framework based on the λΠ-calculus modulo in which many theories and logics can be expressed. It is developed by the Deducteam team at Inria – Saclay. It is distributed under the CeCILL-B free software license.
