Kind 2

Kind 2 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of Lustre programs. It takes as input a Lustre file annotated with properties to prove invariant, and outputs for each property either a confirmation or a counterexample, a sequence inputs that falsifies the property. Kind 2 is a from-scratch reimplementation of the Kind model checker.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element