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!