Building c2proof: C to Rust Migration with Verification

The push for memory safety is moving the industry toward Rust, but rewriting legacy C codebases manually is impossible at scale. Automated tools exist, but they often produce unreadable, unsafe Rust that doesn't compile out of the box or lacks verifiable correctness.

I built c2proof to fix this. It is a verifier-first wrapper around c2rust.

The Problem

Standard c2rust translates C to unsafe Rust. The output is a starting point, not a solution. You still have to manually verify that the logic remains identical and then painstakingly refactor it into idiomatic, safe Rust. If the transpiled code doesn't mathematically prove its equivalence to the original C, the migration introduces as much risk as it solves.

How c2proof Works

c2proof changes the pipeline:

1. Input: You provide a flat C repository.
2. Transpilation: It runs c2rust under the hood.
3. Verification: This is the core. It generates a verification report proving the mathematical equivalence of the original C and the output Rust.
4. Output: It doesn't just dump files. It compiles the Rust port, ensures it builds, and packages it into a ready-to-merge PR, alongside the proof artifact.

Why the Proof Matters

When migrating critical systems, "it compiles and the tests pass" is not enough. The proof artifact generated by c2proof provides mathematical certainty that the translation preserves the exact semantics of the original code. This reduces the review burden on senior engineers from "checking every line" to "reviewing the proof boundaries."

What's Next

Right now, c2proof handles flat C repositories well. The next milestone is handling complex build systems (Makefiles, CMake) and automatically refactoring the generated unsafe Rust into safe abstractions where the borrow checker can prove it's sound.

---

Written in Rust. Wraps c2rust. Verifier-first migration.