# Verified Code Transpilation with LLMs

arXiv: https://arxiv.org/abs/2406.03003 · HTML: https://mlsanity.com/paper/2406.03003/

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Jun 2024.

## Built on by (most cited first, 15 of 15)

- [Formal Mathematical Reasoning: A New Frontier in AI](https://mlsanity.com/paper/2412.16075/) (2024)
- [A Survey on LLM-based Code Generation for Low-Resource and Domain-Specific Programming Languages](https://mlsanity.com/paper/2410.03981/) (2024)
- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [Autocomp: A Powerful and Portable Code Optimizer for Tensor Accelerators](https://mlsanity.com/paper/2505.18574/) (2025)
- [HoarePrompt: Structural Reasoning About Program Correctness in Natural Language](https://mlsanity.com/paper/2503.19599/) (2025)
- [Leveraging LLMs for Legacy Code Modernization: Challenges and Opportunities for LLM-Generated Documentation](https://mlsanity.com/paper/2411.14971/) (2024)
- [SuperCoder: Assembly Program Superoptimization with Large Language Models](https://mlsanity.com/paper/2505.11480/) (2025)
- [The Hitchhiker's Guide to Program Analysis, Part II: Deep Thoughts by LLMs](https://mlsanity.com/paper/2504.11711/) (2025)
- [FlexSQL: Flexible Exploration and Execution Make Better Text-to-SQL Agents](https://mlsanity.com/paper/2605.02815/) (2026)
- [Unlocking LLM Repair Capabilities Through Cross-Language Translation and Multi-Agent Refinement](https://mlsanity.com/paper/2503.22512/) (2025)
- [LLM-Powered Quantum Code Transpilation](https://mlsanity.com/paper/2507.12480/) (2025)
- [Concept Attractors in LLMs and their Applications](https://mlsanity.com/paper/2601.11575/) (2025)
- [CodePivot: Bootstrapping Multilingual Transpilation in LLMs via Reinforcement Learning without Parallel Corpora](https://mlsanity.com/paper/2604.18027/) (2026)
- [SoK: Understanding (New) Security Issues Across AI4Code Use Cases](https://mlsanity.com/paper/2512.18456/) (2025)
- [The New Compiler Stack: A Survey on the Synergy of LLMs and Compilers](https://mlsanity.com/paper/2601.02045/) (2026)

## Abstract (arXiv)

Domain-specific languages (DSLs) are integral to various software workflows. Such languages offer domain-specific optimizations and abstractions that improve code readability and maintainability. However, leveraging these languages requires developers to rewrite existing code using the specific DSL's API. While large language models (LLMs) have shown some success in automatic code transpilation, none of them provide any functional correctness guarantees on the transpiled code. Another approach for automating this task is verified lifting, which relies on program synthesis to find programs in the target language that are functionally equivalent to the source language program. While several verified lifting tools have been developed for various application domains, they are specialized for specific source-target languages or require significant expertise in domain knowledge to make the search efficient. In this paper, leveraging recent advances in LLMs, we propose an LLM-based approach (LLMLift) to building verified lifting tools. We use the LLM's capabilities to reason about programs to translate a given program into its corresponding equivalent in the target language. Additionally, we use LLMs to generate proofs for functional equivalence. We develop lifting-based compilers for em four different DSLs targeting different application domains. Our approach not only outperforms previous symbolic-based tools in both the number of benchmarks transpiled and transpilation time, but also requires significantly less effort to build.