Rust is a rapidly growing programming language for writing performant code with strong type and memory safety guarantees. It is increasily replacing C and C++ for systems programming, because it provides high-level abstractions without the cost of garbage collection. Given the popularity of Rust, and given that bugs in systems programs are costly, there is strong interest in the program verification community for building tools for checking correctness of Rust programs. In this sixth workshop in the series, we aim to continue the conversation among language designers, application developers and formal verification tool builders, to exchange ideas and build collaborations around developing verified Rust programs. 

The goal of the workshop is to bring together researchers from a variety of different backgrounds and perspectives to exchange new and exciting ideas concerning the verification of Rust programs and explore potential avenues for collaboration.

We would like the workshop to be informal and interactive. The program will thus involve a combination of invited talks, contributed talks about work in progress, tool demos, and open discussion sessions. There will be no published proceedings, but participants will be encouraged to submit working documents, talk slides, etc. to be posted on this website.

Building on the success of the first five Rust Verification workshops (virtually in 2021, and in-person in 2022, in 2023, in 2024, and in 2025), we are once again expanding the workshop to span 2 days.

Organizers

• Rajeev Joshi, Amazon Web Services <jorajeev@amazon.com>

• Alex Summers, The University of British Columbia, <alex.summers@ubc.ca>