[clarus]

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.

[InkCanon]

Would be interesting to see how performant it is (or how easily you can write performant code).

[seeknotfind]

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;
    };

This is ... okay, if you like formal systems, but I wouldn't call it performant. Depending on what you are doing, this might be performant. It might be performant compared to other formally verified alternatives. It's certainly a lot nicer than trying to verify something already written in C++, which is just messy.

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].

One of the things formal verification people complain about is that ARM doesn't have a standard memory model, or CPU cache coherence is hard to model. I don't think that's what this project is about. This project is having basically provable code. They also say this in their wiki:

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.

[joomy]

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.

[seeknotfind]

Thanks, yeah, I did see some of the pure C++ types getting converted. Though it makes a lot of sense why you had to go with shared_ptr for generic inductive types.

Have you considered combinatorial testing? Test code generation for each sample program, for each set of mappings, and ensure they all have the same behavior. If you look at the relative size or performance, it could allow you to automatically discover this issue. Also, allocation counting.

Hey also sucks you are not in SF. I'm looking for people into formalization in the area, but I haven't found any yet

[joomy]

> Have you considered combinatorial testing?

Our plan was to do random Rocq program generation and differential testing of Crane extracted code versus other extraction methods and even CertiCoq. But fixing a program and trying different mappings would certainly be a useful tool for any dev who would like to use our tool, and we should put it on our roadmap.

[seeknotfind]

Very cool. Can't wait to see what's next with this project! Congrats on the huge scale of tests/examples as well.

[csto12]

Are LLMs part of your development workflow for something like this? If they are, is it through something like Claude Code or something else?