Rebooting the formal verification working group


You might remember that earlier this year, we started up a formal verification working group…

So, what happened? Well, not that much (sorry!). So, I’d like to reboot the working group with some more concrete goals. To start, we will:

  • identify information needed by tools from the compiler
  • build a set of simple examples to test verification tools on

Overall, the plan for this WG is to enable formal verification of Rust programs, not creating a full semantics of the language (for that, go check out the RustBelt project).

What can you do to help? We have a gitter chat and a github repo. If you currently work on a fv project/tool, open up a PR on the repo to explain what your project does and what information it needs.

Follow us on Twitter!


For better visibility (and because folks cannot feasibly be on Discord, Zulip, IRC, Gitter all at once) I’d recommend moving to Discord.


/me is on Discord, Zulip, IRC and Gitter (and a little grumpy about it)

Here’s a poll on which chat people would like to use: