Theseus

Memory bugs in C parsers keep turning into critical vulnerabilities, and everyone agrees that code should move to Rust. Few teams migrate, because nobody can show the rewrite behaves the same. Theseus doesn't ask the model whether the port works. Gemini 4 Argon translates the C library into safe Rust (#![forbid(unsafe_code)], no dependencies, no way to call the C). Then a deterministic verifier runs the original and the replacement on the same inputs and compares every output byte. Each difference goes back to Argon as a pattern to repair, and compiler errors go back the same way. The final build is checked again on held-out inputs the model never saw. A person approves, and a managed agent opens a pull request carrying the code and the verifier's evidence report.