Some open source projects I am involved with.
veriT is an open source SMT (Satisfiability Modulo Theories) solver. It is quite lightweight and depends only on the GMP library. VeriT supports the theories uninterpreted functions and linear arithmetic on the reals and integers. Some other theories are supported in an experimental fashion. Quantifiers are also supported reasonably well. Furthermore, veriT can produce really nice proofs.
As part of my PhD research I am one of the core developers of veriT. For more information on the project see the veriT website.
The QBFToys are a set of tools to convert QBF and DQBF problems into higher order problems in TPTP THF format. They can also perform some normalization. Furthermore, experimental SMT-LIB2 output is implemented. [GitHub]