I've been working on translating (and modifying) parts of John Harrison's automated theorem proving book from Ocaml into a Rust library.

Highlights so far are an implementation of DPLL with conflict-clause learning that lets us solve hard sudoku problems in less than a second (not competitive w/ SAT solvers like MiniSat, but not bad either), and a Herbrand style semi-decision procedure for first-order validity.

There's lots of room for more sophisticated methods and optimization. More to come soon.