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

Input in Lustre V4 and parts of V6 with support for:
- Signed and unsigned versions of C-style machine integers
- If-Then-Else and Frame Condition blocks
- Refinement types
Assume/guarantee-based contract language
Modular and compositional verification
Counterexample and witness generation
Proof certificate generation
Merit and blame assignment analysis through the computation of:
- Inductive Validity Cores
- Minimal Cut Sets
Realizability and satisfiability checking of contracts
- Deadlocking trace generation for unrealizable contracts
Non-vacuity checks for:
- Conditional properties
- Contract mode implications
Assumption generation for contracts
Multiple model checking engines:
- 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
Graph-based invariant generation
Sharing of discovered invariants between all engines
Support for multiple SMT solvers as backend reasoning engines
- Bitwuzla, cvc5, MathSAT5, SMTInterpol, Yices 2, Yices 1, and Z3
Compilation of executable Lustre models to Rust
Test-case generation

Mailing Lists

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

Documentation

A Lustre Primer for Kind 2 Users: PDF document
User documentation in single HTML page format: v2.2.0 (develop)
User documentation in PDF format: v2.2.0 (develop)
Developer's documentation: develop branch

Try Kind 2 Online

Visit our web interface to try Kind 2 from your browser

Download

Executables

VS Code Extension

You can also install our extension for VS Code which provides support for Kind 2. The extension contains Linux and macOS binaries for Kind 2 and Z3 ready to use. Windows is also supported through WSL2 (see here for more details).

Docker

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

People

Current

Alumni

Kian Weimer
Abdal Mohamed
Andrew Marmaduke
Apoorv Ingle
Mudathir Mohamed
Arjun Viswanathan
Mickaël Laurent
Adrien Champion
Alain Mebsout
Christoph Sticksel
John Bodeen
Kevin Clancy
Mingyu Ma
Baoluo Meng
Eric Burns
Jason Oxley
Ruoyu Zhang

Other contributors to the Kind 2 codebase can be found here.

Publications

Daniel Larraz, Cesare Tinelli. Finding Locally Smallest Cut Sets using Max-SMT. In ACM SIGAda Ada Letters, 2022.

Daniel Larraz, Arjun Viswanathan, Mickaël Laurent, Cesare Tinelli. Beyond model checking of idealized Lustre in Kind 2. In ACM SIGAda Ada Letters, 2022.

Daniel Larraz, Cesare Tinelli. Realizability Checking of Contracts with Kind 2. CoRR abs/2205.09082, 2022.

Daniel Larraz, Mickaël Laurent, Cesare Tinelli. Merit and Blame Assignment with Kind 2. In Proceedings of the 26th International Conference on Formal Methods for Industrial Critical Systems (FMICS), 2021.

Lucas Wagner, Alain Mebsout, Cesare Tinelli, Darren Cofer, Konrad Slind. Qualification of a Model Checker for Avionics Software Verification. In Proceedings of the 9th NASA Formal Methods Symposium (NFM), 2017.

Alain Mebsout, Cesare Tinelli. Proof Certificates for SMT-based Model Checkers for Infinite-state Systems. In Proceedings of 16th Conference on Formal Methods in Computer-Aided Design (FMCAD), 2016.

Adrien Champion, Alain Mebsout, Christoph Sticksel, Cesare Tinelli. The Kind 2 Model-Checker. In Proceedings of 28th International Conference on Computer Aided Verification (CAV), 2016.

Adrien Champion, Arie Gurfinkel, Temesghen Kahsai, Cesare Tinelli. CoCoSpec: A Mode-Aware Contract Language for Reactive Systems. In Proceedings of the 14th International Conference on Software Engineering and Formal Methods (SEFM), 2016.

Pierre-Loïc Garoche, Temesghen Kahsai, Cesare Tinelli. Incremental Invariant Generation using Logic-based Automatic Abstract Transformers. In Proceedings of the 5th NASA Formal Methods Symposium (NFM), 2013.

Temesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli, Mike Whalen. Incremental verification with mode variable invariants in state machines. In Proceedings of the 4th NASA Formal Methods Symposium (NFM), 2012.

Temesghen Kahsai, Cesare Tinelli. PKind: A parallel k-induction based model checker. In Proceedings of 10th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC), 2011.

Temesghen Kahsai, Yeting Ge, Cesare Tinelli. Instantiation-Based Invariant Discovery. In Proceedings of the 3rd NASA Formal Methods Symposium (NFM), 2011.

George Hagen, Cesare Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD), 2008.

George Hagen. Verifying safety properties of Lustre programs: an SMT-based approach. PhD dissertation. Department of Computer Science. The University of Iowa. December 2008.

Acknowledgments

The Kind logo was designed by Daniel Yahyazadeh.

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

AFRL (award #FA8750-13-C-0051)
DARPA (awards #N66001-18-C-4006, N66001-18-C-4012)
GE Global Research
NASA (awards #NNA13AA21C, #NNL14AA06C, #NNX14AI09G)
Collins Aerospace