View all changes

Gospel Ecosystem: Tools Ready to Try, Language Evolving

Gospel, the behavioral specification language for OCaml, is at an interesting inflection point. After years of development and research, some tools in the ecosystem—particularly Ortac/QCheck-STM—are ready for early adopters to try on real codebases. At the same time, Gospel itself is preparing a major release with breaking changes as the language design continues to evolve.

Making Formal Methods Accessible

Traditionally, formal verification delivers strong correctness guarantees but requires significant expertise and resources. Gospel's vision is different: one specification language that will eventually support multiple verification strategies, from lightweight runtime testing to full mathematical proofs. While the testing tools are available today, the proof tools are still under development.

This approach follows a successful pattern established in other language ecosystems. ACSL (ANSI/ISO C Specification Language) provides a behavioral specification language for C programs that supports multiple verification tools including Frama-C, while JML (Java Modeling Language) offers a unified specification language for Java that can be used for runtime assertion checking, static analysis, and theorem proving. Similarly, Eiffel pioneered the concept of design by contract with specifications embedded directly in the programming language. Gospel brings this proven strategy to OCaml.

Gospel provides a non-invasive syntax for annotating OCaml interfaces with formal contracts in special comments beginning with @, describing type invariants, mutability, pre-conditions, post-conditions, and exceptions. The specifications use logical models to represent abstract types—for example, modeling a queue as a mathematical sequence to specify how operations transform its contents.

Status of Gospel and its Toolkit

Gospel language (experimental, major changes coming) is preparing a release with significant breaking changes. Early adopters should expect the language to evolve and should not expect bug fixes in the current version.

Gospel's tool-agnostic design powers an ecosystem of verification tools at different maturity levels:

Ortac provides dynamic verification through runtime assertion checking and automated test generation:

  • Ortac/QCheck-STM (released, battle-tested) generates black-box state-machine tests and has found real bugs including missing bounds checks in varray, integer overflows causing segfaults in bitv, inconsistent behavior with zero-length vectors in bitv, and unexpected behavior in the standard library's Hashtbl.create. Supports higher-order functions like map.
  • Ortac/Wrapper (released, early stage) instruments functions with runtime assertions but hasn't been extensively tested in production yet.
  • Ortac/Monolith (experimental) provides fuzzing integration with Monolith.

Cameleer (working toward first release) translates Gospel into Why3 for deductive verification using automated theorem provers.

Peter (ongoing research) explores separation logic verification through CFML integration with Coq for complex heap manipulation proofs.

Open Source Infrastructure Strategy

Gospel development is funded by ANR grant ANR-22-CE48-0013, executed through collaboration between Nomadic Labs, Tarides, Inria, and LMF (Laboratoire Méthodes Formelles) at Université Paris-Saclay. The project demonstrates how open source can transform formal verification economics: rather than each organization independently funding expensive verification efforts, shared open tooling and verified libraries benefit the entire ecosystem.

Current State and Integration

Ortac/QCheck-STM is released and has proven effective on real codebases, with test runs completing in hundreds of milliseconds. Gospel itself is experimental with major language changes planned, so early adopters should expect breaking changes.

The OCaml Platform roadmap through 2026 includes formal verification as a workflow goal. Currently, using Ortac requires writing Dune rules manually. Integration with Dune as a first-class feature requires further discussion and development.

Try Ortac/QCheck-STM Today

Install via opam:

opam install ortac-qcheck-stm

This installs the ortac command-line tool and everything needed to generate QCheck-STM tests from Gospel specifications. See the Ortac tutorial for a complete walkthrough, or check the QCheck-STM plugin README for details.

The project welcomes early adopters who want to:

  • Try Ortac/QCheck-STM on production codebases and report bugs found
  • Provide feedback on Gospel's evolving specification language
  • Share use cases that could benefit from formal verification

The VOCaL (Verified OCaml Library) project demonstrates Gospel's potential with formally verified data structures.

What to Expect

The verification infrastructure is already useful for testing — bugs are being found, specifications provide value as documentation. Work on establishing the path from testing to formal proofs is ongoing, but the proof tools aren't ready for general use yet.

Learn More

The ecosystem is open source and actively developed. Explore the Gospel GitHub organization, or review research papers:

For teams interested in specification-driven testing, Ortac/QCheck-STM is ready to try. For those interested in formal proofs or stable Gospel language features, watch the project but expect it will be some time before these are production-ready.

Contact: @n-osborne | Get started: Ortac Tutorial | Documentation: Gospel docs