New Calculus Lets LLM-Generated Compilers Verify Each Other Across Multiple Languages

Researchers have developed a formal framework for reasoning about code translation when neither individual translators nor their authors can be fully trusted. Rather than requiring each compiler to be proven correct once (certified compilation) or checking each output manually (translation validation), the new approach treats translation as a network of relationships where correctness claims vary from one path to another.

The Core Problem#

Most compiler verification focuses on a single translator in isolation. In practice, systems often need to support many source languages and multiple routes to different reasoning targets. When an independent developer contributes a new language pair via machine learning or hand-coded implementation, the system needs a way to admit it based on its correctness properties, not the author's reputation. This creates a tension: how do you trust answers from untrusted contributors?

A Fidelity-Graded Approach#

The new calculus assigns each translation pair a fidelity grade — a confidence level that represents what kind of correctness guarantee it provides. These grades compose according to a "weakest link" principle: a chain of translations is only as reliable as its least trustworthy step. The framework supports inline checking during execution to re-establish grades per run, and crucially, grades improve when independent routes between the same languages produce matching results, creating a form of mutual validation.

A key insight is an end-to-end theorem distinguishing two types of answers: those carrying witnesses (proofs) are self-certifying at the source, while universal claims require the full machinery of grades, multiple branches, and certificates to be cost-effective. The compositional core is mechanized in Lean 4.

Implementation: Hurdy-Gurdy#

The researchers tested the framework on hurdy-gurdy, a platform of 13 programming languages with 13 translation pairs connecting two reasoning hubs. Uniquely, every language pair was written by independent large language model agents, largely without human supervision — the architecture's cross-checks served as the only semantic gate. The platform itself is designed as a target for LLM reasoning, and most of the paper was also generated by machine, with humans providing only the architectural design.

The intended growth model reflects this philosophy: anyone can contribute new language pairs (via LLMs, agent-based systems, or manually), and they are admitted based on whether the architecture can verify them, not on who wrote them.