Although Rust primarily intends to be a safe programming language that excludes undefined behaviour, it provides its users with the escape hatch of unsafe Rust, allowing them to circumvent some of its strong compile-time checks. This additional freedom has some advantages, including potentially more efficient code, which is one of the main reasons why unsafe code is used extensively throughout Rust's standard library. However, because unsafe code also re-opens the door to undefined behaviour, Amazon has convened a community to verify the safety of the standard library, and in particular the unsafe code contained therein. Given that this effort is done in public and open-sourced, we have access to a wealth of information on how people are verifying the standard library, as well as what is currently possible and what still appears to be beyond the state of the art for verified software. In this paper, we discuss the lessons learned thus far from this verification effort, from both our work on it, as well as that of the broader community. In particular, we start by reviewing what has been accomplished thus far, as well as the main tools used (specifically, their advantages and their limitations). We then focus on some of the remaining fundamental obstacles to verifying the standard library, and propose potential solutions to overcome them. We hope that these observations can guide future verification of not only the standard library, but also unsafe Rust code in general.

翻译：尽管 Rust 主要旨在成为一种排除未定义行为的安全编程语言，但它为用户提供了不安全 Rust 的“逃生舱口”，允许他们绕过某些严格的编译时检查。这种额外的自由具有一些优势，包括可能实现更高效的代码，这也是不安全代码在 Rust 标准库中被广泛使用的主要原因之一。然而，由于不安全代码也重新打开了未定义行为的大门，亚马逊召集了一个社区来验证标准库的安全性，特别是其中包含的不安全代码。鉴于这项工作是公开且开源的，我们能够获取大量关于人们如何验证标准库的信息，以及当前可能实现的技术和仍超出已验证软件现有技术水平的内容。在本文中，我们讨论了迄今为止从这项验证工作中获得的经验教训，既包括我们自身的工作，也包括更广泛社区的工作。具体而言，我们首先回顾了目前已完成的成果，以及使用的主要工具（特别是它们的优势和局限性）。然后，我们重点关注验证标准库时仍存在的一些基本障碍，并提出克服这些障碍的潜在解决方案。我们希望这些观察结果不仅能为标准库的未来验证提供指导，也能为一般的不安全 Rust 代码验证提供参考。