e5a1c07 · problem
01/The transpiler is solved. Trust isn't.
You have a legacy C codebase. You want it in Rust — memory safety, modern toolchain, crates ecosystem.
So you run a C-to-Rust converter. It outputs thousands of lines. Now the real questions start: Does it compile? What did it hide? How much unsafe came across? Which symbols didn't resolve? Who reviews 40,000 mechanical lines against the original?
Most teams answer by not migrating. The output lands in a folder, gets skimmed once, and dies there. The bottleneck was never translation — it's verification.
b7d42f9 · gates
gated
02/Ship the evidence, not just the code
Four gates stand between your C repo and the pull request. Each one either advances the port or stops everything with a printed reason.
- GATE Flat-scan refusal before any work runs. Subdirectories, build systems, non-C files → rejected with the exact reason, exit 2. No wasted compute on repos v0 can't handle honestly.
- PIN c2rust 0.20.0, containerized, immutable. Runner image lives on GHCR from one pinned Dockerfile. Upstream churn cannot silently change your output.
- VERIFY Output faces cargo clippy. Findings are captured into the report as evidence — never hidden, never fatal for generated code.
- PROOF REPORT.md rides inside the PR. Build status, clippy warning count, per-file unsafe-fn table. Reviewers read evidence first, diff second.
c91e0aa · artifact
03/The artifact reviewers actually read
Every PR carries this file. Generated from tool output on every run — never written by hand.
REPORT.md● verified artifact
# c2proof Verification Report
- Source: `tinyexpr`
- Tool: c2rust 0.20.0
- This is a mechanical translation.
It is NOT safe Rust and NOT reviewed code.
## Build: ✅ compiles (cargo clippy ran)
## Clippy warnings captured: 3
## Unsafe functions per file
| file | `unsafe fn` count |
|---------------|-------------------|
| `tinyexpr.rs` | 14 |
The stamp is the point. A reviewer opening the PR sees build truth and unsafe density before reading a single transpiled line.
d4f8b12 · label
not safe rust
The honesty label
Every port c2proof ships is mechanical translation, labeled as such everywhere it appears. It contains unsafe blocks — the report counts them per file. It is not reviewed code. It is not idiomatic Rust. No safe-Rust promise is made anywhere in this tool, its output, or its documentation.
That honesty is the product. A migration you can't trust is decoration; a migration with counted unsafe and captured warnings is a starting point you can act on.
f02c6d4 · diff
04/Where c2proof fits
Honest comparison, rendered the way engineers read changes.
--- manual rewrite · weeks of engineer time
+++ c2proof · one CI run
− translation coverage ……… human-limited
+ translation coverage ……… via pinned c2rust engine
− input validation ……………… implicit, tribal knowledge
+ flat-C gate ……………………… exit 2 + printed reason
− verification …………………… in reviewer's head
+ REPORT.md ……………………… committed inside the PR
− unattended runs …………… ✗ weeks of meetings
+ GitHub Action native …… ✓ zero-touch
! idiomatic reviewed Rust — mechanical only, both tools. Hire a rewrite if you need that today.
If you need hand-crafted idiomatic Rust today, hire a rewrite. If you need a starting port with evidence attached this afternoon, that's this tool.
1a9e77b · man
05/c2proof(1) — FAQ
Manual-page format. Questions a stranger actually asks.
SYNOPSIS
c2proof migrate <repo-url|path> [--fixture] [--work-dir DIR]
Is the generated Rust safe?
No. Mechanical c2rust translation containing unsafe blocks; the report counts them per file. Safe-Rust refactoring is a later, separate step.
What C projects are supported?
Flat directories of .c/.h files, no build system. Anything else → exit 2 with the exact reason. Makefile/cmake parsing is on the roadmap, not shipped.
Do I need Docker?
Only for real transpilation. --fixture replays a CI-generated golden fixture through the full pipeline offline.
EXIT CODES
0 pipeline completed (build may still be ❌ — read REPORT.md)
1 tooling failure (docker missing, GH API down)
2 refused — input outside v0 scope, reason printed
Which converter does it use?
c2rust, version-pinned at 0.20.0 inside an immutable GHCR image. The pin exists so upstream releases cannot silently change your migration output.
Can I trust the verification report?
Generated from cargo clippy and source scans every run — never hand-written. Limits labeled in-file: regex-level unsafe counting, no formal proofs.
8cc31d0 · trust
06/Verifiable, not promised
license MIT. Read it, fork it, audit it — LICENSE.
ci Every push runs fmt, clippy -D warnings, tests, cargo-audit, cargo-deny. Badge is live, not decorative.
pin c2rust 0.20.0 · rust stable · GHCR image digest-locked per build.
scope v0.1 targets flat C projects; tinyexpr is the CI-tested dogfood target. Refusals are documented behavior with exit codes.