The March, 2024 Rust for Lunch meet-up. We'll have a single talk and then time for questions afterwards.

We'd like to remind everyone that all participants (speakers, moderators, and attendees) must follow the Code of Conduct during the meetup.

Formal verification for Rust with coq-of-rust

Speaker: Guillaume Claret

With formal verification, we can assert that a program contains no bugs for a specification, covering all execution cases. We present coq-of-rust https://github.com/formal-land/coq-of-rust , a formal verification tool for Rust that we developed. It works by translating Rust programs to the proof system Coq.