2024-03-19

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.

• Meet-up call link: https://lecture.senfcall.de/hay-gmh-wox-mru (Senfcall)
• Date: Tuesday, 19 March, 2024
• Time: 12:00 - 13:00 UTC
  • 12:00 - 13:00 GMT (e.g. London, Bamako)
  • 13:00 - 14:00 WAT/CET (e.g. Kinshasa, Berlin)
  • 14:00 - 15:00 EET/CAT (e.g. Lviv, Cairo)

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.

• Slides online: https://formal.land/lunch-rs-presentation/
• Slides download: Slides: lunch-rs-guillaume-coq-of-rust.zip