View on GitHub

Kind 2

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

About

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

kind2-announce@googlegroups.com
Release announcements
kind2-users@googlegroups.com
Discussions between users and developers

Documentation

Try Kind 2 Online

Visit our web interface to try Kind 2 from your browser

Download

Executables

Docker

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

People

Former Developers

External Contributors

Acknowledgments

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