View on GitHub

Kind 2

Multi-engine SMT-based automatic model checker for synchronous reactive systems


Kind 2 is an open-source, multi-engine, SMT-based automatic model checker for safety properties of synchronous reactive systems expressed as in an extension of the Lustre language. It takes as input one or more Lustre files annotated with properties to be proven invariant, and outputs for each property either a confirmation or a counterexample, i.e., a sequence inputs that falsifies the property.

Kind 2 is a from-scratch reimplementation of the Kind model checker.

Main features:

Mailing Lists
Release announcements
Discussions between users and developers


Try Kind 2 Online

Visit our web interface to try Kind 2 from your browser