Extracting verified C++ from the Rocq theorem prover at Bloomberg

A new extraction system from Rocq to functional-style, memory-safe, thread-safe, readable, valid, performant, and modern C++.

Interestingly, this can be integrated into production system to quickly formally verify critical components while being fully compatible with the existing Bloomberg's C++ codebase.

Why does it have to be C++? Can the extraction strategy be ported to Rust? Rust is just getting a lot more attention from formal methods folks in general, and has good basic interop with C.

Where is this team based? Was curious if it was the London office.

Getting the AI to work with Rocq is a useful goal, Lean has been useful so far.