coq-of-rust: Formal Verification for 100% Bug-Free Rust Code

coq-of-rust is a formal verification tool for Rust that translates Rust programs into the Coq proof assistant to achieve 100% bug-free code. By translating Rust code to Coq, it leverages Coq's powerful proof techniques to verify the correctness of the code, eliminating all bugs. The tool supports a wide range of Rust features and offers formal verification services for critical applications like smart contracts and database engines.