JKind is a Java implementation of the Kind 2 model checker. Kind 2 is a multi-engine SMT-based automatic model checker for safety properties of Lustre programs.
The latest release of JKind is available on the releases page. This includes the JKind model checker as well as the Lustre2excel and Lustre2kind utilities.
JKind is designed to be cross-platform, reliable, and easy to extend. Power and performance are secondary goals. Additionally, JKind attempts to be mostly compatible with pkind and Kind 2, though this varies over time due to developments in both systems.
By default, JKind requires Yices (version 1) to be installed on your PATH. Alternatively, one can use CVC4, Z3, Yices 2, MathSAT, or SMTInterpol.
