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主要旨在成为排除未定义行为的安全编程语言，但它仍为用户提供了unsafe Rust这一"逃生舱口"，允许其绕过部分严格的编译时检查。这种额外自由度具有若干优势，包括可能实现更高效率的代码，这也是unsafe代码在Rust标准库中被广泛使用的主要原因之一。然而，由于unsafe代码会重新开启未定义行为的大门，亚马逊已召集社区开展标准库安全性验证工作，重点针对其中包含的unsafe代码。鉴于该工作以公开开源方式进行，我们得以获取大量关于标准库验证方法的信息，以及当前验证技术的可行边界与前沿局限。本文系统论述从该验证工作中迄今获得的经验，涵盖我们自身及更广泛社区的研究成果。具体而言，我们首先回顾目前已完成的验证成果及使用的主要工具（特别关注其优势与局限性），继而聚焦验证标准库仍面临的基础性障碍，并提出潜在的解决方案。我们希望这些发现不仅能指导标准库的未来验证工作，也能为unsafe Rust代码的通用验证提供方向。