PV4 JKindinfers invariants and checks user-specified properties for a Lustre system

Application domain/field

Type of tool

Model checker

Expected input


.lus file (Lustre language)

Expected output

A list of valid properties and invalid properties, including the time it took to verify/falsify each property.


SMT-based infinite-state model checker for safety properties. Models and properties are specified in Lustre. The JKind architecture consists of 5 separate 'engines':
  1. Bounded Model Checking (BMC) engine for standard iterative unrolling to find counterexamples.
  2. k-Induction engine to perform the inductive step of k-induction
  3. Invariant generation engine that generates invariants based on templates.
  4. Property Directed Reachability (PDR) engine to do property directed reachability.
  5. Advice engine to generate invariants based on previous JKind runs.
Uses SMTInterpol as an SMT-solver to prove/falsify properties.


There exists an Eclipse plug-in with syntax highlighting and static analysis for Lustre code which also runs JKind and reports the results graphically.


Related papers

The JKind Model Checker

Last publication date

18 July 2018

Related tools

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.