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.

翻译：摘要：Rust语言融合了内存安全与底层控制能力，在提供类C性能的同时默认避免未定义行为。随着Rust语言日益普及，如何安全正确地迁移现有代码库至Rust已成为研究热点。现有方法分为两类：基于规则的方法和基于大语言模型（LLM）的方法。基于规则的方法理论上能够生成保持与原程序输入输出等价性的正确迁移代码，但其生成的Rust代码通常不可读且依赖于Rust的不安全子集。相比之下，基于LLM的方法通常能生成更可读、可维护且安全的代码，但无法保证正确性。本文提出VERT工具，可在提供形式化正确性保证的前提下生成可读的Rust迁移代码。VERT的唯一前提条件是源代码语言存在Web Assembly编译器（目前主流语言大多满足该条件）。VERT首先通过Web Assembly编译器获取Oracle Rust程序，同时使用LLM生成可读候选Rust程序。随后将候选程序与Oracle程序进行验证，若验证失败则重新生成候选迁移代码直至验证通过。我们在包含1394个竞争性编程基准测试程序的数据集上对VERT进行评估。与单独使用Anthropic的Claude-2相比，结合VERT后基于属性测试的Rust迁移通过率从31%提升至54%，基于有界模型检验的通过率从1%提升至42%。此外，我们还在大量使用指针的真实C项目上评估VERT生成非平凡安全Rust代码的能力。实验结果揭示了LLM在编写安全Rust代码方面的局限性。