Rocket-fast proof checking for SMT solvers, submitted to TACAS 2008. fx8-r1091.tar.gz contains a snapshot of the fx8 branch of fx7. This includes the C, OCaml and Maude implementation of the proof checker (in trew/ subdirectory). There are also rewrite rules (in prelude.rw) as well as the Coq translation of them (in trew/prelude.v).
Technical report (slightly outdated).
E-Matching for Fun and Profit, describes e-matching algorithms, accepted to SMT workshop 2007. Benchmarks used in the paper.
More info about SMT: SMT-lib.
Available at the BitBucket mercurial repository, under BSD-like license. There is also an Fx8 branch there, where the solver is capable of producing proofs. The current version already passes most of the smt-lib AUFLIA division problems as well as all the Boogie benchmarks. The solver was second in the AUFLIA division of 2007 SMT-COMP.
It is based on C# port of the minisat SAT solver, with which it cooperates in a half-backed DPLL(T) (no theory propagation). It is written in Nemerle (except for minisat).
A ChangeLog is available. It is updated hourly (it's only for the main branch).
The human being behind all that stuff is Michal Moskal. I'm open for cooperation, with potential co-developers as well as potential users (which are probably going to be software verification systems).