Open Source Formal Verification: The Gospel Ecosystem

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! By Sabine Schmaltz