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

July

Due to a cancellation we no longer have a scheduled speaker for July! If you're interested please let us know.

We hold our meetings on the last monday of every month. Currently, we base ourselve off of European time, with meetings at 7PM. If this causes an issue for you, please leave a message on zulip.