Kind 2 (nightly version)

Nightly build (64-bit binaries).

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.

Kind 2 v1.6.0

In addition to several improvements and bug fixes, this release includes a new implementation of Kind 2's language front-end with:

• Support for forward references to nodes and modes in contracts.
• Individual namespaces for imported contracts.
• Enhanced type checking of composite data types.

Although we strongly encourage users to use the new front-end, the old front-end can still be enabled for now by passing --old_frontend true to Kind 2.

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

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

Kind 2 v1.5.1

This release includes performance improvements and various fixes. Notably:

• Improve performance of realizability checks with Z3.
• Fix realizability check of imported functions.
• Fix realizability check when --ae_val_use_ctx is false (bug introduced in v1.5.0).
• Fix generation of tracing information when a contract is proven unrealizable.
• Fix shape of generated invariant candidates when --invgen_all_out is true.
• Fix generation of SMT-LIB 2 certificates.
• Make Kind 2 compatible with the latest version (5.1.4) of the OCaml bindings for ZMQ.

In addition, this version adds support for a new Visual Studio Code extension for Kind 2.

Thanks to Andreas Katis for his feedback and bug reports.

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

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