About
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.
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
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
Documentation
- User documentation in single HTML page format.
- User documentation in PDF format.
- Caml documentation (develop branch).
- Developer's documentation for current develop branch
Try Kind 2 Online
Visit our web interface to try Kind 2 from your browser.
Contact
People
Formerly:
- Alain Mebsout
- Christoph Sticksel
- John Bodeen
- Kevin Clancy
- Mingyu Ma
- Baoluo Meng
- Eric Burns
- Jason Oxley
- Ruoyu Zhang