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