Gospel is a behavioural specification language for OCaml program. It provides
developers with a non-invasive and easy-to-use syntax to annotate their module
interfaces with formal contracts that describe type invariants, mutability,
function pre-conditions and post-conditions, effects, exceptions, and much
We designed Gospel to provide a tool-agnostic frontend for bringing formal
methods into the OCaml ecosystem, meaning that we make no assumptions on the
future use of the specifications.
You can use Gospel specifications to complete and precise your documentation
comments with non-ambiguous annotations and use a type-checker to ensure they
always remain in sync. Other tools also rely on these annotations to provide
additional features such as automated deductive verification or runtime
Please feel free to visit the project
page if you wish to learn more about
Gospel is not yet available on Opam repositories. You can install it via pinning:
$ opam pin add gospel.dev firstname.lastname@example.org:ocaml-gospel/gospel $ opam install gospel
This will install the
gospel tool binary, as well as the developer library if you
wish to build your software on top of Gospel. You may check the installation with.
$ gospel --version gospel version xxxxxx
Gospel contracts live in OCaml interface files (
.mli), as special comments
starting with the
val max_array: int array -> int (*@ m = max_array a requires Array.length a > 0 ensures forall i. 0 <= i < Array.length a -> a.(i) <= m ensures exists i. 0 <= i < Array.length a /\ a.(i) = m *)
Gospel provides a type-checker that ensures that your specifications are
well-formed, well-typed, and remain in sync with the interface they annotate!
$ gospel check max_array.mli OK
Tools using Gospel
At the moment, three tools leverage Gospel specifications to provide more
guarantees to your programs:
Cameleer. A tool that extends
Gospel to implementation files to provide semi-automated deductive
verification of OCaml programs.
Ortac. A runtime assertion
checking tool based that generates verifying code for your test suites or
Why3gospel. A Why3 plugin that
lets you verify that a program proof refines the Gospel specifications before
extracting it to OCaml.
This project is licensed under the MIT license.
See the LICENSE file for more information.
Gospel was initially developed by Cláudio Lourenço (LRI postdoctorate).
It is now maintained by Clément Pascutto, Mário Pereira, and Jean-Christophe
The full list of contributors is available
The development is supported by:
>= "0.23.0" & < "0.26.0"