An infinite-state model checker for safety properties in Lustre

JKind is a tool for verifying safety properties of synchronous systems. Systems and their properties are expressed in the Lustre language. Verification is based on k-induction and property directed reachability using a back-end SMT solver. A verified property is guaranteed to be true for all runs of the system. A falsified property is reported with an explicit counterexample demonstrating the property violation.

JKind is used as the back-end model checker for many projects and tools at Rockwell Collins including the AGREE tool and the SIMPAL tool. JKind is designed to be cross-platform, reliable, and easy to extend, with power and performance as secondary goals. JKind is mostly compatible with the KIND and Kind 2 model checkers.

JKind requires at least Java 8. JKind uses SMTInterpol by default (packaged with JKind), but it also supports Z3, Yices 1, Yices 2, CVC4, and MathSAT.

JKind Xtext is an Eclipse plug-in with syntax highlighting and static analysis for Lustre code. It also runs JKind and reports the results graphically.

JKind is primarily developed by Andrew Gacek.