The RFMIG provides a forum for academics, industry users and any other interested party discuss and collaborate on the challenges of Rust program verification.
Our objectives are to:
Improve communication between formal tool developers and the Rust core teams
- Hold 'office hours' with Rust team members to answer questions about the
rustcAPI or the direction of the language.
- Identify weak points in Rust's current tool interfaces, help shepherd the improvements the formal methods community needs.
Foster a community of formal methods tools and users
- Provide a platform for tool developers to share their work and encourage collaboration.
- Gather feedback and input from industrial and hobbyist users of formal method tooling.
- Work towards improving tool inter-compatibility, in particular of specifications.
These initiatives may interest the developers of formal methods tools for Rust, don't hesitate to join the discussion on Zulip.
- Project Stable MIR: An effort to define a semi-stable API boundary for the Rust compiler specifically targeting verification usecases.
- Project Ghost Code: An experiment to define a generic notion of 'ghost code' for use in the compiler which would enable verification tools to more easily encode their invariants.