A n automatic conversion technology developed by Korea Advanced Institute of Science & Technology researchers transforms legacy C code into Rust, addressing C’s structural vulnerabilities. The work mathematically proves the correctness of the translations, unlike methods that rely on large language models. The approach includes converting key C features such as mutexes, output parameters, and unions into Rust while preserving behavior. The researchers also are exploring verification of quantum-computer programs and automation of WebAssembly correctness.