Performant, Readable and Interoperable Rust from Dafny

Watch this 17-minute conference talk from the Dafny 2025 workshop that introduces a novel Dafny-to-Rust compiler developed by researchers from Amazon Web Services and UC Berkeley. Learn about an advanced translation architecture that generates efficient and readable Rust code from Dafny source, addressing challenges in type system disparities, memory management, and cross-language interoperability. Discover how this compiler bridges the gap between Dafny's formal verification capabilities and Rust's high performance, with comprehensive benchmarks showing the generated code performing within 22% of native Rust implementations in most cases, and achieving performance parity in two benchmarks. This presentation was sponsored by ACM SIGPLAN and delivered at the Dafny 2025 workshop on January 19, 2025.