HiRustVer: Industrial Rust Verification via Mature C Toolchains

Rust is increasingly adopted in mission-critical systems, yet its type system alone cannot prevent panics, logic errors, or undefined behavior from unsafe code—formal verification remains necessary. However, real-world industrial Rust codebases pose three key challenges for verification: pervasive use of advanced features (associated types, dynamic dispatch, closures, unsafe blocks), complex dependency graphs with over a hundred transitive crates, and stringent industrial constraints where code rewriting is infeasible and automation is essential. No existing Rust verification tool meets these combined requirements. We present HiRustVer, a verification framework that takes a different route: translating Rust to verification-friendly C to exploit the maturity of existing C verification infrastructure. Our pipeline extends Charon (Rust to LLBC) and Eurydice (LLBC to C) with broader Rust feature support, then employs Frama-C for deductive verification with LLM-based contract inference to reduce manual annotation overhead. Applied to a production component from Huawei's HarmonyOS, HiRustVer successfully translates the entire codebase—handling associated types, dynamic dispatch, closures, and unsafe blocks—and achieves 56% automated verification, with the remainder under expert review. This work demonstrates that formal verification of real-world, non-verification-oriented Rust codebases is achievable today with appropriate tooling and engineering effort.