This Sunday we're hosting Joomy Korkut to present Crane, an extraction system from the Rocq Prover to modern C++, developed at Bloomberg with Matthew Z. Weaver. A proof assistant is a good place to build a correct-by-construction program; getting that program out of the prover and into a running system is a separate problem, and it is the one Crane is aimed at:
Proof assistants are increasingly good environments for developing correct-by-construction programs, but deployment raises a different question: how should verified code leave the prover and enter real systems?
Existing extractors mostly target functional languages such as OCaml and Haskell, or drop to plain C or Rust. None of those make a verified development a plausible candidate for integration into a large C++ codebase. Crane instead generates readable, functional-style C++ that uses disciplined ownership, stack-safe control flow, and standard zero-overhead abstractions. It ships as a Rocq plugin, needs no separate runtime system, and can map Rocq datatypes onto C++ standard-library types, or onto the types an existing codebase already uses, so extracted code meets the rest of the system halfway.
Although Crane targets Rocq, the design questions behind it are the ones Lean users run into too: what should extraction actually guarantee, how much runtime should generated code depend on, what should that code look like to a reader who never opens the proof, and how do you build trust in an extractor that is itself unverified? Joomy will cover Crane's design and implementation, its trust model, the AI-assisted workflow used to build it, and early lessons from bridging verified programming and production C++. The work was presented as Crane Lowers Rocq Safely into C++ at RocqPL 2026, and the project is open source and in active development.
Come hear the full story at his talk this Sunday, August 2.