"Hardcaml Verification Tools" Verification support for Hardcaml. Interface to SAT solvers for combinational logic problems. Code generation for NuSMV for sequential model checking.