Verification WG Goals

Short Term

Extract required information from the compiler

• trait impls
• MIR
• types

Determine a way to write specifications

• create a set of example
• subset of rust
• extensible

Areas of interest

• Functional correctness
• Taint Tracing
• Reachability
• Constant time execution

Long term

Formalize semantics of the Rust language itself

• make the semantic model more faithful to the language
• reason about the memory model (in particular, relaxed memory)
• create a valgrind plugin?

Perform verification directly on Rust programs

• Eventually, also be able to verify unsafe code

Integrate verification with testing