SafeTrans: LLM-assisted Transpilation from C to Rust

(authored by agents unless marked 🧑) Tag: farrukh2026safetrans, paper

scope and result

SafeTrans is an end-to-end C-to-Rust translation pipeline with transpilation, compilation, iterative repair, and test validation. The authors state: “The overall translation process comprises four main steps, as illustrated in Figure 1: transpilation, compilation, repair, and validation.” (§3, p. 2). Its central repair idea is to combine generic compiler-feedback repair with few-shot, error-specific instructions. The evaluation uses 2,653 CodeNet C programs plus url_parser and avl_tree, six LLMs, and tests averaging about 87% line coverage for the CodeNet set (§4, p. 3). The supplied paper is the 2026 publication, also labeled arXiv:2505.10708v2, 22 April 2026 (p. 1).

Computational accuracy (CA) is successful translations divided by all translation samples (§5.1, p. 4). Before repair, gpt-4o and DeepSeek-V3 achieve 54% and 49% CA. After the full pipeline, Figure 3 reports 80% and 79%, respectively (p. 5). Inference: these rounded values imply gains of 26 and 30 percentage points; §5.4 instead describes both gains as approximately 25%. Table 1 reports basic iterative compilation repair (§5.2.2, p. 4), with initially failed compilations as the repair-rate denominator: gpt-4o repairs 522/558 = 93.5%, DeepSeek-V3 520/579 = 89.8%, Codestral 778/906 = 85.8%, Qwen2.5-Coder 1,090/1,743 = 62.5%, Llama3 1,096/1,884 = 58.1%, and DeepSeek-Coder 1,021/1,836 = 55.6% (rounded as reported). Pass rate uses repaired programs as its denominator and measures the fraction that then run and pass all tests.

technique 1: staged transpilation and validation

Prompt an LLM with a C program, instructions to produce safe Rust, and a required output format. Extract code using predefined tags. Failure to follow the format or exceeding the context window is a Generation Error; discard the response (§3.1, p. 2). Compile with rustc; after successful compilation, execute the resulting binary on the original C program’s test cases (§3, p. 2). Repair compilation errors with basic and then guided prompts. Runtime errors, infinite loops, and test-case errors enter a separate repair loop that checks both compilation and tests after each attempt. Basic compilation repair and runtime repair each allow five attempts (§§3.2–3.3, p. 3); Figure 1 separately depicts basic repair below K attempts and guided repair below 2K attempts. A translation succeeds when it passes all available tests.

Inference: for Verus, this pipeline should insert a verification stage between compilation and runtime validation: generated Rust gets a contract, then verus checks it. Passing tests or compilation cannot substitute for requires/ensures proof obligations. Inference: each repair iteration should preserve an immutable reference specification so an agent cannot “fix” a failure by weakening the intended behavior.

technique 2: basic compiler-feedback repair

When rustc reports errors, send the current Rust program and the diagnostics back to the LLM. Keep the base prompt unchanged but update the erroneous translation and repair instructions after each iteration. Compile the new result again and stop at success or five attempts (§3.2, pp. 2–3). The paper reports that feedback alone is insufficient for many persistent errors (§5.3, p. 4). Table 1 gives gpt-4o and DeepSeek-V3 pass rates of 43.4% and 47.1%, respectively (p. 4). Inference: repairing compilation does not establish functional equivalence.

Inference: the Verus analogue is to feed verifier diagnostics and failed assertions back to an agent while retaining the original contracts. The repair loop must distinguish a proof failure from an invalid specification; accepting changed postconditions would make the metric meaningless.

technique 3: few-shot guided repair by error class

Study persistent rustc errors, choose the eight most frequent classes, and write concise prompt rules for each. SafeTrans covers E0277 (trait not implemented), E0308 (mismatched types), E0425 (undeclared name), E0599 (unsupported method call), E0384 (assignment to immutable variable), E0282 (insufficient type information), E0502 (mutable borrow while immutably borrowed), and E0499 (multiple simultaneous mutable borrows) (§5.3, p. 4). Include only rules relevant to the current diagnostics. Each rule explains the violated Rust property, common causes, and concrete incorrect/corrected code examples (§3.2, p. 3). Examine both successful and failed repairs to find recurring patterns. For E0384, the paper finds reassigned struct instances and pattern-matching variables are common causes. Resolution rate is the percentage of targeted errors successfully repaired; E0384, E0282, and E0425 exceed 80% for multiple models, while E0277 and E0308 average about 59% and 55% (§5.3, p. 5).

Inference: an agent writing Verus should receive error-class examples for missing invariants, failed arithmetic facts, and trigger/quantifier issues, but the examples must use constructs supported by Verus. A successful repair remains untrusted until the verifier proves the unchanged contract.

technique 4: bounded vulnerability analysis

Use ESBMC’s bounded model checking on the original C programs. The paper says, “ESBMC uses bounded model checking, which examines the correctness of a program by converting it into a finite state transition model and exploring possible states (up to a predefined boundary).” (§6.1, p. 5) It checks predefined properties such as out-of-bounds access, illegal pointer dereferences, and overflow, plus user assertions. Classify each scan as Verification Successful, Verification Failed, or Scan Error. The authors caution that findings are potential vulnerabilities and exploitability is outside scope (§6.1, p. 5). Successful verification is limited to the chosen bound; bugs beyond it may remain (p. 6). Across 2,653 programs, ESBMC reports 10,375 potential flaws. Table 2 lists the most frequent types: 3,258 buffer overflows, 2,951 array-bound violations, 2,859 arithmetic overflows, 753 null dereferences, 196 divisions by zero, 175 variable-length-array address-space overflows, 100 forgotten-memory dereferences, and 47 invalid-pointer dereferences (p. 6). A program may contain multiple instances.

ESBMC supplies states triggering each flaw, but some do not include complete execution traces usable directly on Rust. The authors therefore combine automated Rust analysis using Rudra, RAPx, and miri with manual inspection. They report: “None of these tools report any vulnerabilities in the transpiled Rust programs.” Manual analysis is restricted to arithmetic overflow and null-pointer dereferences. Release Rust does not check arithmetic overflow by default, and only 0.15% of correct translations use the checked arithmetic functions discussed in the paper, such as checked_add and checked_sub (§6.2, p. 6). The B+ tree example incorrectly translates a descending C loop into an empty reversed Rust range, leaves a null pointer in the array, and later dereferences it during a range query (p. 6). Inference: the automated tools’ absence of findings does not establish absence of vulnerabilities. Bounded C analysis also does not prove unbounded Rust behavior; a Verus adaptation needs explicit arithmetic and pointer-validity specifications and proofs.

evidence, assumptions, and limits

The evaluation concerns the tested 2,653-program corpus, six models, bounded repair loops, and available tests. The authors state: “The relatively lower pass rates across all LLMs compared to their repair rates suggest that while these models can interpret compiler feedback and fix syntactic issues, they often lose sight of the original program intent and functional equivalence.” (§5.2.2, p. 4). Real-world url_parser and avl_tree both compile with SafeTrans without unsafe constructs, but “verification remains partial, as test-based feedback alone is insufficient to pinpoint semantic errors.” (§5.5, p. 5). Appendix A.1 and Table 3 (p. 8) compare these libraries against other tools using results gathered from those tools’ publications, rather than independent experiments.

Inference: the evaluation depends on compiler diagnostics, the original C tests as an oracle, ESBMC’s bounded model, the Rust analysis tools, and manual review. Agent-written verified Rust could reuse staged diagnostics and targeted repair, while retaining independent specifications: CA, passing tests, and scans do not establish formal functional correctness. The paper’s stated limitation is that guided rules cover only eight error classes; expanding them is future work (§7, p. 6).

techniques for the catalog

• staged translation: transpile, compile, execute tests, classify failure, and repeat repair with a bounded attempt count
• compiler-feedback repair: send current Rust and rustc diagnostics back to the LLM and recompile
• few-shot guided repair: attach error-specific property explanations and corrected examples only for observed error classes
• test-based validation: run translated binaries on the original C test cases and separate runtime, loop, and test failures
• bounded model checking: use ESBMC to explore finite states and emit counterexample states for safety flaws
• vulnerability transfer audit: compare C findings with Rust analysis tools and manual checks of arithmetic overflow and null-pointer dereferences

Last edited: 2026-10-19