Developing provably correct Rust code with Verus

Many open-source and industry software projects, including several here at Amazon, are embracing the Rust programming language, since it provides performance and flexibility similar to that of the C programming language, while its clever type system automatically prevents a variety of bugs and security vulnerabilities. The result is fast code that's more correct and secure than average. However, "more correct and secure" is not the same as "actually correct and secure". For example, in C, accessing an array out of bounds — indexing into an array past the boundary of the memory allotted to it — is a dangerous mistake that can have unforeseeable consequences. In Rust, it will halt the program, which is definitely safer, but a correct program would never perform the out-of-bounds access in the first place. Similarly, Rust cannot guarantee that your program will compute the results you were expecting or that…