rsmt2. A generic library to interact with SMT-LIB 2 compliant solvers running in a separate system process, such as Z3 and CVC4.
kino. Kinō (帰納: induction, recursion) is an SMT-based, k-induction engine for transition systems.