# \[ANN\] Ortac/QCheck-STM 0.4.0 Dynamic formal verification beyond one system under test

**URL:** https://discuss.ocaml.org/t/ann-ortac-qcheck-stm-0-4-0-dynamic-formal-verification-beyond-one-system-under-test/15427
**Category:** Ecosystem
**Tags:** announce, testing
**Created:** [October 11, 2024, 3:34pm UTC](https://discuss.ocaml.org/t/ann-ortac-qcheck-stm-0-4-0-dynamic-formal-verification-beyond-one-system-under-test/15427 "2024-10-11T15:34:17Z")
**Posts on this page:** 1
**Page:** 1

<div class="post-metadata">

### Author: ![n-osborne](https://avatars.discourse-cdn.com/v4/letter/n/4da419/32.png) [@n-osborne](https://discuss.ocaml.org/u/n-osborne)
#### Post date: [October 11, 2024, 3:34pm UTC](https://discuss.ocaml.org/t/ann-ortac-qcheck-stm-0-4-0-dynamic-formal-verification-beyond-one-system-under-test/15427/1 "2024-10-11T15:34:17Z")

</div>

Hi everyone!

I’m very pleased to announce this exciting new release of `ortac-qcheck-stm.0.4.0`!

This new release brings some exciting new features, mostly the result of Nikolaus Huber’s contributions! Thank you Nik!

Ortac/QCheck-STM is a test generator based on the [QCheck-STM](https://github.com/ocaml-multicore/multicoretests) model-based testing framework and the [Gospel](https://github.com/ocaml-gospel/gospel) specification language for OCaml.

You can find the project on [this repo](https://github.com/ocaml-gospel/ortac) and install the released packages via `opam`.

It is also encourage to install `ortac-dune` to avoid having to write too much dune boilerplate.

In particular, this release extend Ortac/QCheck-STM so that the generated tests will include functions that can take multiple System-Under-Tests as argument and/or that can return one. So now, if we write Gospel specifications for `append`-like functions, Ortac/QCheck-STM will include them in the generated tests!

Happy testing!