  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.
