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 KaRaMel compiler to compile Low* to C, and the verified GC is integrated with the OCaml runtime. Our GC is evaluated against off-the shelf OCaml GC and Boehm-Demers-Weiser conservative GC, and the experimental results show that verified GC is pragmatic.