Researchers formally verified a multi-generation garbage collector in Rocq+VST, written in C and compatible with OCaml data types. The verification uses a modular API specification independent of implementation details, demonstrating adequacy through verified client programs and supporting components like forwarding functions.