Beyond Transpilation: Software Recreation and the Correctness-Efficiency Paradox

Every enterprise with a mainframe has the same conversation eventually: the COBOL still runs, the people who understand it are retiring, and rewriting it by hand is a multi-year, eight-figure project nobody wants to own. Large language models, per Chen et al.'s foundational work training them on code at trillion-token scale, have made a real dent in that calculus — not by getting faster at the old approach, but by replacing it with a different one entirely. What follows is a walk through the architecture that replacement actually requires, and the specific ways its own benchmarks say it can quietly go wrong.

01 From Transpilers to Generative Recreation

Modern enterprise infrastructure sits on geological strata of engineering history. Banking systems process trillions of dollars a day through COBOL routines compiled decades ago; telecom switches run on millions of lines of C and C++ nobody fully maps anymore; scientific computing depends on FORTRAN libraries whose original authors have long since retired. None of that code survives because it's optimal — it survives because the cost, risk, and cognitive load of rewriting it are prohibitive.

Software architects have a name for the tax that imposes: the polyglot tax, and it has three faces. Architectural drift — decades of patches diverge from any original design document, until implicit assumptions about endianness, word size, and compiler-specific undefined behavior become load-bearing structure nobody wrote down. Talent attrition — the supply of engineers fluent in COBOL-85, obscure assembly dialects, or MUMPS shrinks every year modern stacks evolve faster. And compounding technical debt — bridging old and new systems via FFI, serialization shims, and RPC layers is a second full-time maintenance job stacked on the first.

Why Deterministic Transpilers Stall

The traditional answer was a deterministic, rule-based source-to-source compiler — a transpiler like C2Rust, cxgo, or Java2CSharp — parsing source into an AST, applying handcrafted transformation rules, and emitting a target AST. That pipeline guarantees syntactic validity and gives you a rigorous paper trail, and it fails in three specific ways that have nothing to do with engineering effort.

Writing the rules requires full semantic modeling of both languages, including every place their memory models and runtime primitives quietly disagree — a combinatorial problem that gets worse, not better, as the language pair gets more distant. What comes out the other side translates syntax, not intent: C2Rust wraps every legacy pointer in an unsafe block, producing Rust that compiles but keeps every manual-memory-management footgun the borrow checker exists to remove. And some gaps simply can't be closed by one-to-one AST mapping at all — there's no deterministic rule that turns Node.js's event loop into legacy Java's thread-pooled blocking I/O, because the two aren't expressing the same execution model in different syntax.

Naïve Translation vs. Software Recreation

LLMs change the shape of the problem because they perform probabilistic semantic mapping instead of static rule-rewriting — recognizing design patterns, inferring intent, and synthesizing idiomatic target constructs rather than looking up a transformation rule, an approach that traces back to Roziere et al.'s early unsupervised program-translation work. That capability gets used two very differently, though, and the distinction is worth being precise about — starting with something as unglamorous as how the request gets phrased: Aljagthami et al. found translation quality moves measurably just from prompt language and prompt design, holding the model itself fixed.

Naïve code translation maps an isolated snippet, function, or file from language A to language B with no holistic awareness of project architecture, object lifecycles, or cross-file dependencies — which is exactly the mode that produces the runtime inefficiencies covered below. Software recreation is the end-to-end alternative: analyze the whole system's topology, extract the business logic actually implemented (not just described), map implicit state machines, refactor monoliths into decoupled modules, synthesize comprehensive test harnesses, and verify semantic equivalence with formal methods and differential runtime execution before anything reaches a human reviewer.

02 Building the Pipeline: Semantic Graphs and Topological Slicing

Feeding an entire codebase into an LLM's context window doesn't work — context saturates, the model loses track of what's in the middle, and cross-file references start getting hallucinated. Every serious recreation system solves this the same way: build a graph of the system's actual semantics first, and query it for exactly the slice a given translation step needs.

The Enriched Semantic Program Graph

Industrial pipelines construct what's usually called an Enriched Semantic Program Graph (ESPG), unifying four representations that are normally kept separate: the Abstract Syntax Tree (structural decomposition of declarations and expressions), the Control Flow Graph (every possible execution path through basic blocks), the Program Dependence Graph (data-dependency arcs tracking variable definition-use chains across statements), and the Call Graph (inter-procedural invocation hierarchies across functions, classes, and module boundaries). Querying that unified graph, rather than the raw source, is what lets the synthesis engine extract a self-contained semantic slice — the target AST, its full data-dependency chain, and the type signatures of everything it calls — and pack that into a bounded, relevant prompt instead of the whole repository.

Slicing a Repository So It Compiles in Order

Method-level translation is one problem; class- and repository-level translation is a meaningfully harder one, and benchmarks built specifically to isolate that jump — Du et al.'s class-level evaluation and Xue et al.'s ClassEval-T among them — are specific about where it breaks. LLMs lose track of field shadowing and state mutation across instance methods, struggle to translate polymorphism and dynamic dispatch into a target idiom (a Java interface becoming a Rust trait isn't a mechanical rename), and introduce naming drift — declaring a snake_case field and then calling a camelCase accessor for it in the same class.

The fix is ordering: build a dependency graph of the whole repository, collapse it into strongly connected components with Tarjan's algorithm, and process components in topological order — leaf nodes (data models, utility functions, primitive types) get translated, compiled, and verified first, so that by the time a higher-order module is processed, its dependencies' verified interfaces and type signatures can be injected directly into the prompt instead of guessed at.

import ast
import networkx as nx

class SystemDependencySlicer:
    def __init__(self, entrypoint_files: list[str]):
        self.call_graph = nx.DiGraph()
        self.entrypoints = entrypoint_files

    def parse_module(self, file_path: str, source: str) -> None:
        for node in ast.walk(ast.parse(source)):
            if isinstance(node, ast.FunctionDef):
                self._record_function(file_path, node)

    def _record_function(self, file_path: str, node: ast.FunctionDef) -> None:
        qualified = f"{file_path}::{node.name}"
        self.call_graph.add_node(qualified, ast=node)
        for sub in ast.walk(node):
            if isinstance(sub, ast.Call) and isinstance(sub.func, ast.Name):
                self.call_graph.add_edge(qualified, sub.func.id, relation="calls")

    def get_execution_order(self) -> list[str]:
        # leaves first — compile-safe order, or Tarjan SCCs for recursive cycles
        try:
            return list(nx.topological_sort(self.call_graph))
        except nx.NetworkXUnfeasible:
            sccs = list(nx.strongly_connected_components(self.call_graph))
            return [n for scc in sccs for n in scc]

The Tree of Code Translation

Some language pairs are too far apart for a single hop. Migrating dynamically-typed Python straight to borrow-checked Rust, or COBOL straight to async TypeScript, asks a model to resolve type inference, ownership semantics, and idiomatic syntax in one pass — and the literature's answer is to not ask it to.

Macedo et al.'s InterTrans is the clearest statement of that answer: the Tree of Code Translation (ToCT) framework routes through intermediate pivot languages, resolving one conceptual gap per hop: a type discovery phase (Python → Java/C# forces dynamic typing into explicit nominal types), a lifetime planning phase (Java → modern C++ exposes explicit lifecycles and pointer semantics), and a final concretion phase (modern C++ → safe Rust turns RAII patterns into ownership and borrow mechanics).

03 The Correctness-Efficiency Paradox

Here's the failure mode standard testing doesn't catch, made concrete — the same category Pan et al. catalogued in their study of bugs LLMs introduce while translating code. Source C++ does an O(1) hash-map lookup inside a loop over a stream. The LLM-translated Python drops the hash map and checks membership with if x in list_of_keys instead — syntactically clean, and semantically identical on every unit test, because a linear scan and a hash lookup return the same answer for the same input. They just don't take the same amount of time.

A transformation like that preserves functional equivalence while quietly degrading computational complexity, and it's invisible to any test suite built around small, hand-picked inputs — which describes most test suites, hand-written or LLM-generated alike.

TRACE: Passing Tests Isn't the Same as Fast

The TRACE benchmark (Gong et al.) puts a number on how often this happens: 357 hand-curated problems expanded into 1,000 efficiency-critical translation tasks across six translation directions spanning C++, Java, and Python, run against 28 LLMs and stress-tested with production-scale inputs rather than the small vectors standard benchmarks like HumanEval and the original Transcoder-Test use.

Three findings from TRACE are worth carrying forward. First, a correctness-efficiency inversion: the model with the best pass rate isn't the model with the best time score, because reasoning-heavy models reach for defensive checks, dynamic unboxing, and extra abstraction layers that guarantee the test passes at the cost of runtime speed.

Second, the gap is common, not an outlier case — 23.5% of functionally correct translations exceed a 2x slowdown threshold. Third, and the one that should worry anyone relying on small test inputs: moving from toy-sized inputs to production-scale stress tests amplifies execution time by a median of 8.9x and peak memory by 3.4x on TRACE's own curated tasks — and by 84.6x and 78.6x respectively on the original, unfiltered Transcoder-Test suite. A translation can look fully functional right up until someone runs it at scale.

A Taxonomy of Generative Inefficiencies

The regressions aren't random — they cluster into three structural domains, and TRACE's own error analysis puts a rough split on how common each one is. Algorithmic-level discrepancy (11.9% of inefficiency cases): an O(N) scan becomes an O(N²) nested loop through an accidental re-traversal, or a manual sort-based maximum lookup gets carried over from Python instead of reaching for C++'s std::max_element.

Language construct mismatches (66.4%, the dominant category): Java's HashMap maps to C++'s std::map — an O(log N) red-black tree — instead of the O(1) std::unordered_map; string joins become iterative += inside a loop, turning linear-time work into O(N²) memory reallocation. Resource mismanagement (21.7%): C++ primitive vectors become Java Vector<Integer>, boxing every element and triggering GC pressure the source never had; a source relying on fixed 64-bit overflow behavior gets translated into an arbitrary-precision BigInteger nobody asked for.

04 The Legacy-to-Modern Asymmetry

Empirical studies of translation direction find something that isn't obvious in advance: modernizing legacy code is meaningfully easier for an LLM than generating legacy code from a modern source, and the gap is large. COBOL and TypeScript targets translated from COBOL land somewhere around 65–80% pass rates; the reverse direction — modern code translated into COBOL — scores 10.37% on the COBOLEval benchmark.

The asymmetry has a structural explanation on both sides. Legacy targets like COBOL and FORTRAN enforce rigid physical structures — strict column positions, fixed data-division layouts, explicit memory offsets — that models have comparatively little training data to draw on. Going the other direction is hard in a different way: the model has to extract implicit procedural business logic buried in decades-old code and lift it into an object-oriented or modular target without silently changing an edge case nobody documented.

A COBOL Case Study: Packed Decimals and REDEFINES

Take a small, representative COBOL program: a working-storage record WS-BALANCE-DATA stores a raw 20-byte field, REDEFINES it as a parsed structure — an 8-digit account ID, a signed packed-decimal principal, and a one-character risk flag — and applies a rate adjustment based on that flag.

Translating that snippet to Java forces three structural decisions a mechanical transpiler can't make correctly. Packed decimal conversion: COBOL's COMP-3 stores numeric fields as binary-coded decimal nibbles specifically to guarantee decimal precision; a direct translation to double introduces IEEE-754 precision loss that would fail a financial audit, so the target has to use BigDecimal with an explicit rounding mode instead. Memory aliasing: REDEFINES overlays multiple struct interpretations on the same byte buffer — a naïve translation to isolated Java fields breaks the implicit coupling where mutating the raw record is supposed to update the parsed view automatically.

Static state mechanics round out the three: COBOL working storage is stateful and global by default, and an honest modernization has to refactor that into encapsulated, immutable domain objects rather than preserving the mutation-in-place pattern.

public final class AccountRiskProcessor {

    private static final BigDecimal HIGH_RISK_MULTIPLIER = new BigDecimal("1.085");
    private static final BigDecimal MEDIUM_RISK_MULTIPLIER = new BigDecimal("1.045");

    public record AccountBalance(String accountId, BigDecimal principal, RiskTier riskTier) {
        public AccountBalance {
            Objects.requireNonNull(accountId, "accountId must not be null");
        }
    }

    public enum RiskTier {
        HIGH, MEDIUM, LOW;

        public static RiskTier fromFlag(char flag) {
            return switch (flag) {
                case 'H' -> HIGH;
                case 'M' -> MEDIUM;
                default -> LOW;
            };
        }
    }

    public static AccountBalance applyRiskAdjustment(final AccountBalance account) {
        BigDecimal multiplier = switch (account.riskTier()) {
            case HIGH -> HIGH_RISK_MULTIPLIER;
            case MEDIUM -> MEDIUM_RISK_MULTIPLIER;
            case LOW -> BigDecimal.ONE;
        };
        BigDecimal updated = account.principal()
            .multiply(multiplier)
            .setScale(2, RoundingMode.HALF_EVEN);
        return new AccountBalance(account.accountId(), updated, account.riskTier());
    }
}

C to Safe Rust

The C-to-Rust direction is a different flavor of demanding, because Rust's affine type system and borrow checker won't accept a syntactically-plausible translation the way Java will — Eniser et al.'s study of translating real-world C to Rust is the fullest account of exactly where that rejection happens.

05 Verifying What Actually Got Built

None of the correctness-efficiency paradox's or the legacy-asymmetry's failure modes show up in a lexical diff. Verifying a recreated system means answering a harder question than "does this look right": does it behave identically, on every input that matters, including the ones nobody thought to write a test for.

The Fallacy of BLEU and Exact Match

Näumann et al. put a name on this problem — "beyond BLEU" — that's worth borrowing directly. Early code-translation research borrowed evaluation metrics from machine translation — BLEU, METEOR, CodeBLEU — that score lexical n-gram overlap against a reference implementation. They're close to useless here, and the failure mode is stark enough to make the point in one example.

Lexical overlap and semantic correctness aren't just uncorrelated here — they point in opposite directions. Verifying software recreation has to mean runtime execution and formal proof, not string similarity.

Differential Fuzzing as an Equivalence Oracle

The dynamic half of that verification is differential fuzzing: generate an input, run it against both the legacy and recreated executables, and compare exit states — return values, stdout/stderr, mutation-state hashes, and execution time — rather than comparing source text. A divergence in output is a functional bug; a divergence in execution time past some threshold is exactly the kind of performance regression the correctness-efficiency paradox describes, and it's the same loop that catches both.

Differential Symbolic Execution: Proving It, Not Just Testing It

Fuzzing explores discrete concrete inputs; Differential Symbolic Execution (DSE) evaluates every execution path at once — represent input parameters as symbolic variables, run a source symbolic engine and a target symbolic engine in parallel, and hand both sets of accumulated path constraints to an SMT solver. The solver is asked to prove that for every guard condition satisfied by both implementations, the two return values are equal.

If the negation of that claim is unsatisfiable, the two implementations are mathematically identical across all edge cases — not "identical on the inputs we tried," identical, full stop. If it's satisfiable, the solver hands back the exact input that breaks the equivalence, which feeds directly into the LLM repair loop instead of a human going spelunking for it.

Where This Already Ships

None of this is purely academic scaffolding, though the honest version of that claim has a gap in it. RustAssure (Bai & Palit, 2025) is the closest real instance of DSE applied to LLM-transpiled C-to-Rust code, and it's upfront about not yet closing the loop all the way: rather than pairing two separate engines, it compiles both the C and the Rust to a shared LLVM IR and symbolically executes both sides with a single KLEE instance. Across five real-world applications and libraries:

• 89.8% of C functions produced compilable Rust
• 69.9% of those showed equivalent symbolic return values
• "Equivalent" here means a graph edit-distance comparison between return-value expressions, not an SMT-proved UNSAT — the authors list SMT-based strict equivalence as their own next step, not something the tool does today

The idealized diagram above is where this is headed; RustAssure is how far a working version has actually gotten. LLMLift — Bhatia, Qiu, Hasabnis, Seshia, and Cheung, out of UC Berkeley — runs closer to the full picture in a different corner of the same problem: an LLM translates source code (C, C++, Java) into a Python-encoded intermediate representation built from the target DSL's own operators, generates loop invariants for anything that isn't straight-line code, and hands both to an SMT-LIB solver to prove equivalence before a syntax-driven pass emits the real target code.

Across four DSL domains — MapReduce, switchISA, TensIR, and the tensor-algebra target TACO — the results held up against the tools it replaced:

• 138 of 138 test programs transpiled, against 40/45 for the prior symbolic tool Metalift on Java-to-MapReduce and 57/60 for C2TACO on C++-to-TACO
• Up to 20x faster than those prior symbolic tools
• Zero hand-written search-space tuning, against roughly a thousand lines of it for its predecessors

The company built around that research, Code Metal, backs it with real capital and a real defense customer:

• $125 million Series B, closed February 2026, at a $1.25 billion valuation
• $80 million agreement, signed August 2026, to bring the pipeline to the U.S. Air Force's WarMatrix platform
• L3Harris named as a customer for the same code-acceleration work

The grand challenge at the top of this post already has real capital and real defense-procurement money behind one version of the answer.

Code Metal's own writing is candid about where that proof stops mattering:

Their own illustration is the 737 MAX: the original MCAS system read a single angle-of-attack sensor, and any code built to that specification could have been formally verified against it without catching the flaw — the spec itself was the problem. The fix, after the grounding, wasn't a better proof of the old system; it was a redesigned one that compares both sensors and suppresses activation when they disagree. Every DSE proof in this post inherits the same caveat — UNSAT proves the two RetVal functions agree, not that either one was the function anyone actually wanted.

Code Metal's own writing traces that problem to its root, and the root has a name this post has already used in a different context: what happens when an LLM writes both the code and the specification it's checked against.

That's the same failure mode the open-questions section raised about training signals for efficiency, showing up one layer up, in the proof itself rather than the code it's proving.

Translation — this post's actual subject — sidesteps that specific failure by construction, and it's worth stating plainly why: "the source program becomes the specification," and "the source program is the ground truth, by definition." There's no LLM-generated spec to distrust, because the thing being proved equivalent to the target is whatever the legacy system already, verifiably, does. It's a real reason software recreation is a safer application of AI-plus-proof than asking a model to write both new code and the spec that new code has to satisfy.

Their verification stack is layered the same way this post's pipeline is, for the same reason: testing catches the obvious errors cheaply, lightweight methods — bounded model checking, symbolic execution, static analysis — eliminate large error classes before anything expensive runs, and full proof only engages on what's left. And a second Code Metal post makes the case for why any of this is worth the cost at all, reaching for Dijkstra's old line that "program testing can be used to show the presence of bugs, but never to show their absence" — precisely the gap a fuzzer alone leaves open. Their own framing of the trade:

"AI scales generation; formal methods scale trust."

Two precedents for what that bar actually looks like when someone pays for it, both proved years before LLMs existed: the seL4 microkernel and the CompCert verified C compiler.

They're candid, too, about how far that market actually reaches today — not "verify all AI-generated code," but a specific list with "large budgets, high failure costs, and clear notions of success" already attached: software modernization, language translation, compiler correctness, protocol compliance, security properties, hardware migration, safety-critical systems. And they don't pretend the skills gap closes just because the tooling exists: "most programmers are not trained to state formal properties, reason about invariants, or understand what a verifier has and has not proved." Coding agents democratized writing code. Nothing has democratized checking the proof yet — which is exactly why this post keeps a human at the end of the pipeline instead of just at the start of it.

Mutation Testing Catches the Harness That's Lying to You

There's a failure mode underneath both of the above: test harness overfitting, where translated code passes an existing suite simply because the suite never exercised the boundary state that would have caught the bug. Mutation testing checks the checker — inject deliberate synthetic faults into the legacy codebase (flip + to -, < to <=, invert a boolean, delete a statement) and run the translated code's test harness against each mutant.

A killed mutant means the harness caught the divergence; a survived mutant means the harness has a blind spot at exactly that execution path, and the pipeline should be synthesizing a targeted test for it before anything ships — not after. Mutation score is simply killed / total mutants × 100%, and it's a much better proxy for "is this actually tested" than raw line coverage ever was.

06 Technical Debt in the Wild

Everything above is about the moment of translation. Recreated code still has to survive a production lifecycle, and the largest study of what that looks like in practice is sobering in a specific way — not because AI-generated code is bad, but because of exactly which category of bad it is.

What 302,600 AI-Authored Commits Look Like Six Months Later

A large-scale empirical study (Liu et al.) tracked 302.6k verified AI-authored commits across 6,299 production repositories using differential, commit-level static analysis.

22.7% of that debt persists all the way through to the repository's current HEAD revision rather than getting cleaned up later. The maintainability smells that dominate the table are ordinary and mostly harmless in isolation — bare except: pass handlers, unclosed file descriptors, missing encoding parameters, unreferenced locals, high cyclomatic complexity — and the pattern holds regardless of which tool wrote the commit: across GitHub Copilot, Cursor, Claude Code, and Devin, issue-introduction rates land in a steady 17.4–29.1% band of all commits. This isn't one vendor's model behaving badly; it's a property of the category.

The Security Asymmetry

The one number in this study that should change how a team reviews AI-generated diffs: AI-assisted commits introduce roughly 1.5 times more security vulnerabilities than they remediate. That's not because generative models are careless across the board — the same study finds a net positive reduction of 7,069 code smells, meaning the tools are genuinely good at simple maintainability cleanup. They just struggle specifically with security invariants that only make sense in cross-file, cross-context terms.

All three compile cleanly, pass a functional test, and look plausible in a code review — which is exactly the problem the next section is about.

Automation Bias and Review Burnout

Because AI-generated code reads as syntactically fluent, human reviewers exhibit automation bias — treating plausible-looking code as probably-correct code and reviewing it more shallowly than they would a colleague's diff. That compounds three ways over time, and each one feeds the next.

Codebase expansion is where it starts: a model asked to add a feature frequently emits verbose boilerplate instead of wiring into an internal shared library, because reusing an undocumented helper is harder for the model than restating the logic inline. Every such commit grows the surface a reviewer must hold in their head, and it does so without adding any capability the system didn't already have.

Context fragmentation is the second-order effect: those redundant reimplementations of the same utility now proliferate across files, each a slightly different fork. Reviewing one no longer reviews all of them, and a defect fixed in a copy here remains latent in the cousin there — which is precisely the kind of drift that a human skimming a fluent diff won't catch.

Review burnout closes the loop. Reviewers facing large, AI-generated, fluent diffs eventually stop reading them at full depth, and the edge-case correctness and security issues from the previous section are exactly what slips through first, because they're the least visible in a shallow skim. None of this is a reason to stop using the tools — it's the reason the pipeline in the next section can't leave verification to a human reviewing a diff.

07 An Enterprise Pipeline, Sketched

Put the semantic-graph slicing, the paradox, the asymmetry, the verification machinery, and the production-debt findings together and the shape of a real recreation pipeline falls out — not a single LLM call with a good prompt, but seven stages, most of them deterministic and none of them optional. Zhang et al. describe a version of this shape already validated end to end, on whole projects rather than isolated snippets.

Three Agents, Not One Prompt

Splitting the orchestrator into specialized roles beats one large prompt for the same reason a monolithic language-model agent underperforms a harnessed one elsewhere in this literature: each agent gets a narrow, checkable job instead of an open-ended one.

The Modernization Agent ingests the source AST, dependency context, and target architectural constraints, and synthesizes idiomatic target code — prioritizing memory safety and standard-library idioms, explicitly instructed to avoid unidiomatic wrappers like C2Rust's blanket unsafe blocks. The Test Harness Agent ingests source specs, control-flow invariants, and data boundaries, and generates high-coverage parameterized tests plus edge-case fuzzing harnesses — the same pairing of translation and test generation Yang et al.'s UniTrans argues belongs in one system rather than two — targeting exactly the boundary conditions the verification section covers: null and uninitialized states, numeric extremes, off-by-one and empty-collection cases, concurrency races.

The Compiler/Repair Agent intercepts compiler diagnostics, linter flags, and SMT counterexamples, and generates precise AST-diff patches — not a full rewrite — that resolve the failure without regressing components already verified.

class IterativeCompilationEngine:
    def __init__(self, target_compiler: str, max_healing_rounds: int = 5):
        self.compiler = target_compiler
        self.max_rounds = max_healing_rounds

    def compile_target(self, file_path: str) -> tuple[bool, str]:
        result = subprocess.run([self.compiler, "--check", file_path],
                                stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True)
        return (result.returncode == 0, result.stderr)

    def execute_self_repair_loop(self, file_path: str, llm_repair_client) -> bool:
        for attempt in range(self.max_rounds):
            success, diagnostics = self.compile_target(file_path)
            if success:
                return True

            with open(file_path, "r") as f:
                current_code = f.read()

            repair_prompt = f"""Code failed to compile with '{self.compiler}'.
            [COMPILER DIAGNOSTIC OUTPUT] {diagnostics}
            [SOURCE CODE] {current_code}
            Fix all compilation errors. Return ONLY compilable target code."""

            repaired = llm_repair_client.generate(repair_prompt)
            with open(file_path, "w") as f:
                f.write(repaired)
        return False

Where Humans Still Sign Off

Automation handles the bulk translation and the formal verification; humans stay in the loop at specific decision points, and the point of the pipeline is to change what a reviewer is looking at, not remove the reviewer. The shape of that division of labor matters as much as the tools themselves.

Automated pre-flight is what a human never sees unless it fails: a 100% build pass across the target toolchain, a proven SMT equivalence or differential-fuzz proof, and zero critical static-analysis findings, all gating the change before review even opens. Passing those gates is the price of entering the human step at all — the pipeline deliberately absorbs the low-signal, machine-checkable work so the review a person actually does can be short and high-density.

Enriched PR generation is what makes that short review possible. Instead of a raw diff, the reviewer gets a side-by-side AST behavioral diff — the semantic change, not the textual churn — with architectural migrations flagged explicitly (global state moving into a DI container, say) and the formal-verification proof certificate attached. The reviewer no longer reverse-engineers intent out of a hundred changed lines; intent is presented, and the remaining job is judgment.

Human reviewer focus narrows to the parts the machinery can't decide: validating business-logic intent, checking integration boundaries against operational reality, and signing off on the trade-offs a solver has no vocabulary for. That is the version of the old line-by-line review where a human actually adds value — the syntactically-plausible pass is now the part a solver already did, and what's left is judgment about whether the code does what the business needed, not whether it looks like code.

What This Looks Like Inside Google

That division of labor isn't just this post's idealized sketch. Ziftci et al. published Google's own account of an LLM-assisted migration at production scale, and while it's a narrower kind of change than the cross-language recreation this post has mostly been about, the pipeline shape and the discipline around it are close cousins. The migration itself was mundane and specific: Google's protocol-buffer IDs were 32-bit integers, and enough product surfaces were approaching 2,147,483,647 — the paper's own framing is "running out of IDs for new toys" — that widening them to 64-bit became an active, sustained migration project spanning Java, C++, Python, and Dart, touching both direct accessors like getToyId() and indirect references reachable only by tracing data flow.

The verification pipeline they built runs five stages deep before a change is submittable: an AST parse check that the file is still syntactically valid, the LLM itself asked whether a given change is actually necessary, a full build to catch compilation errors, the existing regression suite, and then — with nothing skipped, no matter how clean the first four stages looked — a developer visually inspecting every single changed file. That last gate is the part worth sitting with: this is Google, running an LLM-assisted pipeline at scale, and the answer to "can we skip human review once the automated gates are green" was still no.

Over twelve months and three engineers, the numbers were concrete:

• 39 distinct ID migrations completed
• 595 code changes, 93,574 individual edits
• 74.45% of changes and 69.46% of edits generated by the LLM outright
• Roughly 50% reduction in total migration time, developer-estimated against doing the same work by hand

The failure modes are just as informative as the win:

• 25.55% of changes needed manual correction — the model sometimes produced a no-op dressed up as a fix, reformatting the code or adding a comment without making the actual change
• Files that exceeded the context window had to be migrated by hand
• Dart was "not well supported, as the LLM was not trained on enough Dart code" — a plainer version of the training-data-representation gap this post's asymmetry section raised for COBOL and FORTRAN, except the underserved language here is a widely used, entirely modern one

Corpus representation turns out to be a broader problem than "legacy code specifically."

None of that is full software recreation — there's no ESPG here, no differential fuzzer, no symbolic-equivalence proof, just AST checks, a test suite, and a person reading the diff, applied to a type migration rather than a cross-language port. But that's exactly what makes it a useful data point: even at the easy end of this post's spectrum, inside a company with Google's own tooling budget, "no human in the loop" wasn't the destination. A human read every change anyway.

And What It Looks Like Inside Airbnb

Airbnb published a similarly shaped account, credited to engineer Charles Covey-Brandt: migrating nearly 3,500 React component test files from Enzyme to React Testing Library. Narrower still than Google's ID migration — one framework swap, not four languages and a data-flow trace — but built on the same underlying instinct: don't trust a single-shot prompt, build a validated pipeline around it.

Their system modeled each file's conversion as a state machine — an Enzyme refactor step, then Jest fixes, then lint and TypeScript fixes, then done — with a retry loop at every stage that fed validation errors straight back into the next prompt, using context-rich prompts (40,000 to 100,000 tokens of related files, examples, and team-specific patterns) and a "sample, tune, sweep" cycle to keep improving the pipeline itself as failures accumulated.

The numbers land higher than Google's:

• 97% of the 3,500 files converted automatically, three-quarters of those in the first four hours of a bulk run
• 3% — around 100 files — needed a further week of manual work
• Six weeks total elapsed time, against an estimated 1.5 years by hand

The honest part is where they stopped. After 50 to 100 retries on the hardest long-tail files, the team hit what they call a "ceiling of what we could fix via automation" and made the deliberate call to finish those by hand instead of continuing to optimize the pipeline. That's the same discipline this post's mutation-testing and human-sign-off sections keep arguing for: knowing when to stop trusting the automation is itself part of the job, not a failure of it.

Put next to Google's, the two numbers make a small but real point on their own: 97% automated versus 74.45%, on a narrower and more uniform kind of change. The automation rate this technology delivers isn't a fixed constant — it tracks how narrow and uniform the migration actually is, which is the same axis the repository-level translation section raised earlier about method-level versus repo-level difficulty, just measured this time in a live production system instead of a benchmark.

08 Open Questions

Seven gaps the literature hasn't closed, in roughly descending order of how close they are to solvable — and behind each is a place where the pipeline above quietly stops being able to prove what it claims. Several of these looked more open a year ago than they do now; where recent work has actually moved the needle, it's called out below alongside what it still doesn't reach.

Choosing a Pivot Language Without Trying Them All

Multi-hop transitive translation works, which is exactly why the search-space problem stops being theoretical. The Tree of Code Translation ask is no longer "can we route through an intermediate" but "which intermediate, and is one hop enough" — and the current answer is to try paths and measure. Each candidate path costs a full translate-compile-verify cycle, and over a repo with hundreds of modules that cost compounds until exhaustive search stops being an option.

Nobody has a lightweight structural predictor that looks at the source AST and the target and ranks candidate pivots before spending a verification budget. A workable version probably looks like an embedding-based distance — encode both languages, measure how far the source's idioms sit from the target's, and let that rank the intermediate candidates the way a compiler's cost model ranks optimization passes.

The closest recent progress is orthogonal to the actual ask: BabelCoder's generate/validate/repair loop pushes translation accuracy up by iterating harder on a single path — three specialized agents refining one attempt — not by choosing a better path in the first place. That's a real improvement on execution; it says nothing about selection, which is still open.

Proving Functions Equal Doesn't Prove Threads Safe

The verification machinery introduced above reasons about data-flow and return-value equivalence; it does not reason about interleaving or global order. A differential symbolic-execution proof can establish that two functions produce the same output given the same inputs, but it says nothing about whether a fine-grained lock stays correct, or a lock-free structure stays lock-free, across a paradigm shift — thread-pooled blocking I/O to event-driven async, say.

That gap is structural, not incidental: an interleaving is a property of a whole schedule, not of any single path constraint, so per-function path constraints can't contain it. What has to appear is a happens-before or scheduling model layered on top of the equivalence proof before concurrency claims can be verified the way data-flow claims are today.

The closest attempt is explicit about stopping short of it. CIR+CVN has an LLM synthesize a concurrency model from a natural-language specification and formally checks that model against Petri-net semantics — a real, working neuro-symbolic loop, evaluated so far on nine bounded concurrency patterns. But by the authors' own description, "the trust boundary is the generated artifact... rather than arbitrary source code": it verifies the model the LLM produced, not that a translated implementation preserves the legacy source's actual concurrency behavior. That's the harder claim, and it's still unmade.

No Training Signal Rewards Both Speed and Correctness

The TRACE results above gave the cleanest statement of the problem: the model most likely to be functionally correct is routinely not the model most likely to be efficient, because the reasoning-heavy behavior that defends the test pass also buys runtime cost. The open piece is that nobody has a training objective that trades those off on purpose.

The difficulty is that efficiency isn't a per-example label — it's a distributional property of how an implementation behaves across inputs a training set won't contain. Any RL reward that proxies it with token count or a toy-profile signal is wide open to reward hacking, and a signal that only fires on a production-scale benchmark arrives too sparsely and too late to shape decoding. A real objective would penalize an O(N)-to-O(N²) regression the way the field already penalizes a failed test — and as of mid-2026, something finally does, if not yet inside a recreation pipeline like this one.

RLPF attacks the sparsity problem directly with a staged reward: rank failing programs by how far they got before failing, then rank correct ones by efficiency against a reference implementation. On one model, that took correct-and-runnable output from 11.1% to 54.6% and relative efficiency from 8.1% to 38.6%. EffiReasonTrans applies the same dual-objective idea specifically to code translation rather than generation from scratch. Neither is wired into a translation pipeline yet, and RLPF's own cross-benchmark transfer was modest — but "nobody has a training objective for this" stopped being true this year.

Security Checks Have to Move Into the Decoding Loop

The production-debt study's 1.5x ratio is the warning; the upstream fix is the open problem. Catching a vulnerability after code review means a human is still the last line of defense, and the whole lesson of the asymmetry is that the fluent-code bias defeats that. Moving the check earlier — into the decoding or refinement loop itself, before an AST even gets constructed — is the direction, but it collides with the same limitation the correctness side hit: security invariants are cross-file and cross-context.

A path traversal is visible only once the tainted value's origin and its sink are both in view, and a decoding gate that looks at one token at a time cannot see that. What's missing is taint-and-sink tracking integrated into generation rather than bolted onto review.

Constrained decoding already proves this is possible in a narrower sense: CodeGuard+ steers generation away from known CWE patterns and beats prefix-tuning at it, without needing a specialized training set. But the same study found prefix-tuning's apparent security gains often came at the cost of functional correctness — exactly the trade-off a taint-and-sink-aware decoder has to avoid before it's worth deploying ahead of, rather than alongside, code review.

Formal Verification Wasn't Built for COBOL's Column Layout

Differential symbolic execution earns its keep on statically-typed pairs with clean, explicit structure. The exact legacy targets this post keeps circling — COBOL's column layout and packed decimals, FORTRAN's shared blocks, C's raw pointers and unions — break every assumption that machinery leans on: irregular physical layouts that don't map to a tidy type system, GOTO and fall-through that defeat path constraint collection, and pointer aliasing that makes two syntactically distinct expressions refer to the same memory.

Pointing KLEE or Z3 at those inputs isn't a tuning problem; the abstractions they depend on were never built for them. Scaling formal verification to that surface remains genuinely open, and it's the single longest lever on the grand challenge.

The COBOL-specific tooling that does exist stops short of closing it. SEDCoT pairs symbolic execution with delta debugging to localize exactly where an LLM-translated COBOL program's behavior diverges from its source — genuinely useful for debugging a translation in progress. But it's bug-finding, not an equivalence proof, and it doesn't reason about COMP-3 packed decimals or REDEFINES specifically. The tooling got closer to the problem this section describes; the problem is still there.

Beyond Source: Decompilation and Neuro-Symbolic Compilers

Further out, two directions worth naming rather than dwelling on. Autonomous decompilation — the direction Tan et al.'s LLM4Decompile points at — would recreate clean, maintainable source directly from a stripped binary, with no source access at all, going past what IDA Pro and Ghidra give you: pseudo-C that has lost every variable name and struct layout, whose recreation then inherits every verification problem this post has described, with the additional twist that there is no legacy source to fuzz differentially against.

Neuro-symbolic compilers point the other way, folding probabilistic LLM reasoning directly into a deterministic compiler's optimization and synthesis passes rather than sitting in front of it as a separate, and separately-verified, step. That pairing already has a working instance outside the translation context specifically: VerIbmc runs local, open-weight models against ESBMC's bounded model checker for automated loop-invariant synthesis, solving 431 of 499 benchmark problems — beating established checkers like CPA-Checker and 2ls outright, on models small enough to run on-premises. Wiring that same loop into a translation pipeline's own equivalence proofs, rather than a standalone verification benchmark, is the part that's still undone. Both directions are early; both are the natural extension of the pipeline sketched above; and both, tellingly, land on the same unresolved question — how much of software integrity can be delegated to a model that can't, on its own, tell you it was right.

Verifying a System You Can't Safely Run Twice

Every verification technique in this post — differential fuzzing, DSE, mutation testing — assumes you can execute the legacy system on demand, as many times as you like, with synthetic and adversarial inputs alike, and diff the result against a candidate. That assumption is free for a pure function, and expensive but possible for a full node replaying public blockchain history, both covered earlier in this post. It breaks outright for a mainframe transaction system that debits a real account, a SCADA system driving physical machinery, or anything else where running the same input twice isn't idempotent.

The practical answer, where one exists, comes from production engineering rather than formal methods: mirror live traffic at the proxy layer, isolate the replica so its output can't touch the real system, and lean on the legacy system as a running oracle for only as long as it's still in service — a Strangler Fig pattern doing verification's job by attrition instead of proof. That's a reasonable operational answer for a gradual migration. It's a much weaker one for the differential-fuzz and DSE claims this post has been making about proving equivalence before a single line ships, and nothing in the literature surveyed here squares that circle for a genuinely non-replayable system.

09 Conclusions

The cost of writing a second implementation of a legacy system has genuinely collapsed — that part of the pitch holds up. What hasn't collapsed, and what the benchmarks in this post keep insisting on, is the cost of knowing whether the result is actually right: right in the sense of matching behavior on every input, and right in the sense of not silently turning an O(1) lookup into an O(N) one along the way.

That's the actual argument for the seven-stage pipeline over a well-prompted single LLM call: not that it produces better first drafts, but that it produces a provable one — a translation with a differential-fuzz report, a symbolic-equivalence certificate, and a mutation score attached, instead of a diff that reads fine and a test suite that, per TRACE's own numbers, has better-than-even odds of missing a 2x-or-worse slowdown in a translation it just marked "correct." The generative model got cheap. The verification harness around it is where the engineering still lives.

That gap isn't only about speed. The production-debt study in the Technical Debt section showed the same shape on the security side: AI-assisted commits net roughly 1.5× more vulnerabilities than they remediate, because a fluent diff is no more a guarantee of soundness than a green test suite is a guarantee of speed. Both are the same failure of inference — treating plausible as correct — wearing different hats. Which is why the grand challenge that opened this post doesn't end when a model emits idiomatic target code; it ends when a reviewer can look at that code, and at the proof certificate attached to it, and tell which side of that line the machine landed on.

References

• Chen, M., et al. (2021). "Evaluating Large Language Models Trained on Code." arXiv preprint. Available at: arXiv:2107.03374
• Roziere, B., Lachaux, M. A., Chanussot, L., & Lample, G. (2020). "Unsupervised Translation of Programming Languages." Advances in Neural Information Processing Systems (NeurIPS), 33, 20601–20611.
• Aljagthami, A., Banabila, M., Alshehri, M., Kabini, M., & Alahmadi, M. D. (2025). "Evaluating Large Language Models for Code Translation: Effects of Prompt Language and Prompt Design." Proceedings of the ACM Conference on Software Engineering, 1–5.
• Macedo, M., Tian, Y., Nie, P., Cogo, F. R., & Adams, B. (2024). "InterTrans: Leveraging Transitive Intermediate Translations to Enhance LLM-Based Code Translation." arXiv preprint. Available at: arXiv:2411.01063
• Zhang, H., David, C., Wang, M., Paulsen, B., & Kroening, D. (2025). "Scalable, Validated Code Translation of Entire Projects Using Large Language Models." Proceedings of the ACM on Programming Languages (PACMPL / PLDI), 9, 1616–1641.
• Rabbi, F., Saha, S. K., Pham, T. M. T., Wang, S., & Yang, J. (2025). "BabelCoder: Agentic Code Translation with Specification Alignment." arXiv preprint. Available at: arXiv:2512.06902
• Ziftci, C., Nikolov, S., Sjövall, A., Kim, B., Codecasa, D., & Kim, M. (2025). "Migrating Code At Scale With LLMs At Google." arXiv preprint. Available at: arXiv:2504.09691

• Du, X., et al. (2024). "Evaluating Large Language Models in Class-Level Code Generation." Proceedings of the IEEE/ACM 46th International Conference on Software Engineering (ICSE), 1–13.
• Xue, Y., et al. (2025). "ClassEval-T: A Class-Level Code Translation Benchmark." arXiv preprint. Available at: arXiv:2411.06145
• Gong, Z., Sun, Z., Huang, D., Liang, Q., Zhang, J. M., & Hao, D. (2026). "TRACE: Evaluating Execution Efficiency of LLM-Based Code Translation." ACL 2026 / arXiv preprint. Available at: arXiv:2508.11468

• Pan, R., Ibrahimzada, A. R., Krishna, R., Sankar, D., Wassi, L. P., Merler, M., et al. (2024). "Lost in Translation: A Study of Bugs Introduced by Large Language Models While Translating Code." Proceedings of the IEEE/ACM 46th International Conference on Software Engineering (ICSE), 1–13.
• Eniser, H. F., Zhang, H., David, C., Wang, M., Christakis, M., Paulsen, B., Dodds, J., & Kroening, D. (2024). "Towards Translating Real-World Code with LLMs: A Study of Translating to Rust." arXiv preprint. Available at: arXiv:2405.11514
• Entin, P., Gu, W., Knapp, A., & Chen, C. (2026). "SEDCoT: Enhancing LLM-Based COBOL Code Translation via Symbolic Execution and Delta Debugging." arXiv preprint. Available at: arXiv:2607.04092

• Näumann, J., Keidel, S., Sharifloo, A. M., & Mezini, M. (2025). "Beyond BLEU: A Semantic Evaluation Method for Code Translation." Preprint. Available at: arXiv:2509.12973
• Yang, X., et al. (2024). "UniTrans: Unifying Code Translation and Unit Test Generation for Enhanced Code Migration." IEEE Transactions on Software Engineering.
• Bhatia, S., Qiu, J., Hasabnis, N., Seshia, S. A., & Cheung, A. (2024). "Verified Code Transpilation with LLMs." Advances in Neural Information Processing Systems (NeurIPS), 38. Available at: arXiv:2406.03003
• Bai, Y., & Palit, T. (2025). "RustAssure: Differential Symbolic Testing for LLM-Transpiled C-to-Rust Code." arXiv preprint. Available at: arXiv:2510.07604
• Pirzada, M. A. A., Parsert, J., Wang, W., Korovin, K., & Cordeiro, L. C. (2026). "Neuro-Symbolic Software Verification: Hyper-Charging Local Language Models with Symbolic Reasoning at Scale." arXiv preprint. Available at: arXiv:2606.16886
• Zhang, K., & Liu, G. (2026). "CIR+CVN: Bridging LLM Semantic Understanding and Petri-Net Verification for Concurrent Programs." arXiv preprint. Available at: arXiv:2604.09318

• Jing, H., Cui, H., Hu, W., et al. (2026). "RLPF: Reinforcement Learning from Performance Feedback for Code Generation." arXiv preprint. Available at: arXiv:2607.27271
• Wang, Y., Ou, R., Wang, Y., et al. (2025). "EffiReasonTrans: RL-Optimized Reasoning for Code Translation." arXiv preprint. Available at: arXiv:2510.18863

• Liu, Y., Widyasari, R., Zhao, Y., Irsan, I. C., Chen, J., & Lo, D. (2026). "Debt Behind the AI Boom: A Large-Scale Empirical Study of AI-Generated Code in the Wild." IEEE Transactions on Software Engineering / arXiv preprint. Available at: arXiv:2603.28592
• Tan, H., Luo, Q., Li, J., & Zhang, Y. (2024). "LLM4Decompile: Decompiling Binary Code with Large Language Models." Proceedings of EMNLP, 3473–3487.
• Fu, Y., et al. (2024). "Constrained Decoding for Secure Code Generation." arXiv preprint. Available at: arXiv:2405.00218