Verus - Verified Rust for low-level systems code by Andrea Lattuada - Rust Zürisee June 2023

Rust programmers care about the correctness of their code and, while the Rust type system and its memory safety are excellent foundations, they aren’t sufficient to ensure correctness. “Full functional verification" of code is an alternative (or a complement) to tests that uses formal methods to prove that the behaviour of a complex program corresponds to a desired specification, i.e. to prove that the program is "correct".

We are building our new tool, Verus, to efficiently verify full functional correctness of low-level systems code written in a safe Rust dialect that supports expressing specifications and proofs. In this talk I'll introduce the basics of functional verification, the verification technique used by Verus, and I'll demonstrate how the tool, with the programmer's help, can ensure that programs are bug-free (or how it catches bugs, if they are any).

Slides: https://github.com/rust-zurichsee/meetups/tree/master/2023-06-08_miri-simd-hir
Guillaume's Blog: https://andrea.lattuada.me/

Would you like to chat or give a talk? Join us in our Matrix room:
https://matrix.to/#/#rust-zuerisee:matrix.coredump.ch

Support the Zürich community: https://estada.ch/support-my-work/

Chapters:
00:00 Introduction
01:19 Examples
38:40 Questions

Видео Verus - Verified Rust for low-level systems code by Andrea Lattuada - Rust Zürisee June 2023 канала Rust