Automating C to Safe Rust Translation

C has been the load-bearing language of systems software for five decades (kernels, drivers, hypervisors, network stacks, embedded firmware, cryptographic runtimes) precisely because it gives the programmer direct memory access, deterministic execution, and a transparent mapping to hardware instructions.

Those are the same properties that make manual memory management a standing invitation to get it wrong: buffer overflows, use-after-free, double frees, null dereferences, uninitialized reads, data races. Microsoft's own review of its CVE history landed on roughly the same number: about seven in ten of the severe vulnerabilities in its products traced back to a memory-safety bug, not a logic error.

Rust's pitch has always been that this is a solved problem, not an inherent cost of systems programming: an affine type system plus compile-time lifetime analysis and ownership/borrowing invariants gets you memory and thread safety with none of a garbage collector's runtime overhead or latency jitter. That pitch has been broadly accepted for years.

The problem was never persuading anyone Rust is safer — it's that manually rewriting the world's legacy C is intractable.

The Linux kernel alone runs tens of millions of lines; a manual port demands deep dual-language expertise, consumes years of engineering time, and risks silently changing behavior the original C relied on.

That's the gap DARPA's TRACTOR program exists to close. Opened under solicitation DARPA-SN-24-89 and run out of the Information Innovation Office by program manager Dan Wallach, TRACTOR states its own goal without much hedging:

"TRACTOR will strive to create the same quality and style that a skilled Rust developer would produce, thereby eliminating the entire class of memory safety security vulnerabilities in C programs." — DARPA

Its stated approach is explicitly hybrid: "novel combinations of software analysis, such as static analysis and dynamic analysis, and machine learning techniques like large language models" — the same neuro-symbolic split the rest of this post converges on independently. MIT Lincoln Laboratory runs test and evaluation for the program, publishing benchmarks and milestone results at ll.mit.edu on roughly a six-month cadence — Battery 01 and a Round 1 Evaluation Report are already out, and DARPA hasn't announced an end date.

Two of the funded teams have described their approach publicly. Aarno Labs' Tenjin, led by Benjamin Karel with MIT's Michael Carbin and Martin Rinard, pairs source-level refactoring with a multi-stage translation pipeline, using Aarno's existing CodeHawk and DIODE analysis platforms to mine semantic models out of the C source before generating Rust.

A six-researcher team led by Wisconsin–Madison's Somesh Jha, with collaborators at UIUC, Berkeley, and Edinburgh, took a $5M award for ForCLift (Formally-Verified Compositional Lifting of C to Rust), which pairs LLM synthesis with formal semantic models of both languages so each translation can be checked against a specification, not just tested against examples.

The graphic below maps the whole argument in one frame.

The technical question underneath the funding is narrower and harder than "translate the syntax" — it's synthesizing a safe, idiomatic Rust program that a compiler's borrow checker actually accepts, while preserving the exact behavior of code nobody fully remembers writing.

01 Two Ways to Fail

That's easiest to see by watching one specific translation fail, rather than by comparing two approaches in the abstract. Every pipeline surveyed below eventually runs into the same wall: a C function whose informal contract with its callers has no direct Rust equivalent, not because the syntax is hard to map, but because Rust's type system forces a decision C never asked anyone to make.

A Function Small Enough to See the Problem

Here's a C function nobody would think twice about:

void increment_both(int *a, int *b) {
    *a += 1;
    *b += 1;
}

Nothing about that signature raises a flag in C. It compiles, it's obviously correct, and C's aliasing rules let a caller pass the same address twice without complaint:

int x = 0;
increment_both(&x, &x);  // x == 2 — perfectly legal C

Now translate the signature the way a model reflexively reaching for "idiomatic Rust" would — two mutable references:

fn increment_both(a: &mut i32, b: &mut i32) {
    *a += 1;
    *b += 1;
}

Call it the same way the C caller above did, and the borrow checker stops the program before it runs:

error[E0499]: cannot borrow `x` as mutable more than once at a time
  |
  |     increment_both(&mut x, &mut x);
  |                     ------       ^^^^^^ second mutable borrow occurs here
  |                     |
  |                     first mutable borrow occurs here

That's not a translation bug a smarter prompt fixes; the two functions aren't equivalent. &mut i32, &mut i32 is Rust's way of asserting, at every call site in the program, that a and b never alias. C's version made no such promise. If even one caller anywhere in a million-line codebase relies on the aliased case (and systems code leans on this trick more than idiomatic code ever admits), the "obviously idiomatic" signature isn't idiomatic, it's wrong.

Rust's affine type system belongs to the same family for a reason: a linear type system turns an aliasing assumption C leaves entirely implicit into a compile-time proof obligation instead.

Getting it right means one of two relatively unattractive answers:

• Unsafe pointers. Keep the raw pointers and the aliasing possibility, wrapped in unsafe: what a mechanical transpiler does.
• Global analysis. Read every call site in the program, prove none of them ever alias a and b, and only then commit to &mut i32, &mut i32: what a whole-program interface-inference pass has to do. Staying sound means treating "can't prove it" the same as "it happens" whenever the proof falls short, which is exactly how these passes end up defaulting to costlier, more conservative types — the Rc<RefCell<T>> fallback &inator's own cost function is built to avoid, covered below — instead of the tightest type the program actually needs.

There is no third option that skips the proof. Multiply this one function by every pointer pair in a real codebase, and the shape of the problem this post is about comes into focus.

The difficulty isn't incidental; it's a structural mismatch between how the two languages model memory:

• C's semantic model is permissive and flat: untyped memory buffers, raw pointer arithmetic, unrestricted aliasing, implicit type coercions, manual lifecycle tracking.
• Safe Rust's semantic model is restrictive and statically checked: unique ownership, explicit borrowing lifetimes, the aliasing XOR mutability rule (&mut T vs. &T, never both at once), and strict RAII (Resource Acquisition Is Initialization) invariants. A resource's lifetime is tied to a single owning value, and releasing it (freeing memory, closing a file, unlocking a mutex) happens automatically and deterministically the instant that value goes out of scope, with no garbage collector and no manual free call to forget.

Historically, automated migration has split into two approaches that sit at opposite corners of that mismatch, trading one failure mode for the other.

Rule-Based Transpilation: Compilable, Still Unsafe

Tools like C2Rust parse the C AST (or an intermediate representation such as LLVM IR, or WebAssembly via rWasm) and map it deterministically onto equivalent Rust constructs. The output reliably compiles and is functionally equivalent to the source; that's the whole value proposition. But it inherits three problems from playing it mechanically safe:

• Pervasive unsafe blocks. Because the transpiler can't infer higher-level ownership intent, every C pointer becomes a raw Rust pointer (*const T, *mut T) wrapped in unsafe.
• Unidiomatic structure. The output keeps manual allocation calls (libc::malloc/free), global mutable state (static mut), and layout-preserving annotations (#[repr(C)]), bypassing Rust's standard-library abstractions entirely.
• Zero security improvement. The resulting codebase runs memory-unsafe C logic inside a Rust-syntactic envelope. It compiles with rustc. It inherits the exact vulnerability surface of the original.

Crown (Zhang et al.) attacks exactly that problem from inside the same rule-based paradigm: ownership-guided static analysis that reasons about pointer mutability and lifetime bounds to rewrite a subset of raw pointers into safe references and Box<T> as it translates. The gain is real but partial — the analysis proves what it can at file and module scope, and the rest of the pointer surface stays raw.

Direct LLM Translation: Idiomatic, Unreliably Correct

At the opposite end, an LLM trained on large open-source corpora can recognize common C idioms (a hand-rolled vector buffer, a linked list) and synthesize genuinely idiomatic equivalents: Vec<T>, Box<T>, Rc<T>, Option<T>, Result<T, E>.

Importantly, unguided, it fails for three structural reasons this blog has covered from other angles before:

• Borrow-checker failures. LLMs struggle to reason about whole-program lifetime graphs and mutability constraints across call chains, and routinely emit code that simply doesn't compile.
• Semantic drift. Edge-case semantics get altered, buffer lengths miscalculated, off-by-one errors introduced, error-handling paths quietly dropped: the same specification-gap problem that shows up in every domain where a model is guessing at intent rather than checking it.
• Decomposition limits. Real repositories have dependency graphs across dozens of files; prompting a model with a monolithic codebase degrades reasoning fidelity and truncates output before the job is done.

The frameworks below all make bets on how to close that gap: keep the LLM for synthesis, and put something deterministic in charge of deciding whether to believe it.

02 The Four Frameworks

The four frameworks divide along a line worth naming first. Three of them — C2SaferRust, SACTOR, and VERT — combine symbolic program analysis (AST parsing, IR manipulation, dataflow tracking) with LLM-driven synthesis inside an automated test-and-repair loop, and differ only in which part of the problem they push onto the symbolic side.

The fourth, &inator, runs no model in the loop at all: it solves for the interface's types up front and leaves the bodies to whoever translates them next.

C2SaferRust: Bridge First, Refine Bottom-Up

C2SaferRust (Nitin et al.) doesn't try to jump from C to safe Rust in one pass. It runs C2Rust first to get a compiling, unidiomatic-but-executable Rust codebase, an artifact that's wrong on idiom but right on semantics, and specifically useful as a working environment where safe and unsafe modules can interoperate without building foreign-function boundaries by hand.

From there it decomposes the codebase into translation units by walking the Rust compiler's own High-level IR (via rustc_hir::intravisit::Visitor) to build a global call graph, then analyzes the Mid-level IR for each unit (live-in variables, entry/exit basic blocks, dataflow dependencies) and packages each slice with its structural context into a targeted LLM prompt.

Because changing a callee's raw pointer to a safe reference changes its type signature, which propagates up the call chain, C2SaferRust refactors leaf functions first and works up the call graph in bottom-up topological order, so callers only ever consume already-verified safe interfaces.

Each candidate slice gets swapped back into the full codebase and run against the project's own end-to-end test suite. Failures (compiler borrow-checker traces, runtime assertion logs) get routed to a repair agent that synthesizes a follow-up prompt and iterates.

That last row's 100% pass rate over the modules that made it all the way through the pipeline unfortunately says nothing about how many didn't. We were unable to determine the completion rate across the full benchmark; only the correctness outcome conditioned on completion.

SACTOR: Prove the Interface First, Refine Idiom Second

SACTOR (Zhou et al.) decouples syntactic porting from safety refactoring into two explicit stages, specifically to avoid inheriting C2Rust's architectural artifacts wholesale.

1. Stage 1 — unidiomatic, interface-preserving. C functions get translated into unidiomatic Rust while strictly preserving the external ABI and parameter types (*const c_char, c_int, and so on). Because the interface stays bit-compatible with C, the translated function links straight back into the original C application via extern "C", and the original C test suite runs against the resulting mixed-language binary, establishing function-level semantic equivalence before any ownership transformation is even attempted.
2. Stage 2 — idiomatic safe refinement. Only once the unidiomatic version passes every functional test does SACTOR invoke refinement. A separate static-analysis tool, Crown, analyzes pointer mutability, "fatness" (array vs. single object), and lifetime bounds to guide the LLM toward idiomatic types (&str, slices, Box<T>) instead of leaving the choice to pattern-matching alone.

The two stages don't stay comparable once refinement changes function signatures, so SACTOR generates its own test harnesses rather than requiring a human to hand-rewrite them: Specification-Driven Harness Generation. The LLM co-produces the idiomatic implementation alongside a machine-readable JSON spec describing the mapping between legacy C types and the new Rust abstractions:

{
  "function": "concat_str",
  "legacy_signature": "const char* concat_str(const char* orig, int num)",
  "idiomatic_signature": "fn concat_str(orig: &str, num: i32) -> String",
  "mapping": [
    { "c_param": "orig", "rust_param": "orig", "rule": "const char* -> &str via CStr::from_ptr" },
    { "c_return": "const char*", "rust_return": "String", "rule": "caller owns a new heap allocation" }
  ]
}

SACTOR's own rule-based engine reads that SPEC to auto-generate dual-layer FFI bridge wrappers, code that marshals the legacy C harness's inputs into idiomatic Rust types, calls the safe function, and unmarshals the return value back into a C-compatible representation. The hybrid binary runs the original test suite one more time; failures map back to specific functions for another repair pass.

VERT: An Assembly-Level Oracle, Verified up to a Bound

VERT (Yang et al.), Verified Equivalent Rust Transpilation, takes the most formally ambitious approach of the four, and is the most explicit about where its guarantee stops.

VERT establishes ground truth by compiling the source C to WebAssembly and lifting the Wasm bytecode to Rust via rWasm. Because Wasm compilation and rWasm lifting are both deterministic, syntax-directed transformations, the resulting "assembly-like" Rust program (unreadable, but faithful) serves as a trusted reference oracle. In parallel, an LLM few-shot synthesizes a clean, idiomatic, human-readable candidate from the same source. Neither path trusts the other; both get checked against each other:

1. Type compilation (rustc). Rejects any candidate that violates Rust's ownership or borrowing rules outright.
2. Property-based testing (Bolero). Runs hundreds of thousands of pseudorandom inputs through both the oracle and the candidate, catching overt logic discrepancies fast and cheaply.
3. Bounded model checking (Kani). A bit-precise, SMT-based model checker that symbolically unrolls loop iterations and program paths up to a fixed bound k, proving the oracle and the candidate produce identical output for every possible input, within that unrolling bound.
4. Deductive verification (Verus). For the subset of code where it applies, proves algebraic loop invariants and formal specifications to establish equivalence without unrolling, i.e., without the bound k that step 3 depends on.

The oracle is deterministic but unreadable, the candidate readable but unverified, and only a candidate that survives all four checks against the oracle counts as verified.

When Kani or Bolero find a divergence, they hand back a concrete counterexample (a specific input that triggers the mismatch), which VERT embeds directly into the next repair prompt, letting the LLM fix the exact trace where it deviated from the oracle instead of guessing at what might be wrong.

&inator: Solve the Interface Globally First

&inator (Chen et al.) tackles a different angle entirely: not "is this function's body safe" but "what Rust type should this interface even have." In a modular C project, translating functions independently requires choosing correct, safe Rust types for every top-level interface (struct fields, globals, parameter and return types) before any function body can be written. Pick the wrong one, an immutable &T where an internal routine needs mutation, or a Box<T> where multiple aliased pointers reference the same object, and the function body becomes unimplementable in safe Rust without a runtime panic or an unsafe escape hatch.

&inator formulates that choice as an SMT constraint-satisfaction problem over a lattice of Rust Type Fragments (structs, Box<T>, Rc<T>, shared and exclusive references, each parameterized by a mutability qualifier μ and a lifetime/region variable ρ).

It processes the LLVM IR extracted from the C program and generates logical constraints over every memory access: if static alias analysis finds two pointers that may alias at the same program point, both can't be assigned exclusive &mut types; if a field is read through a shared reference but sometimes needs interior mutation, the type inference engine is forced to wrap it in RefCell<T>.

&inator optimizes an explicit cost function via the Z3 SMT solver, ranking candidate types from cheapest to most expensive:

Cost(&T)
        < Cost(&mut T)
                < Cost(Box<T>)
                        < Cost(Rc<T>)
                                < Cost(Rc<RefCell<T>>)

and picks the cheapest type that satisfies every safety constraint simultaneously. Solving that constraint system globally, upfront is the actual contribution: it produces a formally sound type skeleton for the whole interface before a single function body is translated, which means the modular per-function translation pass that follows (human or LLM) can proceed without a borrow-check failure surfacing three call sites from the bad type choice.

The paper is explicit that this doesn't scale yet: constraint-solving time grows superlinearly with program size, taking several hours to resolve C programs that span only a few thousand lines. The aliasing model is also conservative by design: &inator reasons about the C program's aliasing as written, not about semantics-preserving reorderings that might yield a tighter, more precise interface. Both are named in the paper as future work, not quietly hoped past.

The Field Keeps Moving

The four frameworks above aren't the only game in town, and the pace hasn't slowed since. Forcrat (Hong & Ryu, KAIST) is the most structurally interesting of the newer entries, because it removes the LLM entirely: a formally verified translator scoped to specific library boundaries (I/O APIs, unions) that proves correctness through programming-language theory rather than testing for it. The deterministic layer stands on its own — it just covers a narrower fragment of C than the model-driven pipelines attempt — and its Communications of the ACM writeup made the November 2025 cover.

Three more recent efforts push the same wager from other directions:

• DepTrans — a repository-scale pipeline that fine-tunes an LLM with reinforcement alignment against Rust's own syntax, reporting a 60.7% compilation success rate on real industrial C projects.
• EvoC2Rust — another repository-scale pipeline, skeleton-guided: translates project structure first, then fills in function bodies.
• Program Skeletons — the more general framework EvoC2Rust's "skeleton" idea traces to, demonstrated on Python-to-JavaScript rather than C-to-Rust, but built on the same wager: abstract away the language-specific details, translate the skeleton, then fill in verified fragments.

None of this changes the argument above; every one of them still leans on a deterministic layer to keep the LLM honest, but the roster of who's building that layer keeps growing.

03 Comparing the Approaches

Laid side by side against the two baselines, the trade-off each framework is actually making gets easier to see: what it optimizes, what it verifies, and at what granularity it scales. The chart below plots it for the six tools at this post's core — the higher up, the harder it is for a wrong translation to survive verification; the further right, the more the output reads like Rust a person would actually write.

The four neuro-symbolic pipelines all sit above and to the right of the two single-strategy baselines, and none of them reach the top-right corner. The table below spells out what sits behind each box:

Read the "granularity" column against the "safety guarantee" column and a pattern falls out: the strongest guarantees belong to the frameworks operating at the smallest scope. &inator's interface-level proofs are complete for interfaces; VERT's bounded equivalence is absolute within the bound and at function granularity. Nothing in this table claims a whole-program formal guarantee, because nothing here has one.

04 Recent Case Studies

Outside the four research frameworks above, eight recent efforts tackled the same problem. What separates them is less the architecture than who is doing the work, and how much judgment stays human. All six point events land between October 2025 and August 2026, while zlib-rs and Code Metal run as multi-year background efforts spanning the same period.

• Three push a single technique to unusual scale: Vasily Sartakov's Ship-of-Theseus methodology on a 12,500-line DNS tunnel, Mark Bacarella's file-by-file port of the 40,000-line OCaml runtime, and Jarred Sumner's nine-day agentic rewrite of Bun's million lines of Zig.
• Two research groups measure how little a person has to do: ACToR's adversarial loop across 57 utilities with nobody in the loop at all, and Reboot's six interpreters at one to eleven human touches apiece.
• Two are industry deployments: Google's production pilot on giflib, validated against 30 million real GIFs, and Code Metal, selling the same architecture as a product to aerospace and defense buyers.
• One is the control case: zlib-rs, hand-written over two years with no model anywhere in the pipeline.

The timeline below places all eight efforts on a single line.

Twelve Thousand Lines, One Piece at a Time

Vasily Sartakov's Ship-of-Theseus methodology, posted in July 2026, names the underlying pattern out loud: mature C systems can't be translated directly, because implicit layout assumptions, aliasing patterns, and undefined behavior have to be reconstructed before safe Rust can be produced at all.

Its answer is to generate a semantics-preserving but unidiomatic Rust baseline first, then have an agent incrementally rewrite it toward idiomatic Rust piece by piece, validating each swap against compilation and behavioral tests before moving to the next: the same unidiomatic-first, refine-second shape as SACTOR's two-stage pipeline (covered above), and the same per-piece testing discipline the OCaml vignette below used by hand.

Applied to iodine (a DNS-tunneling tool, 12,500 lines of C), the paper frames the result as a methodological claim more than a benchmark score: reliable C-to-Rust migration is a structured transformation workflow, not a single translation step.

This is a smaller, more modest case study than the two efforts that follow (one project, one author, no leaderboard), but it's evidence the shape of the answer holds even off the beaten path of libogg and GNU CoreUtils benchmarks.

Forty Thousand Lines, Two Thousand Unsafe Blocks

In June 2026, developer Mark Bacarella described directing Claude Code through a file-by-file, line-by-line translation of the entire OCaml runtime (roughly 40,000 lines across 71 files), with a per-file build toggle that ran the same upstream test suite against either the C or the Rust implementation after every single conversion.

The runtime confirmed the increment_both lesson at industrial scale. OCaml represents every value as an untyped machine word, a tagged integer or a heap pointer distinguished by stealing the low bit, so in the author's own words "every field access is a raw pointer deref. The borrow checker can't work with that." The finished translation carries roughly 2,015 unsafe blocks, not a failure of the process but the same honest admission this post already made about C2Rust's own output: some C patterns simply have no safe Rust equivalent.

Two costs showed up that none of the frameworks above report a number for. Losing GCC's computed-goto extension slowed the bytecode interpreter by 44% on stable Rust, clawed back to actually faster than C (0.91x) only on a nightly branch using explicit tail calls. And three low-level mechanisms (thread-local storage, variadic functions, weak-symbol ephemeron initialization) needed hand-written inline assembly, because stable Rust has no other way to express them at all.

The whole effort passed OCaml's own compiler test suite, a fixpoint self-build check, and ThreadSanitizer, and took about a week of wall-clock time, most of it spent waiting on test runs.

A Million Lines, Nine Days, and 13,000 Unsafe Blocks

The OCaml runtime is what this discipline looks like applied patiently, one file at a time, for a week. An earlier experiment ran at roughly twenty-five times the scale and a fraction of the wall-clock time: not a C codebase, this time, but Zig, wired through the same low-level, pointer-heavy memory model and the same bet that an LLM can handle the mechanical part.

In May 2026, Bun creator Jarred Sumner merged a rewrite of the entire JavaScript runtime from Zig to Rust: 1,009,257 lines added across 6,755 commits in a single PR, from an effort that took nine days. That is the size of the change, not of the result: once the leftover Zig was removed, Bun's Rust tree settled at roughly 681,000 lines.

The process was explicitly agentic rather than human-directed line by line: Claude coding agents worked from the full Zig codebase in a four-phase pipeline, generating Rust in parallel, feeding compiler errors back through iterative correction loops, and checking the result against the existing test suite, from over 16,000 initial compiler errors down to a 99.8% test pass rate.

Sumner was candid about how it got there: "We haven't been typing code ourselves for many months now."

What those numbers don't describe is idiomatic safety. The port carries more than 13,000 unsafe blocks; for comparison, uv, a hand-written Rust tool roughly half the size, has 73. That's not a rounding difference; it's evidence the translation optimized for compiling and passing tests, not for the ownership design a human choosing between &mut and Rc<RefCell<T>> would have made along the way.

A follow-up cleanup PR — more than 600,000 lines of leftover Zig deleted — was self-labeled "ai slop" by its own author, and GitHub's own bot flagged and auto-closed it. Speed and safety traded off the way this post's opening example predicts: nobody proved the aliasing claims a decade of Zig callers relied on, so the fallback was raw pointers wrapped in unsafe, at a scale two orders of magnitude past what a comparable hand-written codebase needed.

Fifty-Seven Programs, Zero Humans in the Loop

The three efforts above all have a person somewhere in the loop, steering, reviewing, or at minimum picking the project. ACToR removes that entirely by pitting two LLM agents against each other instead: a translator (Claude Sonnet 4.5) proposes Rust, and a discriminator hunts for an input where the C original and the Rust candidate actually disagree, using differential fuzzing to find one rather than reading the code and guessing.

The loop runs to a fixed budget rather than until convergence: ten iterations by default, with the discriminator generating roughly three new adversarial tests each round for the translator to reconcile against. Every candidate also has to clear a harder bar than "compiles": no unsafe blocks are permitted at all, so both agents are fighting inside the same safe-Rust-only constraint the rest of this post treats as non-negotiable.

On its macro benchmark (57 real-world command-line utilities, 63 programs counting the six-program micro set, averaging 473 lines each), ACToR reaches a 95.1% relative pass rate, 36.7 points ahead of a coverage-driven baseline running the same model. Swap in the older Sonnet 4 and the gap holds: 93.9% against 75.0%, winning on 55 of the 57 programs. The paper presents the same numbers as a bar chart; this is the same data, laid out as a table.

The discriminator is still an LLM, but the thing it's actually trusted for isn't its opinion; it's the counterexample it hands back once the fuzzer finds one. The real ground truth in the loop is the same as everywhere else in this post: an executable oracle, not a model's judgment call.

None of that comes free. The paper's own accounting for its smaller six-program benchmark puts the bill at roughly $201 and 411 million tokens, real money and real compute spent on a process that, by design, has nobody watching it run.

Six Interpreters, One to Eleven Human Touches

A research line spanning NUS and CMU, from the same lineage as ACToR just above, pushes on a related angle: Reboot targets a narrower but harder class of program (interpreters, not generic utilities), translating six real ones (6,000 to 23,000 lines of C) to safe Rust with as few as one to eleven human interactions per project, by decomposing the work into testable milestones and running a multi-agent loop with automated validation and feedback.

It hit 100% pass rates on each project's own test suite and 62–92% on held-out validation tests, eliminating the heap buffer overflows and use-after-free bugs the original C carried.

The table below breaks that down per interpreter. Reboot's paper has real per-project tables to draw from (Wang et al., arXiv:2606.27122, Tables 2–4), unlike ACToR's bar-chart-only presentation above, so these are the same underlying numbers rather than a replica of the paper's own layout. ("+n" in the intervention column counts minor recovery actions, not full interventions; all six interpreters reach 100% pass on their own provided test suites regardless of the validation-set spread shown.)

Read the intervention column against the validation column and no pattern holds: Wren needed the most interventions among the four mid-sized cases (8) and still posted the best validation score (91.78%), while pocketpy took the most touches overall (11 + 1) and posted the worst (61.58%). More human involvement didn't reliably buy a better result.

Three Thousand Lines, One CVE That Missed Its Target

The five efforts above are all research artifacts: a paper, a personal write-up, a merged PR nobody's paid to maintain. In August 2026, Google published the same bet made inside a production security team, on giflib, Eric S. Raymond's widely used GIF-decoding library, roughly 3,000 lines with no SIMD or inline assembly, a stable and unglamorous codebase chosen precisely because it was tractable, translated with Gemini.

The pipeline ran in three passes: a one-shot full-codebase translation first (small enough to make that feasible in a way it wouldn't be for a million-line runtime), then iterative repair of the FFI boundary specifically, because a memory-safe drop-in replacement still has to expose a C-compatible ABI to every existing caller, which reintroduces exactly the raw-pointer lifecycle bookkeeping at the core of the translation problem. Engineers Bastian Kersting and Max Hils single that step out in their own write-up: "replacing a C library with Rust does not immediately eliminate all unsafe code."

Trust came from validation scale, not from the translation step. The rewrite ran against more than 30 million real-world GIFs with byte-identical output, then a differential fuzzer exercised the original C and the new Rust side by side for six days straight, 200 million iterations without finding a single behavioral divergence. The validation work caught more than translation bugs: it surfaced a pre-existing out-of-bounds write that had been sitting latent in a Google-internal patch to the original C source, until the cross-check exposed it.

The performance worry that usually follows a safety pitch, that bounds checks aren't free, didn't materialize either: monitoring across Google's global image-processing services found the Rust implementation performance-neutral against the original C. Dropping the C library's memory-unsafe status even let some services retire the sandboxing they'd previously needed around it, a latency win that had nothing to do with Rust's runtime and everything to do with no longer needing a containment boundary at all.

Eight Customers, and a Published Benchmark

Most of the work above is research or a one-off port. Code Metal sells the same architecture as a product: static analysis segments a repository into verifiable components, the pipeline generates a test suite with functional and MC/DC coverage, translation is gated on functional equivalence, and verification scales from differential and property-based testing up to formal proof where the code admits it.

Their research line sharpens the same split — LLMLift pairs LLM translation with proof generation to establish equivalence — and the customer list is the one you would want if the claim were hollow: Boeing, Bosch, Toshiba, L3Harris, Raytheon, Collins Aerospace, NVIDIA and the U.S. Air Force, with legacy defense code moved to memory-safe Rust as the stated use case.

The paper's sharper claim is predictive, not just descriptive. Combine three features that individually stump a model into one program, and the same model fails the combined program too: every model with a zero success rate on any constituent feature also scores zero on the combined program, and every model that clears all three also clears the combination. That's preliminary evidence for exactly the kind of feature-level gating Code Metal's own commercial pipeline already does — though it's evidence about raw LLM behavior, not a pass rate for their own product, which still isn't published. The architecture is still left doing most of the persuading: the model proposes, and a deterministic layer that cannot be talked into agreeing disposes. That is the same bet every pipeline in this post makes, here with a sales team and, now, a benchmark paper behind it.

Two Years, 3,000 Adopters, and Not One Line from an LLM

Google's own write-up points to a complementary case it didn't build: zlib-rs, a fully hand-written, memory-safe reimplementation of zlib maintained by the Trifecta Tech Foundation, with no LLM anywhere in its pipeline. It's the control case this section otherwise lacks: proof that the destination, a memory-safe, ABI-compatible, drop-in C replacement, doesn't require an LLM to reach, only that reaching it by hand takes longer.

Initial development, funded by Prossimo and built largely by Tweede golf as an in-kind contribution, began in 2024; an ISRG security audit and an early integration into the Rust flate2 crate followed the same year.

By early 2025 decompression had moved past parity into a real lead, by the team's own benchmarks: over 10% faster than zlib-ng at 1KB inputs, over 6% faster at 65KB, and a smaller edge over Chromium's own fork at the chunk sizes that matter in practice.

Compression told a less one-sided story: faster than zlib-ng at the default level (about 6%) and at maximum compression (over 13%), but still a bit slower across several levels in between. Adoption followed anyway: 3,000+ projects and, as of its January 2026 stable release, 30 million downloads.

The clearest sign of trust earned rather than claimed: as of version 151.0.0, Firefox uses zlib-rs for gzip decompression in production, a two-year path from Mozilla's first conversations with the team in summer 2024 to a shipped release. That's the same timescale the OCaml runtime rewrite compressed into a single week and Bun compressed into nine days; zlib-rs spent it instead on the audit, the benchmark parity, and the incremental trust-building an LLM-driven pipeline is explicitly trying to buy back with differential testing.

05 Limitations

The most useful part of the papers above isn't the benchmark numbers; it's their limitations sections, where the research is candid about where the whole approach still breaks.

Several categories of ordinary C code stubbornly resist all four pipelines above, not because of an implementation gap but because of a mismatch between what the pattern needs and what safe Rust's type system is built to express, plus one problem that's different in kind: even when translation succeeds, the safety guarantee handed back can still defer part of the check to runtime.

Intrusive Data Structures and Macro Layouts

C systems code leans hard on intrusive containers (the Linux kernel's struct list_head is the canonical example), where a list node is embedded directly inside its parent struct, and address-calculation macros like container_of or offsetof walk back from the embedded field to the enclosing object.

Mapping that to safe Rust means restructuring the ownership model entirely: arena indices (store every node in one big preallocated array and pass around integer offsets instead of pointers), generational indices (the same arena scheme plus a generation counter per slot, so reusing a freed slot doesn't let a stale index silently point at the wrong node), or reference-counted nodes (Rc<RefCell<T>>, paying for shared mutable ownership at runtime instead of encoding it in the type). Each is a real, working substitute; none of them is a mechanical rewrite of the original pointer.

Unchecked Pointer Arithmetic and Sentinel Iteration

Idiomatic C walks arrays and buffers by incrementing a raw pointer until it hits a sentinel value (a null-terminated string's trailing \0 being the obvious case). Safe Rust wants slices (&[T]) bounded by an explicit runtime length. Converting sentinel iteration into slice indexing requires whole-program analysis to guarantee buffer bounds, trace length provenance across distant variables, and rule out an out-of-bounds panic during dynamic slicing.

That requirement isn't pedantic: a sentinel-terminated buffer's length isn't stored anywhere in C, it's whatever a scan happens to find at runtime. Recovering it as an explicit, checkable number means tracing where the buffer came from and how far it's actually guaranteed to extend, through every function call and struct field it passes through before the point where a slice gets built. It's the same class of whole-program provenance problem &inator's SMT solver tackles for pointer aliasing and mutability, just aimed at lengths instead of ownership.

Unrestricted Graph Topologies and Cyclic References

C handles doubly linked lists, cyclic ASTs, and parent-pointer tree nodes through unrestricted raw-pointer aliasing. Safe Rust's ownership model wants a strict directed acyclic graph. Resolving an actually cyclic structure in safe Rust means introducing Rc<RefCell<T>> wrappers, Weak<T> back-pointers, or a flat arena allocator (a typed arena, a slotmap), each option trading off runtime performance, memory footprint, and API ergonomics differently, and none of them a mechanical substitution for the original pointer.

One of the earlier research pipelines made this trade-off for real rather than just describing it. Reboot's mujs translation replaced a hand-written mark-and-sweep garbage collector with plain Rc<RefCell<T>> reference counting, eliminating an entire class of GC-algorithm bug in the process (including a real CVE) but at the explicit cost of never collecting a reference cycle again. The paper calls that an acceptable trade when a slow leak beats a use-after-free; it's exactly the trade-off described above, just made with a real interpreter and a real CVE on the other side of the ledger.

Polymorphic Pointers and Variadic Functions

C relies on void* for ad-hoc polymorphism and generic containers. Safe Rust wants generic type parameters, trait objects (dyn Trait), or an enum closing over the concrete cases.

Automatically determining the exact closed set of concrete types ever passed through a given void* across an entire codebase requires whole-program points-to analysis, and that analysis fails outright in the presence of dynamic library loading or runtime function-pointer dispatch, which is to say: in a nontrivial fraction of real systems code. &inator's own authors list function pointers, union types, and the ternary operator alongside void* as C features their current implementation only partially supports.

Callback Hell at the FFI Boundary

A related, more visceral version of the same problem shows up in production driver code rather than a benchmark suite. NVIDIA's DOCA SDK, the toolkit for programming its BlueField data-processing units, exposes much of its I/O surface the way C libraries have for decades: register a function pointer plus an opaque void* context, and the library calls back into it later, on its own schedule, from wherever it happens to be in its own control flow.

The difficulty isn't the function signature; a callback typed as void (*)(void*, int) maps mechanically enough onto a Rust function pointer. It's everything the type system can't see from that signature alone: which thread the callback fires on, how long the context pointer has to stay valid, whether the library ever calls back reentrantly while the caller's own code is still on the stack.

A Rust JP talk on wrapping DOCA describes the fix as a hand-built, runtime-agnostic wrapper that decouples the caller's program logic from the callback's C-shaped control flow entirely, rather than trying to make the callback itself look idiomatic. It's the increment_both lesson again, one level up: some C interfaces can't be typed honestly in Rust without redesigning the interface around them, and no pipeline surveyed here claims to do that redesign automatically.

Dynamic Borrow Panics and Reference Cycles

A global type-inference pass like &inator's resolves a static aliasing conflict by reaching for RefCell<T>, but that only moves the check; it doesn't remove it. RefCell enforces Rust's borrowing rule (shared XOR mutable) at runtime instead of compile time, so a genuinely conflicting pair of borrows that the static analysis missed, or a legitimately dynamic access pattern the type system can't express statically, surfaces later as a panic instead of a compile error.

Rc<T> carries a parallel problem: a reference cycle keeps every node's count above zero forever, which is a memory leak Rust's ownership model does not prevent by construction. Cycles are exactly the case reference counting was never designed to catch. &inator's own paper names both as open follow-up work.

Proving that an inferred interface can't produce a dynamic borrow panic, and proving it can't leak memory through a reference cycle, are stated goals, not shipped guarantees.

06 What Humans Do Differently

Automated pipelines are one way to do this work. The limitations above are about where they stop.

The Human Baseline

Every framework above is graded against a test suite. The closest thing to an outside baseline in this post is a controlled study of humans doing the same job by hand.

Li et al.'s study had 33 participants translate 8 C benchmarks by hand; 31 produced finished translations that were fully safe Rust (zero unsafe, all three known benchmark vulnerabilities eliminated), against tools that leave an average 95.3% of data references as unsafe raw pointers (Laertes) or lift under 3.1% of references into safe Rust (Crown).

Safe, Not Correct

The table below breaks down how the humans achieved that, by reference type (Li et al., arXiv:2411.14174, Table III). ("Static" means enforced by the type system at compile time, with the remainder in each cell caught by a runtime check instead; owning and borrowing sum to 100% of all references, while nullable references and dynamically-sized types are reported separately in the paper and omitted here for clarity.)

The table reads two ways at once. Temporal safety, whether a reference still points at live memory, is settled statically in nearly every category (95–100%), so the check costs nothing at runtime. Spatial safety, whether an access stays inside the object, is settled statically in almost none of them (0–21%), so the bounds check survives into the compiled binary where C's unchecked pointer arithmetic used to be.

The single exception cuts the other way: global references are the only category where static temporal safety itself collapses, to 45.9%, because a compiler can't always prove a global's lifetime the way it can prove a stack slot's or a heap allocation's.

But safe isn't the same claim as correct: across those same 31 translations, an average of 68% of fuzz tests still turned up a discrepancy from the original C, clustered on the same handful of tests per benchmark rather than scattered randomly. A shared misunderstanding, not independent mistakes.

The humans won on safety, against every automated tool. They lost on correctness, against the C they started from.

What the Study Says About the Tools

The same participants weren't sold on the machines helping, either: 31 of the 33 tried LLMs for assistance, 20 of those 31 called the generated code error-prone and hard to debug, and two abandoned LLMs outright and translated from scratch.

The paper's own recommendations for where tools should go next read like a preview of where the field is already heading: model Rust's standard-library types and APIs beyond Box and Option, run type analysis before lifting references rather than after, and support incremental translation (a partially-translated Rust codebase coexisting with the untranslated C around it) instead of demanding a whole-program pass. That last one is the same bet Sartakov's Ship-of-Theseus and SACTOR's two-stage refinement are already making.

What Practitioners Report

That's the research picture. Practitioners describe a messier, slower version of the same problem: not a batch job over a whole repository, but an incremental rewrite that has to ship new features while it replaces the foundation underneath them — the version Luca Palmieri and Vitaly Bragilevsky walk through for teams migrating live C and C++ systems.

Most of the approaches above aren't built for that constraint: their module-by-module discipline assumes a codebase that can sit still long enough to be translated. The exceptions are the ones that never leave the C application behind — SACTOR's first stage links each translated function straight back into it, and Ship-of-Theseus generates a compiling baseline first, then refines it piece by piece.

A consultancy's own account of a live migration adds a cost none of the sources above put a number on: teaching the humans. Mainmatter's write-up of a client engagement (client and product both anonymized) describes decomposing a mature C search-engine codebase into leaf-first modules for a wave-by-wave, no-LLM replacement, backed by CI, linting, and Miri sanitizer runs on every wave — the same incremental discipline as Ship-of-Theseus, minus the model.

But most of the write-up is about the client's engineers, who started with little Rust experience: training workshops, pair-review sessions, ongoing mentoring. It reports no pass rate, no unsafe-block count, no timeline; "key modules have already been ported and released" is the only outcome given, so it's evidence of a shape rather than a result.

07 Conclusions

Three architectural principles fall out of comparing all six tools side by side, and they generalize past C-to-Rust specifically:

1. Rule-based transpilation is a correctness baseline, not a security outcome. It buys compilability and semantic fidelity; it does not buy safety, and was never designed to.
2. Pure LLM generation buys idiomatic output at the cost of reliability — borrow-checker failures, hallucination, and semantic drift that only a symbolic layer reliably catches.
3. Neuro-symbolic hybrids (static analysis, IR slicing, and test-driven or SMT-driven verification wrapped around whatever generates the code) — plus &inator, which skips the model entirely and solves for the interface up front — are the only approaches among the six with a credible path to scale. All four back that claim with real benchmarks rather than a launch announcement, with one caveat the architecture doesn't fix on its own: &inator's global solve takes hours on programs of a few thousand lines, and its own paper names scaling as open work.

That third point is the same argument this blog has made about AI-generated code and about code porting more broadly: the LLM is never the thing doing the trusting.

C2SaferRust trusts a differential test suite. SACTOR trusts an FFI-linked harness against the original C tests. VERT trusts a deterministically-compiled Wasm oracle and a bounded SMT proof. &inator trusts a global Z3 satisfiability solve. In every case, the deterministic layer, not the model, is the thing actually load-bearing enough to ship on.

What that argument doesn't stretch to cover is the ground the limitations section above lays out, or the human baseline in the section just before this one: the parts of a legacy C codebase most likely to be load-bearing, and gnarliest to review by hand, are also the parts most likely to still need a human, or an unsafe escape hatch, at the end of an automated pass.

As reasoning-capable LLMs keep improving and static analysis keeps getting integrated more tightly into the repair loop, automated C-to-Rust migration is a credible bet to move from research pipelines into production developer tooling. Intrusive data structures, sentinel-terminated buffers, cyclic graphs, void* polymorphism, and C-style callbacks at the FFI boundary are the open half of that bet.

Until a paper claims otherwise with a benchmark to back it, "verified C-to-Rust translation" should be read as verified for the code the pipeline accepted, not for the codebase as a whole.

References

• Nitin, V., Krishna, R., do Valle, L. L., & Ray, B. (2026). "C2SaferRust: Transforming C Projects Into Safer Rust With NeuroSymbolic Techniques." IEEE Transactions on Software Engineering, 52(2), 618–630. Available at: computer.org
• Zhou, T., Zhang, Z., Lin, H., Jha, S., Christodorescu, M., Levchenko, K., & Chandrasekaran, V. (2025). "SACTOR: LLM-Driven Correct and Idiomatic C to Rust Translation with Static Analysis and FFI-Based Verification." Available at: arxiv.org
• Yang, A. Z. H., Takashima, Y., Paulsen, B., Dodds, J., & Kroening, D. (2024). "VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners." arXiv preprint; presented at ASE 2025. Available at: arxiv.org
• Chen, V., Coughlin, A., & Bond, M. D. (2026). "&inator: Correct, Precise C-to-Rust Interface Translation." ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Available at: arxiv.org

• Hong, J., & Ryu, S. (2025, November). "Automatically Translating C to Rust." Communications of the ACM, 68(11), 58–65. Available at: cacm.acm.org
• Hong, J., & Ryu, S. (2025). "Forcrat: Automatic I/O API Translation from C to Rust via Origin and Capability Analysis." Proceedings of the 40th IEEE/ACM International Conference on Automated Software Engineering (ASE), 1541–1552. Available at: arxiv.org
• Feng, J., Gan, W., Gao, C., Wang, C., Luo, F., Xia, X., Li, G., & Liu, K. (2026). "Dependency-Guided Repository-Level C-to-Rust Translation with Reinforcement Alignment." Available at: arxiv.org
• Sartakov, V. A. (2026). "From C to Idiomatic Rust: A Ship-of-Theseus Agentic Translation." Available at: arxiv.org
• Wang, C., Yu, T., Shen, B., Wang, J., Chen, D., Zhang, W., Shi, Y., Xie, C., & Gu, X. (2026). "EvoC2Rust: A Skeleton-Guided Framework for Project-Level C-to-Rust Translation." Proceedings of the IEEE/ACM 48th International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), 94–105. Available at: dl.acm.org
• Wang, B., Li, T., Li, R., Mathur, U., & Saxena, P. (2025). "Program Skeletons for Automated Program Translation." Available at: arxiv.org
• Wang, B., Paulsen, B., Dodds, J., Kroening, D., Mathur, U., & Saxena, P. (2026). "Mostly Automatic Translation of Language Interpreters from C to Safe Rust." Available at: arxiv.org
• Li, T., Li, R., Wang, B., Paulsen, B., Mathur, U., & Saxena, P. (2025). "Adversarial Agent Collaboration for Correctness Improvements of C to Safe Rust Translation." Available at: arxiv.org
• Li, R., Wang, B., Li, T., Saxena, P., & Kundu, A. (2024). "Translating C To Rust: Lessons from a User Study." Available at: arxiv.org

• Wallach, D. (2024). "Translating All C to Rust (TRACTOR)." Defense Advanced Research Projects Agency (DARPA), Information Innovation Office. Available at: darpa.mil
• MIT Lincoln Laboratory (2025). "Translating All C To Rust (TRACTOR) Benchmarks." Cyber Security and Information Sciences, Secure Resilient Systems and Technology Group. Available at: ll.mit.edu
• Aarno Labs (2025). "Aarno Labs Awarded DARPA Grant to Develop Tools for Translating C to Safe Rust." Available at: aarno-labs.com
• Coordinated Science Laboratory, University of Illinois (2025, July 15). "Translating Legacy Code for a Safer Future: DARPA Backs Effort to Convert C to Rust." Available at: csl.illinois.edu
• Immunant, Inc. (2020). C2Rust. Available at: github.com
• Microsoft (2019). "A Proactive Approach to More Secure Code." Microsoft Security Response Center. Available at: msrc.microsoft.com
• Zhang, H., David, C., Yu, Y., & Wang, M. (2023). "Ownership Guided C to Rust Translation." Available at: arxiv.org
• Emre, M., Boyland, P., Parekh, A., Schroeder, R., Dewey, K., & Hardekopf, B. (2023). "Aliasing Limits on Translating C to Safe Rust." Proceedings of the ACM on Programming Languages, 7(OOPSLA1), 551–579. Available at: doi.org

• Bacarella, M. (2026, June 10). "A Line-by-Line Translation of the OCaml Runtime from C to Rust." OCaml Discuss. Available at: discuss.ocaml.org
• Sumner, J. (2026, May 14). "Rewrite Bun in Rust." GitHub, oven-sh/bun, Pull Request #30412. Available at: github.com
• ByteIota (2026). "Bun Rust Rewrite Merged: The 13,000 Unsafe Block Problem." Available at: byteiota.com
• Rust JP (2024, December 24). "Overcoming Callback Hell When Integrating C into Rust." Available at: youtube.com
• Bragilevsky, V., & Palmieri, L. (2026, July). "How Do You Rewrite C/C++ Projects to Rust?" JetBrains. Available at: youtube.com
• Kersting, B., & Hils, M. (2026, August 24). "Scaling Memory Safety: AI-Assisted Rewrites of C/C++ Dependencies to Rust." Google Bug Hunters Blog. Available at: bughunters.google.com
• Trifecta Tech Foundation (n.d.). "zlib-rs." Available at: trifectatech.org
• de Vries, F. (2025, February 25). "zlib-rs Is Faster Than C." Trifecta Tech Foundation Blog. Available at: trifectatech.org
• Code Metal (n.d.). "Code Metal Research." Available at: codemetal.ai/research
• Code Metal (2025). "Verified Code Transpilation with LLMs" (LLMLift). Code Metal Research. Available at: codemetal.ai/research
• Code Metal (2026). "AI-Generated Code That Works — and Proves It." Code Metal Research. Available at: codemetal.ai/research
• Kellison, A. E., Titolo, L., Basumallick, A., Hasabnis, N., Hunter, C., Ladden, C., & Yotam, T. (2026). "Can Feature-Level Tests Predict LLM-Based C-to-Rust Translation Reliability?" Code Metal. Available at: github.com
• Mainmatter (n.d.). "Modernizing a Database with Rust: Safe, Fast, Future-Ready." Available at: mainmatter.com