This is the repository to go with the talk I gave at this years' LambdaConf. It goes over the fact that Rusts' borrow checker was formally verified, why that matters, and walks through some of the example source code in the paper the authors put together.
The slides are in this repo, as both .pptx and .pdf, but if you want the Google Slides view link, it's right here.
The paper I referenced is here.
Enjoy the material!