Sabine Schmaltz
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.
Session
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!