Dynamic Formal Verification in OCaml: An Ortac/QCheck-STM Tutorial (opens in new tab)

You may have read our recent post discussing our involvement in the Gospel Project. In today's follow-up post, we will focus on What is Ortac? Ortac aims to give OCaml programmers easy access to dynamic formal verification, also known as specification-driven testing. At its core, it translates computable Gospel terms into equivalent OCaml expressions. Different Ortac modes can then use these translations to generate OCaml code. This post is about the Ortac/QCheck-STM Mode In contrast, QCheck-...