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 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.

Implementation (Fx7 prover)

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).