We report on our ongoing effort to extract verified programs from the Rocq Prover into production-grade C++. While existing compilers and extractors from Rocq target high-level functional languages (OCaml, Haskell) or lower-level imperative ones (C, Rust), none were well-suited for Bloomberg’s requirements. We introduce Crane, a new extraction method to generate idiomatic, functional, memory- and thread-safe C++ code aligned with Bloomberg’s coding practices. Our approach uses modern C++ features to represent Rocq’s functional constructs in a way that preserves readability and maintainability. Our tool can work with mappings of Rocq data types to C++ standard library types, or to Bloomberg’s core library types to facilitate integration with existing C++ code. Additionally, we provide concurrency primitives in Rocq which compile into software transactional memory (STM) constructs in C++, enabling safe concurrent execution. This extended abstract sketches out the design, implementation challenges, and early lessons learned in our quest to integrate verified functional programs into complex concurrent C++ systems.