[OCaml'25] A Mechanically Verified Garbage Collector for OCaml

A Mechanically Verified Garbage Collector for OCaml (Video, OCaml 2025) Sheera Shamsu, Dipesh Kafle, Dhruv Maroo, Kartik Nagar, Karthikeyan Bhargavan, and KC Sivaramakrishnan (IIT Madras; NIT Trichy, Tiruchirappalli, India; IIT Madras, Chennai; IIT Madras; Cryspen, France; IIT Madras and Tarides) Abstract: The GC is a critical component of the OCaml runtime system, and its correctness is essential for the safety of OCaml programs. Therefore, we propose a strategy for crafting a correct, proof-oriented GC from scratch, designed to evolve over time with additional language features. Our approach neatly separates abstract GC correctness from OCaml-specific GC correctness, offering the ability to integrate further GC optimizations, while preserving core abstract GC correctness. As an initial step to demonstrate the viability of our approach, we have developed a verified stop-the-world mark-and- sweep GC for OCaml. The approach is mechanized in F* and its low-level subset Low*. We use the