A Bristol PhD asks the question the C-to-Rust debate keeps skipping: how do you know the translation is right?

A three-year University of Bristol PhD is asking the question the C-to-Rust conversation keeps skipping: not how to translate C into Rust, but how to know the translation is right.

Canonical, the company behind Ubuntu, and UK Research and Innovation (UKRI) are funding a single-PhD project led by Professor Meng Wang of Bristol to investigate whether machine translation of entire code repositories can be verified rigorously enough to ship. Jon Seager will co-supervise alongside Dr. Cristina David. PhD student Alex Wood will run the work, which is set to start later in 2026, according to Seager's announcement on his personal blog.

The bet is on verification. Existing source-to-source translators tend to keep the structure of the C input too literally, often surfacing as Rust that still relies on the language's unsafe escape hatch. Large language models produce code that looks idiomatic to a Rust reviewer, but Seager's framing is blunt: "plausible-looking output is not evidence that the translated program behaves like its source." Both InfoWorld's writeup and LinuxIAC's summary carry the same critique.

The proposed system, called "neurosymbolic" by Seager because it pairs a learned translator with conventional program analysis, is organised in four stages. Scheduling breaks a repository into chunks and attaches the type, dependency, and behaviour context each chunk needs to be translated in place. Translation runs an LLM trained on a known C-to-Rust corpus. Validation tests the output with fuzz testing and checks it for formal equivalence against the original C. Debugging and repair iterates when the validators disagree with the translator.

Validation is where the research bet lives. Fuzz testing throws randomised inputs at the translated program and compares behaviour against the C original. Formal equivalence checking tries to prove, mathematically, that the two programs produce the same outputs for the same inputs. Neither is cheap, and both are harder to scale to hundreds of thousands of lines of interdependent C than to a single function. If the Bristol project can show that a chunked, context-aware pipeline makes those checks tractable at repository scale, the practical cost of moving a legacy codebase to memory-safe Rust drops. If it cannot, the field learns that the verification step is the actual ceiling on automated migration, not the translation step.

The case studies the project starts from are not toy programs. AppArmor is the Linux kernel's mandatory access-control framework; snap-confine is the sandbox wrapper that mediates what snap applications on Ubuntu can and cannot do. Both ship in Ubuntu, both are written in C, and both sit on the security boundary between the operating system and the applications it runs. Translating them well matters because memory-safety bugs in code at that layer are how attackers escape sandboxes and escalate privileges.

This is a three-year PhD with one student and two supervisors, not a shipping timeline. The strongest objection is one Seager himself flags: semantic equivalence at repository scale may be practically undecidable for real-world C, and no amount of clever scheduling will change that. The project's contribution is funding the work of finding out, with a public-facing blog to read as it goes.

Watch item: Wood's first public artefact, whenever it appears, will be the first measurable signal of whether the four-stage pipeline holds together on AppArmor or has to be redrawn.