Backstage OCaml: Gospel Ecosystem: Tools Ready to Try, Language Evolving

data/backstage/gospel/2025-10-15-gospel.md

@@ -0,0 +1,54 @@
+---
+title: "The Gospel Ecosystem is Ready for Early Adopters"
+tags: [gospel, platform]
+---
+
+[Gospel](https://github.com/ocaml-gospel/gospel), the behavioral specification language for OCaml, has reached a milestone where early adopters can meaningfully engage with the tools. After years of development and research, parts of the ecosystem are stable enough to try on real codebases, with the goal of gathering feedback as the project works toward production readiness.
+
+## Making Formal Methods Accessible
+
+Traditional formal verification delivers strong correctness guarantees but requires significant expertise and resources. Gospel takes a different approach: one specification language that supports multiple verification strategies, from lightweight runtime testing to full mathematical proofs. This enables gradual adoption—start with automated testing, add focused verification for critical components, and scale to complete proofs where needed.
+
+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, effects, 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.
+
+## The Verification Toolkit
+
+Gospel's tool-agnostic design powers an ecosystem of verification tools at different maturity levels:
+
+**[Ortac](https://github.com/ocaml-gospel/ortac)** (released, ready for production codebases) provides dynamic verification through runtime assertion checking and automated test generation. Ortac/QCheck-STM generates black-box state-machine tests, while Ortac/Wrapper instruments functions with runtime assertions. Ortac/Monolith provides fuzzing integration and remains experimental. These tools have already found real bugs including missing bounds checks in [varray](https://github.com/art-w/varray), integer overflows causing segfaults in [bitv](https://github.com/backtracking/bitv), inconsistent behavior with zero-length vectors in bitv, and unexpected behavior in the standard library's Hashtbl.create.
+
+**[Cameleer](https://github.com/ocaml-gospel/cameleer)** (working toward first release) translates Gospel into [Why3](https://why3.lri.fr/) for deductive verification using automated theorem provers.
+
+**[Peter](https://github.com/ocaml-gospel/peter)** (ongoing research) explores separation logic verification through [CFML](https://gitlab.inria.fr/charguer/cfml) integration with [Coq](https://coq.inria.fr/) for complex heap manipulation proofs.
+
+**[Gospel language](https://github.com/ocaml-gospel/gospel)** (experimental, stabilizing) continues to evolve with ongoing design decisions, but the core concepts are established and the type-checker ensures specifications stay synchronized with code.
+
+## Open Source Infrastructure Strategy
+
+Gospel development is funded by [ANR grant ANR-22-CE48-0013](https://anr.fr/Project-ANR-22-CE48-0013), executed through collaboration between [Nomadic Labs](https://www.nomadic-labs.com/), [Tarides](https://tarides.com/), [Inria](https://www.inria.fr/), and [LMF (Laboratoire Méthodes Formelles)](https://lmf.cnrs.fr/) 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 Platform Integration
+
+Ortac/QCheck-STM and Ortac/Wrapper are released and have proven effective on real codebases. Test runs complete in hundreds of milliseconds, making them practical for CI pipelines. Gospel itself remains experimental with language design still evolving, but it's mature enough for early adopters to write specifications and provide valuable feedback.
+
+The [OCaml Platform roadmap](https://ocaml.org/tools/platform-roadmap#w22-formal-verification) through 2026 includes formal verification as a first-class workflow. The vision: when specifications are defined, `dune test` will automatically report verification failures alongside regular test results, with failures surfaced in editors through the LSP server. [Dune](https://dune.build/) will orchestrate verification tools transparently, making formal methods as accessible as formatting or linting.
+
+## Try It Today
+
+Gospel is available via opam (`opam install gospel`). Integration requires minimal setup: Gospel annotations in `.mli` files, a small configuration file, and a Dune rule to generate tests. The [Ortac tutorial](https://tarides.com/blog/2025-09-10-dynamic-formal-verification-in-ocaml-an-ortac-qcheck-stm-tutorial/) walks through the complete workflow.
+
+The project needs early adopters to:
+- Try Ortac on production codebases and report bugs found
+- Provide feedback on Gospel's specification language design
+- Share use cases that could benefit from formal verification
+- Contribute to the growing ecosystem of verified libraries
+
+The [VOCaL (Verified OCaml Library)](https://github.com/vocal-project/vocal) project demonstrates Gospel's potential with formally verified data structures serving as both reference implementations and reusable components.
+
+## What to Expect
+
+Gospel language design is still evolving—expect changes as design decisions solidify. Ortac plugins are mature enough for serious use, though with some limitations around higher-order functions and OCaml feature coverage. The verification infrastructure is proven: bugs are being found, specifications provide value as documentation, and the path from testing to formal proofs is established.
+
+For teams evaluating formal methods, now is the time to experiment. Early adopter feedback will directly shape how Gospel integrates into the OCaml Platform and becomes part of everyday development workflows.
+
+The ecosystem is open source and actively developed. Explore the [Gospel GitHub organization](https://github.com/ocaml-gospel), review [research](https://inria.hal.science/hal-02157484/file/final.pdf) [papers](https://arxiv.org/pdf/2407.17289) demonstrating collaborative verification workflows, or try Ortac to start finding bugs in your code today.