We present the implementation and mechanized verification of a realistic parallel scheduler for OCaml 5 using the Iris-based Zoo framework. Similarly to Domainslib, it relies on a work-stealing strategy to perform load balancing but also supports other scheduling strategies thanks to its flexible interface. e provide basic benchmarks demonstrating that its performance is on par with other schedulers from the OCaml ecosystem. As part of this effort, we verify the Chase-Lev work-stealing deque, as implemented in the Saturn library. We show that it features a subtle external and future-dependent linearization point. To deal with it, we introduce new abstractions for reasoning about prophecy variables in Iris.

@article{paperbot3700,
  title = {A Verified Parallel Scheduler for OCaml 5},
  author = {Clément Allain and Gabriel Scherer},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {PLDI},
  year = {2026},
  doi = {10.1145/3808337}
}