This paper introduces a novel Dafny-to-Rust compiler, bridging the gap between Dafny’s general-purpose formal verification capabilities and Rust’s high performance. We present an advanced translation architecture that generates efficient and largely readable Rust code from Dafny source. Our approach tackles critical challenges in type system disparities, memory management, and cross-language interoperability. We validate our compiler’s effectiveness through comprehensive performance evaluations, demonstrating competitive results: in 9 of our 10 benchmarks, the generated code was at most 22% slower than native Rust implementations, with 2 achieving performance parity.