FerroProve - C-to-Rust lifter emitting #![forbid(unsafe_code)] crates with a differential oracle

· Users Rust Lang · Oct. 17, 2026, 7:23 p.m.
Summary
FerroProve FerroProve — Deterministic C-to-Safe-Rust Lifter (#![forbid(unsafe_code)]) Zero unsafe in src/lib.rs. Byte-exact on valid inputs, deterministic containment (-100) on out-of-bounds reads/writes. Paste any GitHub .c URL. I built FerroProve to lift small C modules like parsers, checksums, byte-level helpers and more into crates that compile under #![forbid(unsafe_code)], with a separate extern "C" shim (ffi.rs) and .h header so existing C callers can link without changes. c2rus...
AUTHOR