Extracting verified C++ from the Rocq theorem prover at Bloomberg
bloomberg.github.io89 points by clarus 4 days ago
89 points by clarus 4 days ago
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.
We do C++ only because C++ is the primary programming language at Bloomberg, and we aim to generate verified libraries that interact easily with the existing code. More about our design choices can be found here: https://bloomberg.github.io/crane/papers/crane-rocqpl26.pdf
Getting the AI to work with Rocq is a useful goal, Lean has been useful so far.
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.
Would be interesting to see how performant it is (or how easily you can write performant code).
From tests/basics/levenshtein/levenshtein.cpp:
struct Ascii {
std::shared_ptr<Bool0::bool0> _a0;
std::shared_ptr<Bool0::bool0> _a1;
std::shared_ptr<Bool0::bool0> _a2;
std::shared_ptr<Bool0::bool0> _a3;
std::shared_ptr<Bool0::bool0> _a4;
std::shared_ptr<Bool0::bool0> _a5;
std::shared_ptr<Bool0::bool0> _a6;
std::shared_ptr<Bool0::bool0> _a7;
};
From theories/Mapping/NatIntStd.v:
- Since [int] is bounded while [nat] is (theoretically) infinite,
you have to make sure by yourself that your program will not
manipulate numbers greater than [max_int]. Otherwise you should
consider the translation of [nat] into [big_int].
https://github.com/bloomberg/crane/wiki/Design-Principles#4-...
> Crane deliberately does not start from a fully verified compiler pipeline in the style of CompCert.
What this means is that you can formalize things, and you can have assurances, but then sometimes things may still break in weird ways if you do weird things? Well, that happens no matter what you do. This is a noble effort bridging two worlds. It's cool. It's refreshing to see a "simpler" approach. Get some of the benefits of formal verification without all the hassle.
Hi, I'm one of Crane's developers. You can map Rocq `bool`s to C++ `bool`, Rocq strings to C++ `std::string`s, etc. You just have to manually import the mapping module: https://github.com/bloomberg/crane/blob/6a256694460c0f895c27...
The output you posted is from an example that we missed importing. It's also one of the tests that do not yet pass. But then again, in the readme, we are upfront with these issues:
> Crane is under active development. While many features are functional, parts of the extraction pipeline are still experimental, and you may encounter incomplete features or unexpected behavior. Please report issues on the GitHub tracker.
I should also note, mapping Rocq types to ideal C++ types is only one part of it. There are still efficiency concerns with recursive functions, smart pointers, etc. This is an active research project, and we have plans to tackle these problems: for recursion: try CPS + defunctionalization + convert to loops, for smart pointers: trying what Lean does (https://dl.acm.org/doi/10.1145/3412932.3412935), etc.
Where is this team based? Was curious if it was the London office.
We're based in NYC. The Infrastructure and Security Research team in the CTO Office, in particular.
And we are looking for senior researchers to join us, see https://x.com/jvanegue/status/2004593740472807498