Skip to content
Verification working group
Branch: master
Clone or download
avadacatavra Merge pull request #8 from kini/broken-link
Fix a broken link on the site
Latest commit 6f9e9cd Apr 9, 2018
Type Name Latest commit message Commit time
Failed to load latest commit information.
docs Fix a broken link on the site Apr 9, 2018
LICENSE-APACHE Added licensees Apr 2, 2018
LICENSE-CC-BY-SA Added licensees Apr 2, 2018
LICENSE-MIT Added licensees Apr 2, 2018 make gh page in docs/ Apr 5, 2018

The Rust Verification working group

This working group is intended to provide a forum for all things formal methods and verification for Rust. We anticipate significant overlap in requirements for tools and want to provide a central repository to exchange ideas and share progress.

For an overview of our current status, visit our (WIP) page.

Why Rust?

Most of the benefits of performing verification on Rust programs are directly derived from the guarantees of safe Rust. Unsafe code is significantly more complex, but it may be possible to define contracts that must be upheld at the unsafe boundary. For more information on the differences between safe and unsafe Rust, see the Rustonomicon.

  • No need to reason extensively about the memory model
  • Data races are eliminated
  • A substantial subset can be transformed into pure functions


  • Develop formal foundations for the Rust language (RustBelt).
  • Extract required information from the compiler
  • Design methods to formally verify programs written in Rust
  • Investigate ways to combine program verification with broader testing frameworks

Get Involved

Join our mailing list, get in touch with us or open a pull request to let us know about your Rust verification project.

We follow the Rust Code of Contact. Any concerns should be brought to


The output of the verification working group is distributed under the following licenses:

You can’t perform that action at this time.