Rebooting the formal verification working group


#1

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!


#2

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


#3

/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: https://doodle.com/poll/zncq2asiusctqtab