一句话：提出 Zoo 框架，在 Rocq 中借助 Iris 分离逻辑验证 OCaml 5 细粒度并发算法，并验证了标准库与 Saturn/Eio 中的数据结构。
OCaml 5 在运行时引入并行能力后，安全高效的并发数据结构成为迫切需求，Saturn 等新库应运而生，也为程序验证技术提供了应用场景。本文提出 Zoo——一个用于验证细粒度并发 OCaml 5 算法的框架。作者采取务实路线，定义了一个受限但足以忠实表达此类算法的语言片段 ZooLang，并在 Rocq 证明助手中通过深嵌入仔细形式化其语义，过程中揭示了物理相等（physical equality）的若干微妙之处。Zoo 还提供工具将 OCaml 源程序翻译为嵌入 Rocq 的 ZooLang 语法，从而可用 Iris 并发分离逻辑进行规约与验证。评估方面，作者验证了标准库的一个子集，以及来自 Saturn 和 Eio 库的一组细粒度并发数据结构；在此过程中还扩展了 OCaml，以更高效地表达某些并发程序。
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{AllainS26,
title = {Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic},
author = {Clément Allain and Gabriel Scherer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776701}
}