Kind 2 (main branch)

Binaries automatically built from the main branch on every push.

Built from 6235c3f on 2026-11-01 16:39 UTC.

Kind 2 v3.0.0

In addition to several improvements and bug fixes, this release includes the following new functionalities:

• New map and set types.
• Support for structural equality for arrays, maps, and sets.
• Bottom-up type inference for polymorphic node and function calls (using base types only).
• New syntax for specifying contracts.
• New type ascription operator.
• New conditional expression and blocks with lazy semantics, and short-circuiting versions of 'and', 'or', and '=>'.
• Support for machine integers of arbitrary concrete size, including generation of invariant candidates.
• New built-in operator choose. Like any, it denotes an arbitrary stream of values, but the value is determined by the free variables in the predicate (behaving like a function).
• Support for subranges with symbolic constant bounds.
• Support for quantifiers in refinement type predicates.
• Support for a concise refinement type syntax for quantified variables (e.g. forall (i: int | i > 0)).
• New safety proof production feature based on the new cvc5 CPC proof format (replaces LFSC); compatible with cvc5 1.3.2.
• Support for Bitwuzla as an interpolating solver.
• New contract monitor feature to check a given trace satisfies a contract.
• Verification of constant definitions and realizability checks of free constants (a.k.a system parameters) with refinement types (see documentation for more details).

Please refer to the CHANGES file for a more detailed description and a list of breaking changes, and to the user documentation for more details.

Kind 2 v2.3.0

In addition to several improvements and bug fixes, this release includes the following new functionalities:

• Support for polymorphic user types, nodes, functions, and contracts
• New transparent and opaque modifiers to control the abstraction and refinement of nodes and functions
• Support for function calls with arguments that contain quantified variables and symbolic indices, if they can be inlined
• Support for OpenSMT as a backend solver

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

Kind 2 v2.2.0

In addition to several improvements and bug fixes, this release includes the following new functionalities:

• Support for refinement types
• A new built-in operator, any, to denote an arbitrary stream of values
• Realizability checks for contracts of non-imported nodes and refinement types
  • It also checks the realizability of a node's environment. The check can be disabled by passing --check_environment false
• A new type constructor, history, to refer to an unbounded number of previous values of a stream
• Automatic generation of assumptions to ensure the satisfaction of a node's properties

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

Kind 2 v2.1.1

This release includes some minor improvements and various fixes. Notably:

• Fix soundness bug in IC3IA engine.
• Allow variables with subrange types in the interface of a contract node.
• Accept new versions of cvc5 for proof production (up to 1.1.0).

Kind 2 v2.1.0

This release includes multiple improvements and bug fixes. Notably:

• Add a new option for printing the set of viable states of a realizable contract (--print_viable_states).
• Allow the second argument of a shift operator to be non-constant.
• Add support for the latest versions of SMT solver Bitwuzla (v0.1.1 and above).
• Fix compatibility issue with OCaml 5.0.0+
• Fix printing of values of stateless variables in counterexamples (bug introduced in v2.0.0).
• Fix several bugs related to the definition and use of arrays in Lustre models.
• Add static checks on the definition of global subrange constants.
• Accept the param keyword for the declaration of system parameters (global constants without a definition).
• Add subrange and enum constraints on system parameters.
• Fix type checking and handling of constant node arguments.
• Other improvements and bug fixes in the Lustre front end.

N.B. The Linux and macOS binaries available here are statically linked to the ZeroMQ library.

Kind 2 v2.0.0

In addition to several improvements and bug fixes, this release includes the following new functionalities:

• Support for SMTInterpol as a backend solver.
• New IC3 engine based on Implicit (Predicate) Abstraction.
• Support for subrange types with an open end.

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

The Linux and macOS binaries available here are statically linked to the ZeroMQ library.

Kind 2 v1.9.0

In addition to several improvements and bug fixes, this release includes the following new functionalities:

• Support for elsif clauses in If-Then-Else constraints.
• Dedicated syntax for reachability properties of the form:
  • check reachable P [from <int>] [within <int>]
  • check reachable P at <int>
    The modifiers from, within and at allow users to specify a lower and upper bound on the number of execution steps in the witness trace.
• Dedicated syntax for conditional properties of the form:
  • check A provided B
• Non-vacuity checks for conditional properties and contract mode implications.

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

The Linux and macOS binaries available here are statically linked to the ZeroMQ library.

Kind 2 v1.8.0

In addition to several improvements and bug fixes, this release includes the following new functionalities:

• Add syntax for If-Then-Else constraints and Frame Condition constraints.
• Add support for SMT solver Bitwuzla.
• Add option --flatten_proof to break down LFSC proofs into a sequence of lemmas.

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

The Linux and macOS binaries available here are statically linked to the ZeroMQ library.

Kind 2 v1.7.0

This release includes several bug fixes and the following new features:

• Support for new SMT solver cvc5.
• A revamp of Kind 2's proof production facility.

Please refer to the CHANGES file for a more detailed description and to the user documentation for more details.

The Linux and macOS binaries available here are statically linked to the ZeroMQ library.