GOSPEL: A Specification Language and Tooling for OCaml
Gospel and Ortac are maintained, documented and released tools, used to test real OCaml libraries and presented at TACAS 2025.
A specification language that lets OCaml programmers describe what their code should do, and tooling that checks the code actually does it.
- Funder
- Agence Nationale de la Recherche (ANR)
- Partners
- INRIA, LMR, Université Paris-Saclay, Nomadic Labs
- Latest Ortac release
- 0.8.0
- Research partners
- 3
The challenge
Most OCaml code says what it does, not what it is supposed to do. The type system catches a great deal, but it cannot express that a function must be given a sorted list, or that a buffer is never read after it is freed. That knowledge usually lives in documentation, or in the author's head, and neither can be checked by a machine.
Formal specification can close the gap, but it has a reputation for being costly and specialist. The work only pays for itself if an ordinary OCaml developer can write a specification without learning a separate discipline, and if something useful happens once they have.
The approach
Gospel is a tool-agnostic behavioural specification language for OCaml. A
specification is written in a comment above an interface, so it sits with the
code it describes and travels with it, and gospel check type-checks it like
any other part of the build.
Being tool-agnostic matters. The same specification can drive different kinds of checking rather than being tied to one verifier, which is what makes the effort of writing it worth repeating.
Ortac is the tool that turns those specifications into something executable. It translates a subset of Gospel into OCaml and generates runtime checks, so a developer gets a test suite out of the specification they have already written, rather than having to write both.
Tarides worked on this with INRIA, the LMR laboratory at Université Paris-Saclay and Nomadic Labs, funded in part by the Agence Nationale de la Recherche. The work included extending the Gospel typechecker, supporting the OCaml documentation generator odoc so specifications appear in generated documentation, and runtime testing of the code.
The outcome
Gospel and Ortac are both maintained and actively developed in the ocaml-gospel organisation.
Ortac reached version 0.8.0 in September 2026, adding support for testing code that uses domains, which matters now that OCaml 5 has made parallelism ordinary. We wrote that release up in this earlier post on Ortac 0.8.0, and the approach is explained end to end in this earlier Ortac and QCheck-STM tutorial.
The work was presented at TACAS 2025 as "Dynamic Verification of OCaml Software with Gospel and Ortac/QCheck-STM", by Nikolaus Huber, Naomi Spargo, Nicolas Osborne, Samuel Hym and Jan Midtgaard.