  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.
