Part of the benefit of open-source development is the opportunity to collaborate on projects across traditional organisational boundaries, such as academia and industry. Tarides is part of a larger effort to develop a behavioural specification language and associated tooling for OCaml. The project creates an easy-to-use foundation for formal specifications, allowing users to include them in generated documentation and perform automated testing and verification. This important work is funded in part by ANR.

The Gospel Project

The French National Research Agency (ANR) is a public institution in France that funds innovative research projects where public institutions collaborate with each other or the private sector. OCaml was invented at the French National Institute for Research in Digital Science and Technology, INRIA, and ANR is funding a research project as a collaboration between INRIA, Tarides, LMF UPSaclay, and Nomadic Labs. The goal of the project is to develop and improve the specification language Gospel alongside its tooling ecosystem and demonstrate its usefulness in different case studies.

What is Gospel?

Gospel is a contract-based behavioural specification language that allows you to write specifications in the module interface you want to specify. As a specification language, it is a formal language, meaning its semantics are precisely defined (by means of translation into Separation Logic, see this paper).

By behavioural specification language, we mean a language that allows you to describe the expected functional behaviour of a function. Specifications don't reference resources such as CPU time or memory size, but only what the program does (so-called functional behaviour). Expected behaviour is expressed as a contract. The basic premise is that as long as the user of the library calls functions with arguments that respect the expressed preconditions, then the implementation of the library should behave per their description.

Per se, Gospel doesn't guarantee that your implementation respects its given specifications, it is simply a language that allows you to express precisely what your code should do. However, note that Gospel still comes with a type-checker. This type-checker lets you check that your specifications are well-formed and in sync with the interface. For example, if you add an extra argument to a function in your library, the Gospel type-checker will tell you if you forgot to update the specifications accordingly.

Gospel is a relatively new specification language and is bound to evolve, but it is already mature enough to specify a diverse set of libraries. It provides developers with a non-invasive and easy-to-use syntax to annotate their module interfaces with formal contracts describing type invariants, mutability, function pre- and postconditions, exceptions, etc. For example, let's say you want to specify a fixed-size stack. The type declaration in the module interface would look like:

type a t
(*@ model capacity : integer
    mutable model contents : a sequence
    with s
    invariant Sequence.length s.contents <= s.capacity *)

You give two logical models to your datatype: an immutable one for the capacity of the stack and a mutable one for the content. Then, given a stack, s, you can formulate type invariants. Namely, the stack should not have more elements than capacity allows. The specification for the create function would look like:

val create : int -> 'a t
(*@ s = create n
    requires n > 0
    ensures s.capacity = n
    ensures s.contents = Sequence.empty *)

The first line binds the arguments and the returned value to names so that we can talk about them. Then we express the precondition that the given argument should be strictly positive and the two postconditions that fill the logical models as expected.

Gospel is also a tool-agnostic specification language, meaning it doesn’t make any assumption about how and by which tools its specifications will be consumed. Some users use Gospel specifications to provide proofs of functional correctness for their implementations. For example, Cameleer does so by leveraging the power of the Why3 deductive verification platform. At Tarides, with the Ortac project, we explore how to use Gospel specifications to do runtime assertion checking.

Gospel was initially developed by Cláudio Lourenço (LRI post-doctorate) and is currently maintained by Jean-Christophe Filliâtre, Samuel Hym, Nicolas Osborne, and Mário Pereira. Clément Pascutto also maintained Gospel for several years as part of his PhD work at Tarides and LRI.

A Tool for Gospel: Ortac

Ortac stands for OCaml RunTime Assertion Checking. Clément's PhD thesis initiated the Ortac project which has since grown into a greater cooperative effort. Samuel Hym and Nicolas Osborne currently maintain it. At its core, Ortac translates the computable subset of Gospel terms into OCaml code. In addition, it provides a plugin architecture to implement different uses of this translation. Translating Gospel terms into runnable OCaml code opens the possibility of checking an implementation against the interface specification at runtime.

Three plugins have been built upon this translation, plus a fourth one, which is slightly different. Let’s take a look:

1. The Ortac/Wrapper plugin was developed during Clément's PhD. Given the Gospel specified interface of a module, this plugin generates a new module with the same interface, wrapping the initial implementation with runtime checks coming from Gospel specifications. When a Gospel specification is violated by the client for preconditions or by the initial implementation for postconditions, the wrapped version will output an error message providing the user with useful information, such as which Gospel clause they have violated. Users can then use the new wrapped module in place of the original one in their project, to, for example, aid in debugging efforts. This plugin is still considered experimental.
2. The Ortac/Monolith plugin, which is based on Ortac/Wrapper and is the product of an internship, was presented at ICFP 2021. Given the specified interface of a module, this plugin generates the Monolith standalone program, testing the initial implementation against the wrapped one. The idea is that, in case the implementation doesn't respect the specification, the wrapped version will return a special Ortac error while the bare initial one won't. Monolith allows you to use fuzzing to test your library and provides a runnable scenario that demonstrates the unexpected behaviour. This plugin is also still considered experimental.
3. The Ortac/QCheck-STM plugin is based on Naomi Spargo's internship project. Given the specified interface of a module and some user-provided extra information, this plugin generates standalone QCheck-STM tests. In addition to avoiding having to write the QCheck-STM test by hand and as a recently added feature, in case of a test failure, the generated tests will inform you which part of the specification has been violated, give you a runnable scenario demonstrating the unexpected behaviour, and the expected returned value when the Gospel specifications allow to compute it. This plugin has been released.
4. The Ortac/Dune plugin is slightly different as it doesn't rely on a Gospel specification. Instead, it helps you by generating the Dune rules necessary to run another plugin. So far, only the command for Dune rules related to the Ortac/QCheck-STM plugin is available, as it is the only one that has been released. The command yields the Dune rules required to generate and run the tests.

Future Steps

Regarding Ortac, the 0.3.0 version of a set of Ortac packages, including the first Ortac/Dune release, has recently been published. Among other improvements and fixes, this release makes dynamic formal verification with Ortac very easy. The team is now investigating how to test more functions by lifting some limitations that come with a naive use of the QCheck-STM test framework, with an intern (Nikolaus Huber) working on this last topic.

With Gospel 0.3.0 published, the upcoming goals centre around continuing maintenance and development, using our engineering expertise to help our research partners bring new features to the Gospel language.

Until Next Time

Do you want to try out Gospel and Ortac? Check out the documentation and report back on your experience! If you want to stay informed about our projects, follow us on X (formerly known as Twitter) and LinkedIn for all our latest updates. Are you interested in using Gospel for your own projects? Contact us, and we will be happy to discuss the benefits of implementing specification languages in your workflow.

Tarides champions open-source development. We create and maintain key features of the OCaml language in collaboration with the OCaml community. To learn more about how you can support our open-source work, discover our page on GitHub.

We are always happy to discuss commercial opportunities around OCaml. We provide core services, including training, tailor-made tools, and secure solutions. Contact us today to learn more about how Tarides can help your teams realise their vision.