About
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:
- 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
Mailing Lists
- kind2-announce@googlegroups.com
- Release announcements
- kind2-users@googlegroups.com
- Discussions between users and developers
Documentation
- User documentation in single HTML page format
- User documentation in PDF format
- Developer's documentation for current develop branch
Try Kind 2 Online
Visit our web interface to try Kind 2 from your browser
Download
- 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
People
Formerly:
- Adrien Champion
- Alain Mebsout
- Christoph Sticksel
- John Bodeen
- Kevin Clancy
- Mingyu Ma
- Baoluo Meng
- Eric Burns
- Jason Oxley
- Ruoyu Zhang