Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)

TL;DR

This work addresses the challenge of integrating dynamic runtime assertion checking and deductive verification for OCaml programs by using Gospel as a shared specification language. It proposes a workflow where Ortac performs runtime checks against Gospel-specified interfaces, followed by formal proofs with Cameleer (via Why3/WhyML) or CFML (Coq with Separation Logic) to achieve stronger guarantees. Through a case study on a path-checking algorithm in OCamlGraph, the authors demonstrate how RAC and deductive verification complement each other and how Gospel specifications can be leveraged across tools. The results support a flexible certification pipeline that can adapt to program changes and future extensions, promoting broader adoption of formal methods in OCaml development.

Abstract

We present our work on the collaborative use of dynamic and static analysis tools for the verification of software written in the OCaml language. We build upon Gospel, a specification language for OCaml that can be used both in dynamic and static analyses. We employ Ortac, for runtime assertion checking, and Cameleer and CFML for the deductive verification of OCaml code. We report on the use of such tools to build a case study of collaborative analysis of a non-trivial OCaml program. This shows how these tools nicely complement each others, while at the same highlights the differences when writing specification targeting dynamic or static analysis methods.

Figures (4)

• Figure 1: Gospel Queue Specification.
• Figure 2: Gospel certification workflow.
• Figure 3: Excerpt of the Hashtbl module, specified using Gospel.
• Figure 4: Visual representation of the intermediate_value lemma.