Rust Formal Methods Interest Group

WG repo | Zulip Channel

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 rustc API 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.

Interesting projects

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.

Upcoming Meetings

January (TBA)

s