Tenjin

Software written in C continues to underpin critical infrastructure, but such code is plagued by memory safety flaws—issues that major technology companies report account for the majority of their security problems. These flaws arise from C’s weak type system and permissive handling of memory through unchecked pointer operations. Attempts to mitigate these issues over the last two decades have failed to stem the tide of vulnerabilities. Recognizing this, the software engineering community and recent White House initiatives have converged on a more durable solution: shifting to safe programming languages like Rust. The DARPA TRACTOR program aims to make this transition feasible at scale by funding research that can automatically translate large C codebases into safe, idiomatic Rust.

Our project, Tenjin, contributes to this vision by building a deterministic translation framework that rewrites C into Rust while preserving the semantics of the original code and ensuring memory safety. Tenjin combines static analysis (via the CodeHawk abstract interpretation engine) and dynamic analysis (via the DIODE input synthesis system) to build a comprehensive semantic model of the source C code. This model captures ownership, lifetimes, aliasing relationships, and other properties essential for generating idiomatic and safe Rust. The translator is structured as a pipeline of modular stages—preprocessing, analysis, translation, improvement, and validation—designed for both automation and flexibility.

Key technical features include staged translation (separating the translation of type signatures from function bodies) and the translator's capacity to accept guidance (which may be provided by human developers or LLMs). Tenjin focuses on generating code that avoids Rust’s unsafe construct by construction. The system also includes a test generation component that builds high-coverage Rust test suites from dynamic input synthesis to support validation.

Tenjin is designed not just to produce correct code, but also maintainable software. By decoupling stages and giving primary consideration to program interfaces, the system enables maintainers to provide lightweight guidance, review transformations, and iteratively refine output. Improvements to idiomaticity—e.g., replacing ad-hoc C data structures with standard Rust collections—are performed in later stages, informed by both heuristic and learned rules. This architecture allows the system to benefit from advances in LLMs while remaining deterministic and auditable. The project’s final output will be an open-source toolchain designed to integrate with existing development workflows and support high-assurance migration from legacy C to modern, safe Rust.

Aarno Labs is collaborating with MIT CSAIL Professors Martin Rinard and Michael Carbin, who bring deep expertise in programming languages, formal methods, and machine learning.