2025-10-01 –, CyberSecurity
This talk presents Gospel (Generic OCaml SPEcification Language), an emerging open source ecosystem for accessible formal verification currently under development through French National Research Agency funding. Gospel enables developers to write strongly-typed behavioral specifications that can be consumed by multiple verification tools.
While the work on static verification tools like Cameleer is in progress, the ecosystem demonstrates a "gradual verification" approach where organizations can start with dynamic testing of all code and progressively apply formal proofs to critical components. The Ortac tool, developed at Tarides, translates Gospel specifications into executable OCaml code for defensive programming, runtime assertion checking, and specification-driven testing.
The ecosystem emerging around Gospel provides a practical entry point to formal methods that industry can adopt today!
Formal verification provides mathematical guarantees of software correctness but has historically been limited to organizations with access to expensive proprietary tools or experts to work on (often closed-source) proofs. This talk presents Gospel (Generic OCaml SPEcification Language) and its emerging open source ecosystem, which has the mission of providing accessible formal methods for mission critical applications, and, ultimately, for everyone who aims to build reliable systems. By establishing a formally verified Open Source ecosystem around Gospel, we expect that formal verification becomes a practical and cost-efficient alternative to common testing practices in the software industry.
Gospel enables developers to write specifications that can be used to create mathematical proofs, and automatically generate both runtime security checks and documentation from a single source. Recent research (TACAS 2025) demonstrates how Gospel-based tools have identified critical vulnerabilities in OCaml libraries and educational codebases that conventional testing missed.
The presentation covers Gospel's potential applications in key domains:
Supply Chain Security: Formal specifications can provide verifiable guarantees about component behavior.
API Behavior Contracts: Formal pre/post-conditions and invariants provide guarantees about function behavior, preventing security vulnerabilities from incorrect API usage.
Algorithm Verification: Critical algorithms can be formally proven to work correctly under all conditions.
The French National Research Agency funds Gospel development through collaboration between INRIA, Tarides, and Nomadic Labs, recognizing formal verification accessibility as strategically important for cybersecurity independence. This investment demonstrates growing recognition of formal methods as essential infrastructure.
We will examine the current state of Gospel tooling, discuss research results showing vulnerability discovery, and explore how organizations might evaluate these open source approaches as they mature. All Gospel tools and documentation are freely available under open source licenses, ensuring that formal verification capabilities remain community-controlled rather than vendor-dependent.
Sabine Schmaltz is Developer Advocate at Tarides, who maintain and develop OCaml tooling and contribute to the OCaml ecosystem. She holds a PhD in Computer Science with research experience in formal verification of system-level C code using Isabelle/HOL, conducted through the German Federal Ministry-funded Verisoft XT project. At Tarides, she manages OCaml community outreach, hosts the FUN OCaml developer conference, and maintains the open source OCaml.org website.