[POPL'26] Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation(…)

Описание: Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic (Video, POPL 2026)
Clément Allain, Gabriel Scherer
(Inria, France; Inria, France / Université Paris Cité, France)

Abstract: The release of Ocaml 5, which introduced parallelism in the OCaml runtime, drove the need for safe and efficient concurrent data structures. New libraries like Saturn address this need. This is an opportunity to apply and further state-of-the-art program verification techniques.

We present Zoo, a framework for verifying fine-grained concurrent OCaml 5 algorithms. Following a pragmatic approach, we defined a limited but sufficient fragment of the language to faithfully express these algorithms: ZooLang. We formalized its semantics carefully via a deep embedding in the Rocq proof assistant, uncovering subtle aspects of physical equality. We provide a tool to translate source OCaml programs into ZooLang syntax embedded inside Rocq, where they can be specified and verified using the Iris concurrent separation logic. To illustrate the applicability of Zoo, we verified a subset of the standard library and a collection of fined-grained concurrent data structures from the Saturn and Eio libraries.

In the process, we also extended OCaml to more efficiently express certain concurrent programs.

Article: https://doi.org/10.1145/3776701

ORCID: https://orcid.org/0009-0005-2972-5181, https://orcid.org/0000-0003-1758-3938

Video Tags: Verification, Separation Logic, Rocq, Iris, OCaml 5, Concurrent Algorithms, doi:10.1145/3776701, orcid:0009-0005-2972-5181, orcid:0000-0003-1758-3938

Presentation at the POPL 2026 conference, Jan 11-17, 2026, https://popl26.sigplan.org/
Sponsored by ACM SIGPLAN.