# VERT: Verified Equivalent Rust Transpilation with Large Language Models as Few-Shot Learners

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

## Key facts

- Cited by 20 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Apr 2024.

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

- [AlphaTrans: A Neuro-Symbolic Compositional Approach for Repository-Level Code Translation and Validation](https://mlsanity.com/paper/2410.24117/) (2024)
- [CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation](https://mlsanity.com/paper/2504.15254/) (2025)
- [Syzygy: Dual Code-Test C to (safe) Rust Translation using LLMs and Dynamic Analysis](https://mlsanity.com/paper/2412.14234/) (2024)
- [From Code Foundation Models to Agents and Applications: A Comprehensive Survey and Practical Guide to Code Intelligence](https://mlsanity.com/paper/2511.18538/) (2025)
- [SACTOR: LLM-Driven Correct and Idiomatic C to Rust Translation with Static Analysis and FFI-Based Verification](https://mlsanity.com/paper/2503.12511/) (2025)
- [Raw Pointer Rewriting with LLMs for Translating C to Safer Rust](https://mlsanity.com/paper/2505.04852/) (2025)
- [MatchFixAgent: Language-Agnostic Autonomous Repository-Level Code Translation Validation and Repair](https://mlsanity.com/paper/2509.16187/) (2025)
- [Skeleton-Guided-Translation: A Benchmarking Framework for Code Repository Translation with Fine-Grained Quality Evaluation](https://mlsanity.com/paper/2501.16050/) (2025)
- [Program Skeletons for Automated Program Translation](https://mlsanity.com/paper/2504.07483/) (2025)
- [Adversarial Agent Collaboration for Correctness Improvements of C to Safe Rust Translation](https://mlsanity.com/paper/2510.03879/) (2025)
- [ENCRUST: Encapsulated Substitution and Agentic Refinement on a Live Scaffold for Safe C-to-Rust Translation](https://mlsanity.com/paper/2604.04527/) (2026)
- [C2RUST-BENCH: A Minimized, Representative Dataset for C-to-Rust Transpilation Evaluation](https://mlsanity.com/paper/2504.15144/) (2025)
- [His2Trans: A Knowledge-Guided Agentic Framework for Project-Level C-to-Rust Migration](https://mlsanity.com/paper/2603.02617/) (2026)
- [ORBIT: Guided Agentic Orchestration for Autonomous C-to-Rust Transpilation](https://mlsanity.com/paper/2604.12048/) (2026)
- [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)
- [Documentation-Guided Agentic Codebase Migration from C to Rust](https://mlsanity.com/paper/2605.14634/) (2026)
- [The Periodic Table of LLM Reasoning: A Structured Survey of Reasoning Paradigms, Methods, and Failure Modes](https://mlsanity.com/paper/2606.11470/) (2026)
- [TreeAgent: A Generalizable Multi-Agent Framework for Automated Bias Labeling in Forestry via Compiled Expert Rules and Vision-Language Models](https://mlsanity.com/paper/2606.31976/) (2026)
- [Towards Reliable C-to-Rust Translation with Rule-Guided Reasoning and Reinforcement Learning](https://mlsanity.com/paper/2607.19966/) (2026)

## Abstract (arXiv)

Rust is a programming language that combines memory safety and low-level control, providing C-like performance while guaranteeing the absence of undefined behaviors by default. Rust's growing popularity has prompted research on safe and correct transpiling of existing code-bases to Rust. Existing work falls into two categories: rule-based and large language model (LLM)-based. While rule-based approaches can theoretically produce correct transpilations that maintain input-output equivalence to the original, they often yield unreadable Rust code that uses unsafe subsets of the Rust language. On the other hand, while LLM-based approaches typically produce more readable, maintainable, and safe code, they do not provide any guarantees about correctness. In this work, we present VERT, a tool that can produce readable Rust transpilations with formal guarantees of correctness. VERT's only requirement is that there is Web Assembly compiler for the source language, which is true for most major languages. VERT first uses the Web Assembly compiler to obtain an oracle Rust program. In parallel, VERT uses an LLM to generate a readable candidate Rust program. This candidate is verified against the oracle, and if verification fails, we regenerate a new candidate transpilation until verification succeeds. We evaluate VERT by transpiling a suite of 1,394 programs taken from competitive programming style benchmarks. Combining Anthropic's Claude-2 and VERT increases Rust transpilations passing property-based testing from 31% to 54% and bounded model-checking from 1% to 42% compared to using Claude alone. In addition, we evaluate VERT's ability to generate non-trivial safe Rust on programs taken from real-world C projects that make significant use of pointers. Our results provide insights into the limitations of LLMs to write safe Rust.