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 finite-state or infinite-state synchronous reactive systems expressed as in an extension of the Lustre language. In its basic configuration 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. More advanced features include contract-based compositional verification, proof generation for proven properties, and contract-based test generation.

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



To run the macOS binary the ZeroMQ library (version 4.x or later) must be installed on your system. You can install it by running brew install zmq.


Kind 2 is also available on Docker Hub. Follow these steps to install one of the images.


Former Developers

External Contributors


The development of Kind 2 has been partially supported with funding from the following organizations.