Rust is a relatively new programming language for writing performant code with strong type and memory safety guarantees. It has become a serious competitor to C and C++ for systems programming, because it provides high-level abstractions but without the cost of garbage collection. Given the growing popularity of Rust, and given that bugs in systems programs can be costly, there is growing interest in the program verification community for building program verifiers for Rust. In this fourth 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.

Submission Guidelines

We solicit proposals for contributed talks and tool demos. Proposals should be at most 2 pages, in either plain text or PDF format, and should specify how long a talk/demo the speaker wishes to give. By default, contributed talks will be 30 minutes long (including time for Q&A), but proposals for shorter or longer talks will also be considered.  

Committees

Organizing Committee

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

• Felix Klock <pnkfelix@pnkfx.org>

• Andrea Lattuada, Max Planck Institute for Software Systems <andrea@mpi-sws.org>

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

Venue

The workshop is co-located with ETAPS 2025, and will be held in McMaster University, Hamilton, Canada in early May.

Contact

All questions about submissions should be emailed to jorajeev@amazon.com