Open Source Summit North America 2025

The Rust programming language is experiencing rapid adoption in critical infrastructure and systems programming, propelled by its memory safety guarantees and developer productivity advantages. Significant technology policies, such as the US National Cyber Strategy, explicitly endorse Rust as a pathway to memory-safe software. Unsafe code blocks, however, can circumvent Rust’s compile-time guarantees. To address this disparity, AWS has collaborated with the Rust Foundation on the Rust Standard Library Verification project, whose objective is to formally verify the safety of the Rust standard library. We are actively integrating automated verification into the Rust Library release process, thereby ensuring continuous safety validation across releases.

Our presentation will elucidate the structural framework and rationale underpinning our verification contest. We will demonstrate our current progress, showcasing successful verification examples and discussing the diverse open-source tools employed in the verification process. We will conclude with our prioritized areas for 2025 and practical ways for the Rust community to actively participate in this pivotal security initiative.