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.
- Bounded Model Checking (BMC)
- k-induction with lazy path compression
- IC3 aka PDR
- Invariant discovery from templates for a syntactic analysis of the system
- Message-passing based parallel composition of model checking engines
- Sharing of discovered invariants between all engines
- Input in Lustre V4 and parts of V6 translated to a modular transition system
- Use of either of the SMT solvers Z3, CVC4 and Yices
- Assume/guarantee-based contract language
- Modular and compositional verification
- An improved graph based invariant generation technique
- Compilation of Lustre to Rust
- Test-case generation
- Proof certificate generation
- Release announcements
- Discussions between users and developers
- Download Kind 2 v1.1.0 for Linux (64 bits)
- Download Kind 2 v1.1.0 for Mac OS X (64 bits)
- Download Kind 2 v1.1.0 sources
- User documentation in single HTML page format.
- User documentation in PDF format.
- Caml documentation (develop branch).
- Developer's documentation for current develop branch
Visit our web interface to try Kind 2 from your browser.